let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of
for J being parahalting shiftable Program of holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of
for J being parahalting shiftable Program of holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))
let I be halt-free parahalting Program of ; :: thesis: for J being parahalting shiftable Program of holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))
let J be parahalting shiftable Program of ; :: thesis: LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))
set sI = stop I;
set sIJ = stop (I ';' J);
set s1 = s;
set s2 = s;
set P1 = P +* (stop (I ';' J));
set P2 = P +* (stop I);
A1: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25;
set s3 = Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s));
set P3 = ((P +* (stop (I ';' J))) +* (stop I)) +* (stop J);
set s4 = Initialize (Result ((P +* (stop I)),s));
set P4 = (P +* (stop I)) +* (stop J);
A2: stop I c= P +* (stop I) by FUNCT_4:25;
A3: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
A4: stop J c= ((P +* (stop (I ';' J))) +* (stop I)) +* (stop J) by FUNCT_4:25;
A5: stop I c= (P +* (stop (I ';' J))) +* (stop I) by FUNCT_4:25;
then Initialize (Result ((P +* (stop I)),s)) = Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s)) by A2, Th6;
then A6: LifeSpan ((((P +* (stop (I ';' J))) +* (stop I)) +* (stop J)),(Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s)))) = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))) by A4, A3, Th6;
LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),s) = LifeSpan ((P +* (stop I)),s) by A5, A2, Th6;
hence LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by A1, A6, Lm4; :: thesis: verum