The rewrite relation of the following TRS is considered.
| f(x,x) | → | f(a,b) | (1) |
| b | → | c | (2) |
final states:
{8, 4, 3, 2, 1}
transitions:
| a0 | → | 2 |
| a1 | → | 2 |
| c2 | → | 8 |
| b1 | → | 3 |
| c1 | → | 8 |
| c0 | → | 4 |
| f1(2,3) | → | 1 |
| f1(2,8) | → | 1 |
| b0 | → | 3 |
| f0(1,4) | → | 1 |
| f0(3,2) | → | 1 |
| f0(3,3) | → | 1 |
| f0(2,4) | → | 1 |
| f0(1,1) | → | 1 |
| f0(1,3) | → | 1 |
| f0(8,4) | → | 1 |
| f0(2,8) | → | 1 |
| f0(2,1) | → | 1 |
| f0(4,3) | → | 1 |
| f0(4,8) | → | 1 |
| f0(3,1) | → | 1 |
| f0(1,8) | → | 1 |
| f0(8,1) | → | 1 |
| f0(2,2) | → | 1 |
| f0(8,2) | → | 1 |
| f0(2,3) | → | 1 |
| f0(4,4) | → | 1 |
| f0(1,2) | → | 1 |
| f0(3,8) | → | 1 |
| f0(8,8) | → | 1 |
| f0(4,1) | → | 1 |
| f0(3,4) | → | 1 |
| f0(8,3) | → | 1 |
| f0(4,2) | → | 1 |
| 2 | » | 2 |
| 4 | » | 8 |
| 4 | » | 4 |
| 1 | » | 1 |
| 3 | » | 8 |
| 3 | » | 3 |
| 8 | » | 8 |