We consider the TRS containing the following rules:
| f(x,x) | → | g(x) | (1) |
| f(x,g(x)) | → | b | (2) |
| h(c,y) | → | f(h(y,c),h(y,y)) | (3) |
The underlying signature is as follows:
{f/2, g/1, b/0, h/2, c/0}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| f(x,x) | → | g(x) | (1) |
| f(x,g(x)) | → | b | (2) |
| h(c,y) | → | f(h(y,c),h(y,y)) | (3) |
| h(c,c) | → | g(h(c,c)) | (4) |
| f(x,f(x,x)) | → | b | (5) |
All redundant rules that were added or removed can be simulated in 3 steps .
| t0 | = | h(c,c) |
| → | f(h(c,c),h(c,c)) | |
| → | f(h(c,c),g(h(c,c))) | |
| → | b | |
| = | t3 |
| t0 | = | h(c,c) |
| → | g(h(c,c)) | |
| → | g(g(h(c,c))) | |
| → | g(g(g(h(c,c)))) | |
| = | t3 |