r(X,Y,Q,R) = { ( X, Y, X/Y, X mod Y ) | X >= 0 and Y > 0 }
( X,Y,Q,R := X,Y,0,X ) o
[while R>=Y do must "guess" loop function f
Q := Q + 1 Let's try
R := R - Y ( R < Y --> ident )
end] | ( R >= Y and Y > 0 -->
Q,R := Q+R/Y, R mod Y )
