let a be Int_position ; :: thesis: for i being Integer
for n being Element of 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; :: thesis: for n being Element of 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 Element of NAT ; :: thesis: 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 ; :: thesis: 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:15 ; :: thesis: verum