theorem Th12: :: SCM_HALT:14

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st p +* I halts_on Initialized s holds
for J being Program of SCM+FSA
for k being Nat st k <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),k) = Comput ((p +* (I ";" J)),(Initialized s),k)