(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}.
)