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 s = Comput (ProgramPart s),s,k
let k be Element of NAT ; :: thesis: ( s . (IC (Comput (ProgramPart s),s,k)) = halt SCM implies Result s = Comput (ProgramPart s),s,k )
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 AMI_1:150;
assume s . (IC (Comput (ProgramPart s),s,k)) = halt SCM ; :: thesis: Result s = Comput (ProgramPart s),s,k
then ( ProgramPart s halts_on s & CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM ) by Th3, AMI_1:54, Y;
hence Result s = Comput (ProgramPart s),s,k by AMI_1:def 22; :: thesis: verum