We consider the TRS containing the following rules:
| f(x,f(y,z)) | → | f(f(x,y),f(x,z)) | (1) |
| f(f(x,y),z) | → | f(f(x,z),f(y,z)) | (2) |
| f(f(x,y),f(y,z)) | → | y | (3) |
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,f(y,z)) | → | f(f(x,y),f(x,z)) | (1) |
| f(f(x,y),z) | → | f(f(x,z),f(y,z)) | (2) |
| f(f(x,y),f(y,z)) | → | y | (3) |
| f(y,f(y,z)) | → | y | (4) |
| f(f(x,z),z) | → | z | (5) |
All redundant rules that were added or removed can be simulated in 3 steps .
| t0 | = | f(y,f(y,f(y,x378))) |
| → | f(y,y) | |
| = | t1 |
| t0 | = | f(y,f(y,f(y,x378))) |
| → | y | |
| = | t1 |