let I be Program of ; :: thesis: for a being Int_position

for i being Integer

for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let a be Int_position; :: thesis: for i being Integer

for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let i be Integer; :: thesis: for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let n be Nat; :: thesis: Shift (I,1) c= for-up (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-up (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-up (a,i,n,I) by A1, Th3; :: thesis: verum

for i being Integer

for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let a be Int_position; :: thesis: for i being Integer

for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let i be Integer; :: thesis: for n being Nat holds Shift (I,1) c= for-up (a,i,n,I)

let n be Nat; :: thesis: Shift (I,1) c= for-up (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-up (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-up (a,i,n,I) by A1, Th3; :: thesis: verum