by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| q0(a(x0)) | → | x(q1(x0)) |
| q1(a(x0)) | → | a(q1(x0)) |
| q1(y(x0)) | → | y(q1(x0)) |
| a(q1(b(x0))) | → | q2(a(y(x0))) |
| a(q2(a(x0))) | → | q2(a(a(x0))) |
| a(q2(y(x0))) | → | q2(a(y(x0))) |
| y(q1(b(x0))) | → | q2(y(y(x0))) |
| y(q2(a(x0))) | → | q2(y(a(x0))) |
| y(q2(y(x0))) | → | q2(y(y(x0))) |
| q2(x(x0)) | → | x(q0(x0)) |
| q0(y(x0)) | → | y(q3(x0)) |
| q3(y(x0)) | → | y(q3(x0)) |
| q3(bl(x0)) | → | bl(q4(x0)) |
| prec(q4) | = | 0 | weight(q4) | = | 1 | ||||
| prec(bl) | = | 0 | weight(bl) | = | 1 | ||||
| prec(q3) | = | 8 | weight(q3) | = | 1 | ||||
| prec(q2) | = | 1 | weight(q2) | = | 1 | ||||
| prec(b) | = | 15 | weight(b) | = | 1 | ||||
| prec(y) | = | 2 | weight(y) | = | 1 | ||||
| prec(x) | = | 0 | weight(x) | = | 1 | ||||
| prec(q1) | = | 3 | weight(q1) | = | 1 | ||||
| prec(q0) | = | 3 | weight(q0) | = | 1 | ||||
| prec(a) | = | 2 | weight(a) | = | 1 |
There are no rules in the TRS. Hence, it is terminating.