let s be State of ; :: thesis: for k being Element of NAT st IC (Computation s,k) <> IC (Computation s,(k + 1)) & s . (IC (Computation s,(k + 1))) = halt SCM holds
LifeSpan s = k + 1
let k be Element of NAT ; :: thesis: ( IC (Computation s,k) <> IC (Computation s,(k + 1)) & s . (IC (Computation s,(k + 1))) = halt SCM implies LifeSpan s = k + 1 )
assume that
A1: IC (Computation s,k) <> IC (Computation s,(k + 1)) and
A2: s . (IC (Computation s,(k + 1))) = halt SCM ; :: thesis: LifeSpan s = k + 1

now

assume s . (IC (Computation s,k)) = halt SCM ; :: thesis: contradiction
then CurInstr (Computation s,k) = halt SCM by AMI_1:54;
hence contradiction by A1, AMI_1:52, NAT_1:11; :: thesis: verum

end;

hence LifeSpan s = k + 1 by A2, Th16; :: thesis: verum