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