We consider the TRS containing the following rules:
| +(x,y) | → | if(y,x,s(+(x,-(y,s(0))))) | (1) |
| +(x,y) | → | +(y,x) | (2) |
| if(0,y,z) | → | y | (3) |
| if(s(x),y,z) | → | z | (4) |
| if(x,y,y) | → | y | (5) |
| -(x,0) | → | x | (6) |
| -(0,s(y)) | → | 0 | (7) |
| -(s(x),s(y)) | → | -(x,y) | (8) |
The underlying signature is as follows:
{+/2, if/3, s/1, -/2, 0/0}| t0 | = | +(x,y) |
| → | if(y,x,s(+(x,-(y,s(0))))) | |
| → | if(y,x,s(+(-(y,s(0)),x))) | |
| → | if(y,x,s(+(x,-(y,s(0))))) | |
| = | t3 |
| t0 | = | +(x,y) |
| → | +(y,x) | |
| → | if(x,y,s(+(y,-(x,s(0))))) | |
| → | if(x,y,s(+(-(x,s(0)),y))) | |
| = | t3 |