set i = (a,k1) <=0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
(I ';' (Goto ((card J) + 1))) ';' J = (I ';' (Load (goto ((card J) + 1)))) ';' J by SCMPDS_6:def 1;
then reconsider IJ = (I ';' (Goto ((card J) + 1))) ';' J as shiftable Program of ;
if>0 (a,k1,I,J) = ((((a,k1) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J by SCMPDS_6:def 5
.= (((a,k1) <=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J by SCMPDS_4:14
.= ((a,k1) <=0_goto ((card I) + 2)) ';' IJ by SCMPDS_4:14
.= (Load ((a,k1) <=0_goto ((card I) + 2))) ';' IJ by SCMPDS_4:def 2 ;
hence if>0 (a,k1,I,J) is shiftable ; :: thesis: verum