let s be State of SCM ; :: 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 A1: s . (IC (Computation s,k)) = halt SCM ; :: thesis: Result s = Computation s,k
then A2: s is halting by Th3;
CurInstr (Computation s,k) = halt SCM by A1, AMI_1:54;
hence Result s = Computation s,k by A2, AMI_1:def 22; :: thesis: verum