We consider two TRSs R and S where R contains the rules
| b | → | f(a) | (1) |
| a | → | c | (2) |
| a | → | a | (3) |
| h(c,f(f(f(a)))) | → | h(f(f(c)),h(b,a)) | (4) |
| f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b))))))) | → | c | (5) |
and S contains the following rules:
| a1 | → | b1 | (6) |
| a1 | → | c1 | (7) |
| b1 | → | b2 | (8) |
| c1 | → | c2 | (9) |
| a2 | → | b2 | (10) |
| a2 | → | c2 | (11) |
| b2 | → | b3 | (12) |
| c2 | → | c3 | (13) |
| a3 | → | b3 | (14) |
| a3 | → | c3 | (15) |
| b3 | → | b4 | (16) |
| c3 | → | c4 | (17) |
| a4 | → | b4 | (18) |
| a4 | → | c4 | (19) |
| b4 | → | b5 | (20) |
| c4 | → | c5 | (21) |
| a5 | → | b5 | (22) |
| a5 | → | c5 | (23) |
| b5 | → | b6 | (24) |
| c5 | → | c6 | (25) |
| a6 | → | b6 | (26) |
| a6 | → | c6 | (27) |
| b6 | → | b7 | (28) |
| c6 | → | b7 | (29) |
| b7 | → | b1 | (30) |
| b7 | → | c1 | (31) |
The underlying signature is as follows:
{a/0, b/0, c/0, f/1, h/2, a1/0, a2/0, a3/0, a4/0, a5/0, a6/0, b1/0, b2/0, b3/0, b4/0, b5/0, b6/0, b7/0, c1/0, c2/0, c3/0, c4/0, c5/0, c6/0}