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))))
set SA0 = Start-At 0 ,SCMPDS ;
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 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));
A2: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) = (s +* (Initialized (stop (I ';' J)))) +* (stop I) by FUNCT_4:26, SCMPDS_4:34;
then A3: s +* (Initialized (stop (I ';' J))),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT by AMI_1:120;
A4: Initialized (stop J) c= (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) by FUNCT_4:26;
s +* (Initialized (stop I)) = (s +* (stop I)) +* (Start-At 0 ,SCMPDS ) by FUNCT_4:15
.= (s +* (Start-At 0 ,SCMPDS )) +* (stop I) by SCMPDS_4:62 ;
then A5: s +* (Initialized (stop I)),s +* (Start-At 0 ,SCMPDS ) equal_outside NAT by AMI_1:120, FUNCT_7:28;
A6: Initialized (stop J) c= (Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)) by FUNCT_4:26;
s +* (Initialized (stop (I ';' J))) = (s +* (stop (I ';' J))) +* (Start-At 0 ,SCMPDS ) by FUNCT_4:15
.= (s +* (Start-At 0 ,SCMPDS )) +* (stop (I ';' J)) by SCMPDS_4:62 ;
then s +* (Start-At 0 ,SCMPDS ),s +* (Initialized (stop (I ';' J))) equal_outside NAT by AMI_1:120;
then s +* (Initialized (stop I)),s +* (Initialized (stop (I ';' J))) equal_outside NAT by A5, FUNCT_7:29;
then A7: s +* (Initialized (stop I)),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT by A3, FUNCT_7:29;
A8: Initialized (stop I) c= (s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) by FUNCT_4:26;
then Result (s +* (Initialized (stop I))), Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) equal_outside NAT by A7, A2, Th21;
then (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)),(Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)) equal_outside NAT by FUNCT_7:106;
then A9: LifeSpan ((Result ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J))) = LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) by A6, A4, Th21;
LifeSpan ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) = LifeSpan (s +* (Initialized (stop I))) by A7, A8, A2, Th21;
hence LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) by A1, A9, Lm3; :: thesis: verum