The rewrite relation of the following TRS is considered.
| f(f(x,a),a) | → | f(f(f(a,a),f(x,a)),a) | (1) |
final states:
{2, 1}
transitions:
| a1 | → | 4 |
| f1(1,4) | → | 5 |
| f1(2,4) | → | 5 |
| f1(6,1) | → | 7 |
| f1(7,4) | → | 1 |
| f1(7,4) | → | 5 |
| f1(4,4) | → | 6 |
| f1(6,5) | → | 7 |
| a0 | → | 2 |
| a2 | → | 16 |
| f0(1,2) | → | 1 |
| f0(2,1) | → | 1 |
| f0(1,1) | → | 1 |
| f0(2,2) | → | 1 |
| f2(18,17) | → | 19 |
| f2(7,16) | → | 17 |
| f2(19,16) | → | 5 |
| f2(16,16) | → | 18 |