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,1 c= for-up a,i,n,I
let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT holds Shift I,1 c= for-up a,i,n,I
let i be Integer; :: thesis: for n being Element of NAT holds Shift I,1 c= for-up a,i,n,I
let n be Element of 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:49;
card (Load (a,i >=0_goto ((card I) + 3))) = 1 by SCMPDS_5:6;
hence Shift I,1 c= for-up a,i,n,I by A1, Th16; :: thesis: verum