let s1, s2 be State of SCM ; :: thesis: for k, c being Element of NAT st s2 = Comput (ProgramPart s1),s1,k & LifeSpan (ProgramPart s2),s2 = c & ProgramPart s2 halts_on s2 & 0 < c holds
LifeSpan (ProgramPart s1),s1 = k + c
let k, c be Element of NAT ; :: thesis: ( s2 = Comput (ProgramPart s1),s1,k & LifeSpan (ProgramPart s2),s2 = c & ProgramPart s2 halts_on s2 & 0 < c implies LifeSpan (ProgramPart s1),s1 = k + c )
assume that
A1: s2 = Comput (ProgramPart s1),s1,k and
A2: ( LifeSpan (ProgramPart s2),s2 = c & ProgramPart s2 halts_on s2 ) and
A3: 0 < c ; :: thesis: LifeSpan (ProgramPart s1),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:123;
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, T, AMI_1:51;
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, T, AMI_1:51;
then s1 . (IC (Comput (ProgramPart s1),s1,(k + l))) <> halt SCM by A1, AMI_1:54;
hence LifeSpan (ProgramPart s1),s1 = (k + l) + 1 by A5, Th16
.= k + c by A4 ;
:: thesis: verum