let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Element of NAT holds (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for s being State of S
for k being Element of NAT holds (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
let s be State of S; :: thesis: for k being Element of NAT holds (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
let k be Element of NAT ; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
A: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by LmY;
thus (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by A; :: thesis: verum