let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting keeping_0 Program of
for J being really-closed parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed parahalting keeping_0 Program of
for J being really-closed parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let I be really-closed parahalting keeping_0 Program of ; :: thesis: for J being really-closed parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let J be really-closed parahalting Program of ; :: thesis: LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
A1: 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 A2: 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 Lm2, A1;
A3: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
A4: J c= (P +* I) +* J by FUNCT_4:25;
A5: I c= (P +* (I ";" J)) +* I by FUNCT_4:25;
A6: I c= P +* I by FUNCT_4:25;
A7: (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 Th8, A5, A6;
A8: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by Th8, A5, A6;
thus LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) by A7, Th8, A3, A4, A2, A8; :: thesis: verum