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 4;
then card ((Load (a,i >=0_goto ((card I) + 2))) ';' I) = (card I) + 1 by SCMPDS_6:15;
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:78; :: thesis: verum