let s be State of ; :: thesis: for k being Element of NAT st s . (IC (Computation s,k)) = halt SCM holds
Result s = Computation s,k
let k be Element of NAT ; :: thesis: ( s . (IC (Computation s,k)) = halt SCM implies Result s = Computation s,k )
assume s . (IC (Computation s,k)) = halt SCM ; :: thesis: Result s = Computation s,k
then ( ProgramPart s halts_on s & CurInstr (Computation s,k) = halt SCM ) by Th3, AMI_1:54;
hence Result s = Computation s,k by AMI_1:def 22; :: thesis: verum