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));
A1: card ((a,i <>0_goto 2) ';' (goto ((card I) + 2))) = 2 by SCMP_GCD:9;
while<>0 a,i,I = (((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (Load (goto (- ((card I) + 2)))) by SCMPDS_4:def 5;
hence Shift I,2 c= while<>0 a,i,I by A1, SCMPDS_7:16; :: thesis: verum