let k be Element of NAT ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S holds Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),s,k)
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 holds Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (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 holds Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),s,k)
let s be State of S; :: thesis: Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),s,k)
A: ProgramPart (Comput (ProgramPart s),s,k) = ProgramPart s by LmY;
X: s . (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by Th54;
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by BWL1;
thus Comput (ProgramPart s),s,(k + 1) = Following (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by Th14, A
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
.= Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),s,k) by X, Y ; :: thesis: verum