YES 1 decompositions #1 ----------- 1: f(f(f(x1))) -> a() 3: f(a()) -> a() 4: f(f(g(g(x2)))) -> f(a()) 6: g(a()) -> a() @Knuth and Bendix' criterion --- R 1: f(f(f(x1))) -> a() 3: f(a()) -> a() 4: f(f(g(g(x2)))) -> f(a()) 6: g(a()) -> a() --- S 1: f(f(f(x1))) -> a() 3: f(a()) -> a() 4: f(f(g(g(x2)))) -> f(a()) 6: g(a()) -> a() NOTE: input TRS is reduced original is 1: f(f(f(x1))) -> a() 2: f(f(a())) -> a() 3: f(a()) -> a() 4: f(f(g(g(x2)))) -> f(a()) 5: g(f(a())) -> a() 6: g(a()) -> a() reduced to 1: f(f(f(x1))) -> a() 3: f(a()) -> a() 4: f(f(g(g(x2)))) -> f(a()) 6: g(a()) -> a()