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:8
.= ((card I) + 1) + 1 by SCMPDS_6:15
.= (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:78; :: thesis: verum