let a be Int_position; :: thesis: for i being Integer

for n being Nat

for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

let i be Integer; :: thesis: for n being Nat

for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

let n be Nat; :: thesis: for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

let I be Program of ; :: thesis: card (for-up (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-up (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-up (a,i,n,I)) = (card I) + 3

let i be Integer; :: thesis: for n being Nat

for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

let n be Nat; :: thesis: for I being Program of holds card (for-up (a,i,n,I)) = (card I) + 3

let I be Program of ; :: thesis: card (for-up (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-up (a,i,n,I)) = ((card I) + 2) + 1 by SCMP_GCD:4

.= (card I) + 3 ;

:: thesis: verum