theorem Th11: :: SCM_HALT:13

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