We consider the TRS containing the following rules:
| +(0,y) | → | y | (1) |
| +(s(x),y) | → | s(+(x,y)) | (2) |
| *(0,y) | → | 0 | (3) |
| *(s(x),y) | → | +(*(x,y),y) | (4) |
| *(x,s(y)) | → | +(x,*(x,y)) | (5) |
The underlying signature is as follows:
{+/2, 0/0, s/1, */2}| t0 | = | *(s(x182),s(y)) |
| → | +(*(x182,s(y)),s(y)) | |
| → | +(+(x182,*(x182,y)),s(y)) | |
| = | t2 |
| t0 | = | *(s(x182),s(y)) |
| → | +(s(x182),*(s(x182),y)) | |
| → | +(s(x182),+(*(x182,y),y)) | |
| → | s(+(x182,+(*(x182,y),y))) | |
| = | t3 |