theorem Th8: :: SCM_HALT:10

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p & p halts_on s holds
for m being Nat st m <= LifeSpan (p,s) holds
Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)