let I be Program of SCMPDS; :: thesis: for a being Int_position
for i being Integer
for n being 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 Nat holds Shift ((I ';' (AddTo (a,i,(- n)))),1) c= for-down (a,i,n,I)
let i be Integer; :: thesis: for n being Nat holds Shift ((I ';' (AddTo (a,i,(- n)))),1) c= for-down (a,i,n,I)
let n be 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: 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:15
.= ((Load ((a,i) <=0_goto ((card I) + 3))) ';' (I ';' (AddTo (a,i,(- n))))) ';' (goto (- ((card I) + 2))) by SCMPDS_4:def 2
.= ((Load ((a,i) <=0_goto ((card I) + 3))) ';' (I ';' (AddTo (a,i,(- n))))) ';' (Load (goto (- ((card I) + 2)))) by SCMPDS_4:def 3 ;
card (Load ((a,i) <=0_goto ((card I) + 3))) = 1 by COMPOS_1:54;
hence Shift ((I ';' (AddTo (a,i,(- n)))),1) c= for-down (a,i,n,I) by A1, SCMPDS_7:3; :: thesis: verum