let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting 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 InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting 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 InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting 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 InitHalting 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))))
set inI = Initialized I;
set inIJ = Initialized (I ';' J);
set inJ = Initialized J;
A1: ( Initialized J c= (Result (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J) & Initialized J c= (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) ) by FUNCT_4:26;
A2: ( J c= ((p +* (I ';' J)) +* I) +* J & J c= (p +* I) +* J ) by FUNCT_4:26;
( 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 A3: s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
A4: ( Initialized I c= s +* (Initialized I) & Initialized I c= (s +* (Initialized (I ';' J))) +* I ) by FUNCT_4:26, SCMFSA6A:52;
A5: ( I c= p +* I & I c= (p +* (I ';' J)) +* I ) by FUNCT_4:26;
then Result ((p +* I),(s +* (Initialized I))), Result (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) equal_outside NAT by A3, Th15, A4;
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 A6: (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;
A7: I ';' J c= p +* (I ';' J) by FUNCT_4:26;
Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
then A8: 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 Th25, A7;
LifeSpan ((p +* I),(s +* (Initialized I))) = LifeSpan (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) by A4, A3, Th15, A5;
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 A8, A1, A6, Th15, A2; :: thesis: verum