theorem Th11: :: SCMFSA8A:18

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)