let a be Int_position; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( (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; :: thesis: ( (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; :: thesis: (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; :: thesis: verum