YES (VAR x y z) (RULES g(x) -> b(f(s(x)),f(x)) u(b(x,0())) -> x u(b(x,s(y))) -> s(u(b(x,y))) f(s(s(z))) -> u(b(f(s(z)),f(z))) p(x,y) -> u(b(x,y)) n(b(x,y)) -> b(u(b(x,y)),x) f(s(0())) -> s(0()) f(0()) -> 0() ) (COMMENT Termination is shown by LPO with precedence: n > p > g > f > u > b > s > 0 )