YES (VAR x0 x y) (RULES i(h(x0)) -> g(j(h(x0))) g(f(x,x)) -> i(x) f(h(x),y) -> j(h(x)) f(x,h(y)) -> j(x) ) (COMMENT Termination is shown by KBO with weight w0 = 3 w(f) = 0 w(h) = 1 w(j) = 1 w(g) = 1 w(i) = 3 and precedence: h > f > j > i > g )