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