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