(from AG01 4.27) (VAR x y) (RULES p(0) -> 0 p(s(x)) -> x le(0,y) -> true le(s(x),0) -> false le(s(x),s(y)) -> le(x,y) minus(x,0) -> x minus(x,s(y)) -> if(le(x,s(y)),0,p(minus(x,p(s(y))))) if(true,x,y) -> x if(false,x,y) -> y )