YES 1 decompositions #0 ----------- 1: f(f(g(g(x)))) -> f(a()) 2: g(a()) -> a() 3: f(a()) -> a() 4: f(f(f(x))) -> a() 5: f(f(a())) -> a() @Jouannaud and Kirchner's criterion --- R 1: f(f(g(g(x)))) -> f(a()) 2: g(a()) -> a() 3: f(a()) -> a() 4: f(f(f(x))) -> a() 5: f(f(a())) -> a() --- S 1: f(f(g(g(x)))) -> f(a()) 2: g(a()) -> a() 3: f(a()) -> a() 4: f(f(f(x))) -> a() 5: f(f(a())) -> a()