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 4;
then card PF = (card I) + 1 by SCMPDS_6:15;
then (card PF) + (- ((card I) + 1)) = 0 ;
hence while>0 a,i,I is shiftable by A1, SCMPDS_4:78; :: thesis: verum