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(),0()) -> 0() 7: -(x8,s(x9)) -> p(-(x8,x9)) 8: -(x10,p(x11)) -> s(-(x10,x11)) 9: -(p(x12),x13) -> p(-(x12,x13)) 10: -(s(x14),x15) -> s(-(x14,x15)) @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(),0()) -> 0() 7: -(x8,s(x9)) -> p(-(x8,x9)) 8: -(x10,p(x11)) -> s(-(x10,x11)) 9: -(p(x12),x13) -> p(-(x12,x13)) 10: -(s(x14),x15) -> s(-(x14,x15)) --- 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(),0()) -> 0() 7: -(x8,s(x9)) -> p(-(x8,x9)) 8: -(x10,p(x11)) -> s(-(x10,x11)) 9: -(p(x12),x13) -> p(-(x12,x13)) 10: -(s(x14),x15) -> s(-(x14,x15))