let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting 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 InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting 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 InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting 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 InitHalting 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)))))
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:26;
A2: ( J c= ((p +* (I ';' J)) +* I) +* J & J c= (p +* I) +* J ) by FUNCT_4:26;
A3: NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (s +* (Initialize ((intloc 0) .--> 1))) ;
A4: ( Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) ) by FUNCT_4:26;
A5: ( I c= p +* I & I c= (p +* (I ';' J)) +* I ) by FUNCT_4:26;
then NPP (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) by A3, Th15, A4;
then NPP (Result (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) ;
then A6: 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;
A7: 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 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, A3, Th15, A5;
hence 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 A8, A1, A6, Th15, A2; :: thesis: verum