theorem Th10: :: SCMFSA8A:17

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Nat st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )