:: deftheorem defines if<0 SCMFSA_X:def 5 :
for a being Int-Location
for I being Program of holds if<0 (a,I) = ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);