let s be State of SCMPDS ; :: thesis: for I being parahalting No-StopCode Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS holds LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))
let J be parahalting shiftable Program of SCMPDS ; :: thesis: LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))
set sI = stop I;
set IsI = Initialized (stop I);
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set s1 = s +* (Initialized (stop (I ';' J)));
set s2 = s +* (Initialized (stop I));
A1: Initialized (stop (I ';' J)) c= s +* (Initialized (stop (I ';' J))) by FUNCT_4:26;
set IL = NAT ;
set SA0 = Start-At (inspos 0 );
A2: s +* (Initialized (stop (I ';' J))) = (s +* (stop (I ';' J))) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= (s +* (Start-At (inspos 0 ))) +* (stop (I ';' J)) by SCMPDS_4:62 ;
A3: s +* (Initialized (stop I)) = (s +* (stop I)) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= (s +* (Start-At (inspos 0 ))) +* (stop I) by SCMPDS_4:62 ;
(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) = (s +* (Initialized (stop (I ';' J)))) +* (stop I) by FUNCT_4:26, SCMPDS_4:34;
then A4: s +* (Initialized (stop (I ';' J))),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT by AMI_1:120;
A5: s +* (Initialized (stop I)),s +* (Start-At (inspos 0 )) equal_outside NAT by A3, AMI_1:120, FUNCT_7:28;
s +* (Start-At (inspos 0 )),s +* (Initialized (stop (I ';' J))) equal_outside NAT by A2, AMI_1:120;
then s +* (Initialized (stop I)),s +* (Initialized (stop (I ';' J))) equal_outside NAT by A5, FUNCT_7:29;
then A6: s +* (Initialized (stop I)),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT by A4, FUNCT_7:29;
A7: Initialized (stop I) c= (s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) by FUNCT_4:26;
Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
then A8: ( LifeSpan ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) = LifeSpan (s +* (Initialized (stop I))) & Result (s +* (Initialized (stop I))), Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) equal_outside NAT ) by A6, A7, Th21;
set IsJ = Initialized (stop J);
set s3 = (Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J));
set s4 = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J));
A9: (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)),(Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)) equal_outside NAT by A8, FUNCT_7:106;
A10: Initialized (stop J) c= (Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)) by FUNCT_4:26;
Initialized (stop J) c= (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) by FUNCT_4:26;
then LifeSpan ((Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J))) = LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) by A9, A10, Th21;
hence LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) by A1, A8, Lm3; :: thesis: verum