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