theorem Th17: :: SCMFSA6B:19

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting keeping_0 Program of
for J being really-closed parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))