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