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 SCMPDS_4:45
.= 2 + (card I) by SCMP_GCD:9 ;
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 6;
hence while<>0 a,i,I is shiftable by SCMPDS_4:78; :: thesis: verum