let a be Int_position; :: thesis: for i being Integer
for n being Nat
for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3
let i be Integer; :: thesis: for n being Nat
for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3
let n be Nat; :: thesis: for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3
let I be Program of ; :: thesis: card (for-down (a,i,n,I)) = (card I) + 3
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
set I4 = ((a,i) <=0_goto ((card I) + 3)) ';' I;
set I5 = (((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)));
card (((a,i) <=0_goto ((card I) + 3)) ';' I) = (card I) + 1 by SCMPDS_6:6;
then card ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) = ((card I) + 1) + 1 by SCMP_GCD:4
.= (card I) + (1 + 1) ;
hence card (for-down (a,i,n,I)) = ((card I) + 2) + 1 by SCMP_GCD:4
.= (card I) + 3 ;
:: thesis: verum