YES 1 decompositions #1 ----------- 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x2,x3) -> h(k1(x2),k2(x3)) 3: k1(a()) -> c() 4: k2(b()) -> d() @Knuth and Bendix' criterion --- R 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x2,x3) -> h(k1(x2),k2(x3)) 3: k1(a()) -> c() 4: k2(b()) -> d() --- S 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x2,x3) -> h(k1(x2),k2(x3)) 3: k1(a()) -> c() 4: k2(b()) -> d() NOTE: input TRS is reduced original is 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x2,x3) -> h(k1(x2),k2(x3)) 3: k1(a()) -> c() 4: k2(b()) -> d() 5: f(h(k1(a()),k2(b()))) -> f(h(c(),d())) 6: f(h(c(),k2(b()))) -> f(h(c(),d())) 7: f(h(k1(a()),d())) -> f(h(c(),d())) reduced to 1: f(g(x1,a(),b())) -> x1 2: g(f(h(c(),d())),x2,x3) -> h(k1(x2),k2(x3)) 3: k1(a()) -> c() 4: k2(b()) -> d()