let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
let i be Integer; :: thesis: for I being Program of SCMPDS holds while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
let I be Program of SCMPDS ; :: thesis: 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:51 ; :: thesis: verum