We consider two TRSs R and S where R contains the rules
| a | → | a | (1) |
| f(h(a,a)) | → | f(b) | (2) |
| c | → | b | (3) |
and S contains the following rules:
| f(h(a,c)) | → | h(f(b),h(c,h(c,h(f(h(b,b)),a)))) | (4) |
| h(h(h(f(b),c),b),h(a,h(a,c))) | → | h(f(b),h(c,b)) | (5) |
| a | → | h(h(b,b),b) | (6) |
| c | → | a | (7) |
The underlying signature is as follows:
{a/0, b/0, c/0, f/1, h/2}| t0 | = | f(h(a,a)) |
| →S | f(h(h(h(b,b),b),a)) | |
| = | s1 |
| t0 | = | f(h(a,a)) |
| →R | f(b) | |
| = | t1 |