let s be State of ; :: thesis: ( ex k being Element of NAT st s . (IC (Computation s,k)) = halt SCM implies ProgramPart s halts_on s )
given k being Element of NAT such that A1: s . (IC (Computation s,k)) = halt SCM ; :: thesis: ProgramPart s halts_on s
take k ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,k) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,k)) = halt SCM )
IC (Computation s,k) in NAT by AMI_1:def 4;
hence IC (Computation s,k) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,k)) = halt SCM
CurInstr (Computation s,k) = halt SCM by A1, AMI_1:54;
hence (ProgramPart s) . (IC (Computation s,k)) = halt SCM by AMI_1:145; :: thesis: verum