theorem Th13: :: SCMFSA6B:15

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA