let s be State of SCM ; :: thesis: for k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt SCM holds
Result (ProgramPart s),s = Comput (ProgramPart s),s,k
let k be Element of NAT ; :: thesis: ( s . (IC (Comput (ProgramPart s),s,k)) = halt SCM implies Result (ProgramPart s),s = Comput (ProgramPart s),s,k )
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:123;
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 COMPOS_1:38;
assume Z: s . (IC (Comput (ProgramPart s),s,k)) = halt SCM ; :: thesis: Result (ProgramPart s),s = Comput (ProgramPart s),s,k
then X: ProgramPart s halts_on s by Th3;
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = halt SCM by Z, Y, TX, AMI_1:54;
hence Result (ProgramPart s),s = Comput (ProgramPart s),s,k by X, AMI_1:def 22; :: thesis: verum