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