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