:: deftheorem defines if<=0 SCMPDS_6:def 10 :
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;