The rewrite relation of the following TRS is considered.
| p(f(f(x))) | → | q(f(g(x))) | (1) |
| p(g(g(x))) | → | q(g(f(x))) | (2) |
| q(f(f(x))) | → | p(f(g(x))) | (3) |
| q(g(g(x))) | → | p(g(f(x))) | (4) |
| f(f(p(x))) | → | g(f(q(x))) | (5) |
| g(g(p(x))) | → | f(g(q(x))) | (6) |
| f(f(q(x))) | → | g(f(p(x))) | (7) |
| g(g(q(x))) | → | f(g(p(x))) | (8) |
final states:
{0, 1, 2, 3}
transitions:
| f0(0) | → | 0 |
| f0(1) | → | 0 |
| f0(2) | → | 0 |
| f0(3) | → | 0 |
| p0(0) | → | 1 |
| p0(1) | → | 1 |
| p0(2) | → | 1 |
| p0(3) | → | 1 |
| g0(0) | → | 2 |
| g0(1) | → | 2 |
| g0(2) | → | 2 |
| g0(3) | → | 2 |
| q0(0) | → | 3 |
| q0(1) | → | 3 |
| q0(2) | → | 3 |
| q0(3) | → | 3 |
| q1(0) | → | 5 |
| f1(5) | → | 4 |
| g1(4) | → | 0 |
| q1(1) | → | 5 |
| q1(2) | → | 5 |
| q1(3) | → | 5 |
| g1(5) | → | 6 |
| f1(6) | → | 2 |
| p1(0) | → | 5 |
| p1(1) | → | 5 |
| p1(2) | → | 5 |
| p1(3) | → | 5 |