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