let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J))))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J))))
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA holds LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J))))
let J be parahalting Program of SCM+FSA; :: thesis: LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J))))
( s +* (Initialized (I ';' J)),(s +* (Initialized (I ';' J))) +* I equal_outside NAT & s +* (Initialized I),s +* (Initialized (I ';' J)) equal_outside NAT ) by FUNCT_7:132, SCMFSA6A:53;
then A1: s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
A2: I ';' J c= P +* (I ';' J) by FUNCT_4:26;
Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
then A3: LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I))) + 1) + (LifeSpan ((((P +* (I ';' J)) +* I) +* J),((Result (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J)))) by Lm5, A2;
A4: ( Initialize J c= (Result (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J) & Initialize J c= (Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J) ) by Th8, FUNCT_4:26;
A5: J c= ((P +* (I ';' J)) +* I) +* J by FUNCT_4:26;
A6: J c= (P +* I) +* J by FUNCT_4:26;
Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
then A7: Initialize I c= (s +* (Initialized (I ';' J))) +* I by Th8;
A8: I c= (P +* (I ';' J)) +* I by FUNCT_4:26;
A9: I c= P +* I by FUNCT_4:26;
A10: Initialize I c= s +* (Initialized I) by Th8, FUNCT_4:26;
then Result ((P +* I),(s +* (Initialized I))), Result (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) equal_outside NAT by A7, A1, Th29, A8, A9;
then Result (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)), Result ((P +* I),(s +* (Initialized I))) equal_outside NAT by FUNCT_7:28;
then A11: (Result (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J),(Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J) equal_outside NAT by FUNCT_7:106;
LifeSpan ((P +* I),(s +* (Initialized I))) = LifeSpan (((P +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) by A10, A7, A1, Th29, A8, A9;
hence LifeSpan ((P +* (I ';' J)),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialized I)))) +* (Initialized J)))) by A3, A4, A11, Th29, A5, A6; :: thesis: verum