theorem Th16: :: SCM_HALT:18

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