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