(VAR Y X) (RULES minus(0,Y) -> 0 minus(s(X),s(Y)) -> minus(X,Y) geq(X,0) -> true geq(0,s(Y)) -> false geq(s(X),s(Y)) -> geq(X,Y) div(0,s(Y)) -> 0 div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) if(true,X,Y) -> X if(false,X,Y) -> Y )