let I be Program of SCMPDS; :: thesis: for a being Int_position
for i being Integer
for n being Element of NAT holds Shift (I,1) c= for-down (a,i,n,I)
let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT holds Shift (I,1) c= for-down (a,i,n,I)
let i be Integer; :: thesis: for n being Element of NAT holds Shift (I,1) c= for-down (a,i,n,I)
let n be Element of NAT ; :: thesis: Shift (I,1) c= for-down (a,i,n,I)
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
set i3 = goto (- ((card I) + 2));
A1: for-down (a,i,n,I) = ((Load ((a,i) <=0_goto ((card I) + 3))) ';' I) ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2)))) by SCMPDS_4:13;
card (Load ((a,i) <=0_goto ((card I) + 3))) = 1 by COMPOS_1:54;
hence Shift (I,1) c= for-down (a,i,n,I) by A1, Th16; :: thesis: verum