for P being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA
for I, J being really-closed Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P holds
I ";" J is_halting_on Initialized S,P