set WHL = while<0 (a,i,I);
set i1 = (a,i) >=0_goto ((card I) + 2);
set PF = (Load ((a,i) >=0_goto ((card I) + 2))) ';' I;
A1: (Load ((a,i) >=0_goto ((card I) + 2))) ';' I = ((a,i) >=0_goto ((card I) + 2)) ';' I by SCMPDS_4:def 2;
then card ((Load ((a,i) >=0_goto ((card I) + 2))) ';' I) = (card I) + 1 by SCMPDS_6:6;
then (card ((Load ((a,i) >=0_goto ((card I) + 2))) ';' I)) + (- ((card I) + 1)) = 0 ;
hence while<0 (a,i,I) is shiftable by A1, SCMPDS_4:23; :: thesis: verum