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 ';' (AddTo a,i,(- n))),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 ';' (AddTo a,i,(- n))),1 c= for-down a,i,n,I
let i be Integer; :: thesis: for n being Element of NAT holds Shift (I ';' (AddTo a,i,(- n))),1 c= for-down a,i,n,I
let n be Element of NAT ; :: thesis: Shift (I ';' (AddTo a,i,(- n))),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: card (Load (a,i <=0_goto ((card I) + 3))) = 1 by SCMPDS_5:6;
for-down a,i,n,I = (((a,i <=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2))) by SCMPDS_7:def 2
.= ((a,i <=0_goto ((card I) + 3)) ';' (I ';' (AddTo a,i,(- n)))) ';' (goto (- ((card I) + 2))) by SCMPDS_4:51
.= ((Load (a,i <=0_goto ((card I) + 3))) ';' (I ';' (AddTo a,i,(- n)))) ';' (goto (- ((card I) + 2))) by SCMPDS_4:def 4
.= ((Load (a,i <=0_goto ((card I) + 3))) ';' (I ';' (AddTo a,i,(- n)))) ';' (Load (goto (- ((card I) + 2)))) by SCMPDS_4:def 5 ;
hence Shift (I ';' (AddTo a,i,(- n))),1 c= for-down a,i,n,I by A1, SCMPDS_7:16; :: thesis: verum