:: deftheorem defines if<0 SCMPDS_6:def 6 :
for a being Int_position
for k being Integer
for I, J being Program of holds if<0 (a,k,I,J) = ((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;