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