set FOR = for-up (a,i,n,I);
set i1 = (a,i) >=0_goto ((card I) + 3);
set i2 = AddTo (a,i,n);
set PF = ((Load ((a,i) >=0_goto ((card I) + 3))) ';' I) ';' (AddTo (a,i,n));
card (((Load ((a,i) >=0_goto ((card I) + 3))) ';' I) ';' (AddTo (a,i,n))) = (card (((a,i) >=0_goto ((card I) + 3)) ';' I)) + 1 by SCMP_GCD:4
.= ((card I) + 1) + 1 by SCMPDS_6:6
.= (card I) + (1 + 1) ;
then (card (((Load ((a,i) >=0_goto ((card I) + 3))) ';' I) ';' (AddTo (a,i,n)))) + (- ((card I) + 2)) = 0 ;
hence for-up (a,i,n,I) is shiftable by SCMPDS_4:23; :: thesis: verum