let a be Int_position; for i being Integer
for I being Program of holds while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
let i be Integer; for I being Program of holds while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
let I be Program of ; while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
thus 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 ';' (goto (- ((card I) + 1))))
by SCMPDS_4:15
; verum