let s be State of SCM ; :: thesis: ( ex k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt SCM implies ProgramPart s halts_on s )
given k being Element of NAT such that A1: s . (IC (Comput (ProgramPart s),s,k)) = halt SCM ; :: thesis: ProgramPart s halts_on s
take k ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,k) in proj1 (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt SCM )
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;
IC (Comput (ProgramPart s),s,k) in NAT ;
hence IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt SCM
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM by A1, AMI_1:54, Y;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt SCM by AMI_1:145; :: thesis: verum