let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ';' J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ';' J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ';' J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))
let J be InitHalting Program of SCM+FSA; :: thesis: LifeSpan ((p +* (I ';' J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))
set inI = Initialize ((intloc 0) .--> 1);
set inIJ = Initialize ((intloc 0) .--> 1);
set inJ = Initialize ((intloc 0) .--> 1);
A1: ( Initialize ((intloc 0) .--> 1) c= (Result (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) ) by FUNCT_4:25;
A2: ( J c= ((p +* (I ';' J)) +* I) +* J & J c= (p +* I) +* J ) by FUNCT_4:25;
A4: ( Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) ) by FUNCT_4:25;
A5: ( I c= p +* I & I c= (p +* (I ';' J)) +* I ) by FUNCT_4:25;
then A6: (Result (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by Th15, A4;
A7: I ';' J c= p +* (I ';' J) by FUNCT_4:25;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then A8: LifeSpan ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan ((((p +* (I ';' J)) +* I) +* J),((Result (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) by Th25, A7;
LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by A4, Th15, A5;
hence LifeSpan ((p +* (I ';' J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1))))) by A8, A1, A6, Th15, A2; :: thesis: verum