let s be State of SCM+FSA; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting Program of SCM+FSA holds LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))
let J be InitHalting Program of SCM+FSA; :: thesis: LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))
set inI = Initialized I;
set inIJ = Initialized (I ';' J);
set inJ = Initialized J;
A1: ( Initialized J c= (Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J) & Initialized J c= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) ) by FUNCT_4:26;
( s +* (Initialized (I ';' J)),(s +* (Initialized (I ';' J))) +* I equal_outside NAT & s +* (Initialized I),s +* (Initialized (I ';' J)) equal_outside NAT ) by FUNCT_7:132, SCMFSA6A:53;
then A2: s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
A3: ( Initialized I c= s +* (Initialized I) & Initialized I c= (s +* (Initialized (I ';' J))) +* I ) by FUNCT_4:26, SCMFSA6A:52;
then Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))), Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)) equal_outside NAT by A2, Th15;
then Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)), Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) equal_outside NAT by FUNCT_7:28;
then A4: (Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J),(Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) equal_outside NAT by FUNCT_7:106;
Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
then A5: LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J))),((Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J)))) by Th25;
LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = LifeSpan ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)) by A3, A2, Th15;
hence LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J)))) by A5, A1, A4, Th15; :: thesis: verum