let s1, s2 be State of SCM ; :: thesis: for k, c being Element of NAT st s2 = Computation s1,k & LifeSpan s2 = c & s2 is halting & 0 < c holds
LifeSpan s1 = k + c
let k, c be Element of NAT ; :: thesis: ( s2 = Computation s1,k & LifeSpan s2 = c & s2 is halting & 0 < c implies LifeSpan s1 = k + c )
assume A1: ( s2 = Computation s1,k & LifeSpan s2 = c & s2 is halting & 0 < c ) ; :: thesis: LifeSpan s1 = k + c
then consider l being Nat such that
A2: c = l + 1 by NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
( s2 . (IC (Computation s2,l)) <> halt SCM & s2 . (IC (Computation s2,(l + 1))) = halt SCM ) by A1, A2, Th16;
then ( s2 . (IC (Computation s1,(k + l))) <> halt SCM & s2 . (IC (Computation s1,(k + (l + 1)))) = halt SCM ) by A1, AMI_1:51;
then ( s1 . (IC (Computation s1,(k + l))) <> halt SCM & s1 . (IC (Computation s1,(k + (l + 1)))) = halt SCM ) by A1, AMI_1:54;
hence LifeSpan s1 = (k + l) + 1 by Th16
.= k + c by A2 ;
:: thesis: verum