The rewrite relation of the following TRS is considered.
| f(a,empty) | → | g(a,empty) | (1) |
| f(a,cons(x,k)) | → | f(cons(x,a),k) | (2) |
| g(empty,d) | → | d | (3) |
| g(cons(x,k),d) | → | g(k,cons(x,d)) | (4) |
final states:
{0, 1, 2}
transitions:
| empty0 | → | 0 |
| cons0(0,0) | → | 0 |
| f0(0,0) | → | 1 |
| g0(0,0) | → | 2 |
| empty1 | → | 3 |
| g1(0,3) | → | 1 |
| cons1(0,0) | → | 4 |
| f1(4,0) | → | 1 |
| cons1(0,0) | → | 5 |
| g1(0,5) | → | 2 |
| g1(4,3) | → | 1 |
| cons1(0,4) | → | 4 |
| cons1(0,3) | → | 5 |
| g1(0,5) | → | 1 |
| cons1(0,5) | → | 5 |
| cons2(0,3) | → | 6 |
| g2(0,6) | → | 1 |
| g2(4,6) | → | 1 |
| cons1(0,6) | → | 5 |
| cons2(0,6) | → | 6 |
| 0 | → | 2 |
| 3 | → | 1 |
| 5 | → | 2 |
| 5 | → | 1 |
| 6 | → | 1 |