let I be Program of ; for a being Int_position
for i being Integer
for n being Nat holds Shift (I,1) c= for-down (a,i,n,I)
let a be Int_position; for i being Integer
for n being Nat holds Shift (I,1) c= for-down (a,i,n,I)
let i be Integer; for n being Nat holds Shift (I,1) c= for-down (a,i,n,I)
let n be Nat; 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, Th3; verum