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 SCMPDS ;
card PF = (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 PF) + (- ((card I) + 2)) = 0 ;
hence for-down a,i,n,I is shiftable by SCMPDS_4:78; :: thesis: verum