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

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