theorem Th4: :: SFMASTR1:5

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for Ig being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))