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