YES 1 decompositions #1 ----------- 1: h(c(),c()) -> h(b(),f(b())) 2: f(h(a(),h(c(),a()))) -> c() 3: h(c(),b()) -> f(a()) @Knuth and Bendix' criterion --- R 1: h(c(),c()) -> h(b(),f(b())) 2: f(h(a(),h(c(),a()))) -> c() 3: h(c(),b()) -> f(a()) --- S 1: h(c(),c()) -> h(b(),f(b())) 2: f(h(a(),h(c(),a()))) -> c() 3: h(c(),b()) -> f(a())