(VAR x y v u) (RULES diff(x, y) -> cond1(equal(x, y), x, y) cond1(true, x, y) -> 0 cond1(false, x, y) -> cond2(gt(x, y), x, y) cond2(true, x, y) -> s(diff(x, s(y))) cond2(false, x, y) -> s(diff(s(x), y)) gt(0, v) -> false gt(s(u), 0) -> true gt(s(u), s(v)) -> gt(u, v) equal(0, 0) -> true equal(s(x), 0) -> false equal(0, s(y)) -> false equal(s(x), s(y)) -> equal(x, y) )