for s being State of SCM+FSA
for aa, bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being parahalting MacroInstruction of SCM+FSA holds ProperForUpBody aa,bb,cc,I,s,p by SCMFSA7B:19;