let s be 0 -started State of SCMPDS; for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J)))) = (LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (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 +* (stop (I ';' J)))),(s +* (stop (I ';' J)))) = (LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))))
let J be parahalting shiftable Program of SCMPDS; LifeSpan ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J)))) = (LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))))
set sI = stop I;
set sIJ = stop (I ';' J);
set s1 = s +* (stop (I ';' J));
set s2 = s +* (stop I);
A1:
stop (I ';' J) c= s +* (stop (I ';' J))
by FUNCT_4:26;
set s3 = (Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))))) +* (stop J);
set s4 = (Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J);
A2:
stop I c= s +* (stop I)
by FUNCT_4:26;
A3:
s +* (stop (I ';' J)),(s +* (stop (I ';' J))) +* (stop I) equal_outside NAT
by FUNCT_7:132;
A4:
stop J c= (Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J)
by FUNCT_4:26;
A5:
s +* (stop I),s equal_outside NAT
by FUNCT_7:28, FUNCT_7:132;
A6:
stop J c= (Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))))) +* (stop J)
by FUNCT_4:26;
s,s +* (stop (I ';' J)) equal_outside NAT
by FUNCT_7:132;
then
s +* (stop I),s +* (stop (I ';' J)) equal_outside NAT
by A5, FUNCT_7:29;
then A7:
s +* (stop I),(s +* (stop (I ';' J))) +* (stop I) equal_outside NAT
by A3, FUNCT_7:29;
A8:
stop I c= (s +* (stop (I ';' J))) +* (stop I)
by FUNCT_4:26;
then
Result ((ProgramPart (s +* (stop I))),(s +* (stop I))), Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))) equal_outside NAT
by A7, A2, Th21;
then
Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I)))), Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I)))) equal_outside NAT
by COMPOS_1:81;
then
(Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J),(Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))))) +* (stop J) equal_outside NAT
by FUNCT_7:106;
then A9:
LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))))) +* (stop J))) = LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J)))
by A6, A4, Th21;
LifeSpan ((ProgramPart ((s +* (stop (I ';' J))) +* (stop I))),((s +* (stop (I ';' J))) +* (stop I))) = LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))
by A7, A8, A2, Th21;
hence
LifeSpan ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J)))) = (LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart (s +* (stop I))),(s +* (stop I))))) +* (stop J))))
by A1, A9, Lm3; verum