let I be Program of SCMPDS; :: thesis: for a being Int_position
for i being Integer holds Shift (I,2) c= while<>0 (a,i,I)
let a be Int_position; :: thesis: for i being Integer holds Shift (I,2) c= while<>0 (a,i,I)
let i be Integer; :: thesis: Shift (I,2) c= while<>0 (a,i,I)
set i1 = (a,i) <>0_goto 2;
set i2 = goto ((card I) + 2);
set i3 = goto (- ((card I) + 2));
( card (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) = 2 & while<>0 (a,i,I) = ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (Load (goto (- ((card I) + 2)))) ) by SCMPDS_4:def 3, SCMP_GCD:5;
hence Shift (I,2) c= while<>0 (a,i,I) by SCMPDS_7:3; :: thesis: verum