let I be Program of ; for a being Int_position
for i being Integer holds Shift (I,1) c= while>0 (a,i,I)
let a be Int_position; for i being Integer holds Shift (I,1) c= while>0 (a,i,I)
let i be Integer; Shift (I,1) c= while>0 (a,i,I)
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
A1: while>0 (a,i,I) =
(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)))
by SCMPDS_8:def 3
.=
(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (Load (goto (- ((card I) + 1))))
by SCMPDS_4:def 3
.=
((Load ((a,i) <=0_goto ((card I) + 2))) ';' I) ';' (Load (goto (- ((card I) + 1))))
by SCMPDS_4:def 2
;
card (Load ((a,i) <=0_goto ((card I) + 2))) = 1
by COMPOS_1:54;
hence
Shift (I,1) c= while>0 (a,i,I)
by A1, SCMPDS_7:3; verum