let a be Int_position; for i being Integer
for n being Nat
for I being Program of SCMPDS holds for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
let i be Integer; for n being Nat
for I being Program of SCMPDS holds for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
let n be Nat; for I being Program of SCMPDS holds for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
let I be Program of SCMPDS; for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
set i3 = goto (- ((card I) + 2));
thus for-down (a,i,n,I) =
((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2)))
by SCMPDS_7:def 2
.=
((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
by SCMPDS_7:2
; verum