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