let s be State of SCM+FSA; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting 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))))
set SA0 = Start-At (0,SCM+FSA);
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for J being parahalting 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 parahalting 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))))
( 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 A1: s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
then A2: 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 Lm4;
A3: ( J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I))) +* (Initialized J) & J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) ) by Th8, FUNCT_4:26;
Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
then A4: I +* (Start-At (0,SCM+FSA)) c= (s +* (Initialized (I ';' J))) +* I by Th8;
A5: I +* (Start-At (0,SCM+FSA)) c= s +* (Initialized I) by Th8, FUNCT_4:26;
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 A4, A1, Th29;
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 A6: (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;
LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = LifeSpan ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)) by A5, A4, A1, Th29;
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 A2, A3, A6, Th29; :: thesis: verum