let N be 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 (Computation s,k)) = CurInstr (Computation 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 (Computation s,k)) = CurInstr (Computation s,k)
let s be State of S; :: thesis: for k being Element of NAT holds (ProgramPart s) . (IC (Computation s,k)) = CurInstr (Computation s,k)
let k be Element of NAT ; :: thesis: (ProgramPart s) . (IC (Computation s,k)) = CurInstr (Computation s,k)
A: ProgramPart s = ProgramPart (Computation s,k) by LmY;
IC (Computation s,k) in NAT by Def4;
hence (ProgramPart s) . (IC (Computation s,k)) = (Computation s,k) . (IC (Computation s,k)) by A, FUNCT_1:72
.= CurInstr (Computation s,k) ;
:: thesis: verum