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