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