for s being 0 -started State of SCM+FSA
for I being really-closed Program of
for J being Program of
for P being Instruction-Sequence of SCM+FSA st 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)