let s be State of SCMPDS ; :: thesis: for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)))
set SA0 = Start-At 0 ,SCMPDS ;
let I be halt-free parahalting Program of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS holds LifeSpan (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)))
let J be parahalting shiftable Program of SCMPDS ; :: thesis: LifeSpan (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)))
set sI = stop I;
set sIJ = stop (I ';' J);
set s1 = (Initialize s) +* (stop (I ';' J));
set s2 = (Initialize s) +* (stop I);
I1: (Initialize s) +* (stop (I ';' J)) = s +* (Initialize (stop (I ';' J))) by SCMPDS_4:5;
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
A1: Initialize (stop (I ';' J)) c= (Initialize s) +* (stop (I ';' J)) by I1, FUNCT_4:26;
set s3 = (Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J);
set s4 = (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J);
I5: (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Initialize (stop J)) = (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J) by SCMPDS_4:5;
I3: (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (Initialize (stop J)) = (Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J) by SCMPDS_4:5;
A2: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
I4: ((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop I)) = (Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) by SCMPDS_4:5;
(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) = ((Initialize s) +* (stop (I ';' J))) +* (stop I) by I1, FUNCT_4:26, SCMPDS_4:34;
then A3: (Initialize s) +* (stop (I ';' J)),(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) equal_outside NAT by FUNCT_7:132;
A4: Initialize (stop J) c= (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J) by I5, FUNCT_4:26;
A5: (Initialize s) +* (stop I),s +* (Start-At 0 ,SCMPDS ) equal_outside NAT by FUNCT_7:28, FUNCT_7:132;
A6: Initialize (stop J) c= (Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J) by I3, FUNCT_4:26;
s +* (Start-At 0 ,SCMPDS ),(Initialize s) +* (stop (I ';' J)) equal_outside NAT by FUNCT_7:132;
then (Initialize s) +* (stop I),(Initialize s) +* (stop (I ';' J)) equal_outside NAT by A5, FUNCT_7:29;
then A7: (Initialize s) +* (stop I),((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop I)) equal_outside NAT by A3, I4, FUNCT_7:29;
A8: Initialize (stop I) c= (Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) by I4, FUNCT_4:26;
then Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)), Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)) equal_outside NAT by A7, A2, Th21, I4;
then (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J),(Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J) equal_outside NAT by I3, I5, FUNCT_7:106;
then A9: LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)))) +* (stop J)) = LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) by A6, A4, Th21;
LifeSpan (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)) = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) by A7, A8, A2, Th21, I4;
hence LifeSpan (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) by A1, A9, Lm3; :: thesis: verum