set WHL = while<>0 (a,i,I);
set i1 = (a,i) <>0_goto 2;
set i2 = goto ((card I) + 2);
set PF = (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I;
card ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) = (card (((a,i) <>0_goto 2) ';' (goto ((card I) + 2)))) + (card I) by AFINSQ_1:17
.= 2 + (card I) by SCMP_GCD:5 ;
then ( (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I = ((Load ((a,i) <>0_goto 2)) ';' (Load (goto ((card I) + 2)))) ';' I & (card ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I)) + (- ((card I) + 2)) = 0 ) by SCMPDS_4:def 4;
hence while<>0 (a,i,I) is shiftable by SCMPDS_4:23; :: thesis: verum