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