let k be Element of NAT ; :: thesis: for s being State of SCM holds Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
let s be State of SCM ; :: thesis: Comput (ProgramPart s),s,(k + 1) = Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:144;
thus Comput (ProgramPart s),s,(k + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by T ; :: thesis: verum