let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being 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 parahalting keeping_0 Program of
for J being 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 parahalting keeping_0 Program of ; :: thesis: for J being 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 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)))))
A2: 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 A3: 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 Lm5, A2;
A5: J c= ((P +* (I ';' J)) +* I) +* J by FUNCT_4:25;
A6: J c= (P +* I) +* J by FUNCT_4:25;
A8: I c= (P +* (I ';' J)) +* I by FUNCT_4:25;
A9: I c= P +* I by FUNCT_4:25;
A11: (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 Th29, A8, A9;
XX: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by Th29, A8, A9;
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 A11, Th29, A5, A6, A3, XX; :: thesis: verum