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:52
.= (a,i <>0_goto 2) ';' (((goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 2)))) by SCMPDS_4:51 ; :: thesis: verum