YES 3 decompositions #1 ----------- 1: F(x1,x2) -> c(A()) #2 ----------- 2: G(x3) -> x3 #3 ----------- 3: h(x4) -> c(x4) @Knuth and Bendix' criterion --- R 1: F(x1,x2) -> c(A()) --- S 1: F(x1,x2) -> c(A()) @Knuth and Bendix' criterion --- R 2: G(x3) -> x3 --- S 2: G(x3) -> x3 @Knuth and Bendix' criterion --- R 3: h(x4) -> c(x4) --- S 3: h(x4) -> c(x4)