set FOR = for-down (a,i,n,I);
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
reconsider PF = ((Load ((a,i) <=0_goto ((card I) + 3))) ';' I) ';' (AddTo (a,i,(- n))) as shiftable Program of ;
card PF = (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 PF) + (- ((card I) + 2)) = 0 ;
hence for-down (a,i,n,I) is shiftable by SCMPDS_4:23; :: thesis: verum