:: deftheorem defines if>0 SCMFSA_X:def 2 :
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);