YES 1 decompositions #1 ----------- 1: s(p(x1)) -> x1 2: p(s(x2)) -> x2 3: +(x3,0()) -> x3 4: +(x4,s(x5)) -> s(+(x4,x5)) 5: +(x6,p(x7)) -> p(+(x6,x7)) 6: +(0(),x8) -> x8 7: +(p(x9),x10) -> p(+(x9,x10)) 8: +(s(x11),x12) -> s(+(x11,x12)) @Knuth and Bendix' criterion --- R 1: s(p(x1)) -> x1 2: p(s(x2)) -> x2 3: +(x3,0()) -> x3 4: +(x4,s(x5)) -> s(+(x4,x5)) 5: +(x6,p(x7)) -> p(+(x6,x7)) 6: +(0(),x8) -> x8 7: +(p(x9),x10) -> p(+(x9,x10)) 8: +(s(x11),x12) -> s(+(x11,x12)) --- S 1: s(p(x1)) -> x1 2: p(s(x2)) -> x2 3: +(x3,0()) -> x3 4: +(x4,s(x5)) -> s(+(x4,x5)) 5: +(x6,p(x7)) -> p(+(x6,x7)) 6: +(0(),x8) -> x8 7: +(p(x9),x10) -> p(+(x9,x10)) 8: +(s(x11),x12) -> s(+(x11,x12))