We consider the TRS containing the following rules:
f(b) | → | b | (1) |
b | → | h(h(c,f(b)),a) | (2) |
The underlying signature is as follows:
{f/1, b/0, h/2, c/0, a/0}t0 | = | f(b) |
→ | f(h(h(c,f(b)),a)) | |
= | t1 |
t0 | = | f(b) |
→ | b | |
= | t1 |
Automaton 1
final states:
{1}
transitions:
c | → | 5 |
a | → | 2 |
f(3) | → | 4 |
f(7) | → | 1 |
b | → | 3 |
b | → | 4 |
h(5,4) | → | 6 |
h(6,2) | → | 7 |
h(6,2) | → | 3 |
h(6,2) | → | 4 |
Automaton 2
final states:
{8}
transitions:
c | → | 13 |
a | → | 11 |
f(8) | → | 12 |
b | → | 8 |
b | → | 12 |
h(13,12) | → | 14 |
h(14,11) | → | 8 |
h(14,11) | → | 12 |