We consider the TRS containing the following rules:
| sq(0(x)) | → | p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x))))))))))))))))) | (1) |
| sq(s(x)) | → | s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x))))))))))))))))))))))))))))))))) | (2) |
| twice(0(x)) | → | p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x))))))))))))))))))))))))))) | (3) |
| twice(s(x)) | → | p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x))))))))))))))) | (4) |
| p(p(s(x))) | → | p(x) | (5) |
| p(s(x)) | → | x | (6) |
| p(0(x)) | → | 0(s(s(s(s(s(s(s(s(s(s(s(x)))))))))))) | (7) |
| 0(x) | → | x | (8) |
The underlying signature is as follows:
{sq/1, 0/1, p/1, s/1, twice/1}| t0 | = | p(0(f5)) |
| → | p(f5) | |
| = | t1 |
| t0 | = | p(0(f5)) |
| → | 0(s(s(s(s(s(s(s(s(s(s(s(f5)))))))))))) | |
| = | t1 |
Automaton 1
final states:
{1}
transitions:
| f5 | → | 2 |
| p(2) | → | 1 |
Automaton 2
final states:
{3}
transitions:
| 15 | → | 3 |
| f5 | → | 4 |
| s(13) | → | 14 |
| s(14) | → | 15 |
| s(10) | → | 11 |
| s(8) | → | 9 |
| s(4) | → | 5 |
| s(5) | → | 6 |
| s(11) | → | 12 |
| s(9) | → | 10 |
| s(6) | → | 7 |
| s(12) | → | 13 |
| s(7) | → | 8 |
| 0(15) | → | 3 |