:: deftheorem defines while<0 SCMPDS_8:def 2 :
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds while<0 (a,i,I) = (((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));