theorem Th15: :: SCM_HALT:17

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