let s be State of SCM ; :: thesis: for k being Element of NAT holds
( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & s is halting ) )
let k be Element of NAT ; :: thesis: ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM iff ( LifeSpan s = k + 1 & s is halting ) )

hereby :: thesis: ( LifeSpan s = k + 1 & s is halting implies ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM ) )

assume ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM ) ; :: thesis: ( LifeSpan s = k + 1 & s is halting )
then A1: ( s is halting & CurInstr (Computation s,k) <> halt SCM & CurInstr (Computation s,(k + 1)) = halt SCM ) by Th3, AMI_1:54;

now

let i be Element of NAT ; :: thesis: ( CurInstr (Computation s,i) = halt SCM implies not k + 1 > i )
assume A2: ( CurInstr (Computation s,i) = halt SCM & k + 1 > i ) ; :: thesis: contradiction
then i <= k by NAT_1:13;
hence contradiction by A1, A2, AMI_1:52; :: thesis: verum

end;

hence ( LifeSpan s = k + 1 & s is halting ) by A1, AMI_1:def 46; :: thesis: verum

end;

assume A3: ( LifeSpan s = k + 1 & s is halting ) ; :: thesis: ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM )
then A4: ( CurInstr (Computation s,(k + 1)) = halt SCM & ( for l being Element of NAT st CurInstr (Computation s,l) = halt SCM holds
k + 1 <= l ) ) by AMI_1:def 46;

now

assume CurInstr (Computation s,k) = halt SCM ; :: thesis: contradiction
then k + 1 <= k by A3, AMI_1:def 46;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence ( s . (IC (Computation s,k)) <> halt SCM & s . (IC (Computation s,(k + 1))) = halt SCM ) by A4, AMI_1:54; :: thesis: verum