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