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