:: deftheorem defines if=0 SCMFSA_X:def 1 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds if=0 (a,I) = (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);