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; verum