let s be State of SCMPDS ; for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))) = (LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J))))
set SA0 = Start-At 0 ,SCMPDS ;
let I be halt-free parahalting Program of SCMPDS ; for J being parahalting shiftable Program of SCMPDS holds LifeSpan (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))) = (LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J))))
let J be parahalting shiftable Program of SCMPDS ; LifeSpan (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))) = (LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart (s +* (Initialized (stop I)))),(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 (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J));
set s4 = (Result (ProgramPart (s +* (Initialized (stop I)))),(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 FUNCT_7:132;
A4:
Initialized (stop J) c= (Result (ProgramPart (s +* (Initialized (stop I)))),(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 FUNCT_7:28, FUNCT_7:132;
A6:
Initialized (stop J) c= (Result (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((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 FUNCT_7:132;
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 (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))), Result (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) equal_outside NAT
by A7, A2, Th21;
then
(Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)),(Result (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)) equal_outside NAT
by FUNCT_7:106;
then A9:
LifeSpan (ProgramPart ((Result (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))) +* (Initialized (stop J))) = LifeSpan (ProgramPart ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))
by A6, A4, Th21;
LifeSpan (ProgramPart ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)))),((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) = LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))
by A7, A8, A2, Th21;
hence
LifeSpan (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))) = (LifeSpan (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J)))),((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (Initialized (stop J))))
by A1, A9, Lm3; verum