let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA
for J being really-closed 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 really-closed InitHalting keepInt0_1 Program of SCM+FSA
for J being really-closed 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 really-closed InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being really-closed 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 really-closed 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;
A3: ( Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) ) by FUNCT_4:25;
A4: ( I c= p +* I & I c= (p +* (I ";" J)) +* I ) by FUNCT_4:25;
then A5: (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 Th6, A3;
A6: 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 A7: 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 Th13, A6;
LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((p +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by A3, Th6, A4;
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 A7, A1, A5, Th6, A2; :: thesis: verum