We consider two TRSs R and S where R contains the rules
| +(x,0) | → | x | (1) |
| +(x,s(y)) | → | s(+(x,y)) | (2) |
| -(0,x) | → | 0 | (3) |
| -(x,0) | → | x | (4) |
| -(s(x),s(y)) | → | -(x,y) | (5) |
and S contains the following rules:
| +(0,y) | → | y | (6) |
| +(s(x),y) | → | s(+(x,y)) | (7) |
| +(x,0) | → | x | (1) |
| +(x,s(y)) | → | s(+(x,y)) | (2) |
The underlying signature is as follows:
{+/2, -/2, 0/0, s/1}