let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA 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 SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA 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 SCM+FSA; :: 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: NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (s +* (Initialize ((intloc 0) .--> 1))) ;
A2: I ';' J c= P +* (I ';' J) by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
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;
B4: ( 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:26;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then A4: ( Start-At (0,SCM+FSA) c= (Result (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) & Start-At (0,SCM+FSA) c= (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) ) by B4, XBOOLE_1:1;
A5: J c= ((P +* (I ';' J)) +* I) +* J by FUNCT_4:26;
uu: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
A6: J c= (P +* I) +* J by FUNCT_4:26;
A8: I c= (P +* (I ';' J)) +* I by FUNCT_4:26;
A9: I c= P +* I by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A10: Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1)) by uu, XBOOLE_1:1;
then NPP (Result (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) by A1, Th29, A8, A9;
then A11: NPP ((Result (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) = NPP ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) by COMPOS_1:235;
XX: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((P +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by A10, A1, 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 A4, A11, Th29, A5, A6, A3, XX; :: thesis: verum