:: deftheorem defines for-up SCMPDS_7:def 1 :
for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds for-up (a,i,n,I) = ((((a,i) >=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)));