theorem Th32: :: SCMPDS_7:34

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)) . 0 = (a,i) >=0_goto ((card I) + 3) & (for-up (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,n) & (for-up (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )