let s be State of SCM ; :: thesis: ( ex k being Element of NAT st s . (IC (Computation s,k)) = halt SCM implies s is halting )
given k being Element of NAT such that A1: s . (IC (Computation s,k)) = halt SCM ; :: thesis: s is halting
take k ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,k) = halt SCM
thus CurInstr (Computation s,k) = halt SCM by A1, AMI_1:54; :: thesis: verum