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