(VAR x y) (RULES leq(0, y) -> true leq(s(x), 0) -> false leq(s(x),s(y)) -> leq(x, y) if(true, x, y) -> x if(false, x, y) -> y -(x, 0) -> x -(s(x), s(y)) -> -(x, y) mod(0,y) -> 0 mod(s(x),0) -> 0 mod(s(x),s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)),s(x)) ) (COMMENT Modified Example 4.30 (third TRS) in \cite{AG01}. )