let a be Int_position; for i being Integer
for n being Nat
for I being Program of holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let i be Integer; for n being Nat
for I being Program of holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let n be Nat; for I being Program of holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let I be Program of ; ( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = 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));
set I4 = ((a,i) <=0_goto ((card I) + 3)) ';' I;
set I5 = (((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)));
set J6 = (AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2)));
set J5 = I ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2))));
set FLOOP = for-down (a,i,n,I);
for-down (a,i,n,I) = (((a,i) <=0_goto ((card I) + 3)) ';' I) ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2))))
by SCMPDS_4:13;
then
for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' (I ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2)))))
by SCMPDS_4:14;
hence
(for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3)
by SCMPDS_6:7; ( (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
A1:
card (((a,i) <=0_goto ((card I) + 3)) ';' I) = (card I) + 1
by SCMPDS_6:6;
hence
(for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n))
by SCMP_GCD:7; (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2))
card ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) =
((card I) + 1) + 1
by A1, SCMP_GCD:4
.=
(card I) + (1 + 1)
;
hence
(for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2))
by SCMP_GCD:6; verum