The rewrite relation of the following TRS is considered.
| 0(q0(0(x1))) | → | 0(0(q0(x1))) | (1) |
| 0(q0(1(x1))) | → | 0(1(q0(x1))) | (2) |
| 1(q0(0(x1))) | → | 0(0(q1(x1))) | (3) |
| 1(q0(1(x1))) | → | 0(1(q1(x1))) | (4) |
| 1(q1(0(x1))) | → | 1(0(q1(x1))) | (5) |
| 1(q1(1(x1))) | → | 1(1(q1(x1))) | (6) |
| 0(q1(0(x1))) | → | 0(0(q2(x1))) | (7) |
| 0(q1(1(x1))) | → | 0(1(q2(x1))) | (8) |
| 1(q2(0(x1))) | → | 1(0(q2(x1))) | (9) |
| 1(q2(1(x1))) | → | 1(1(q2(x1))) | (10) |
| 0(q2(x1)) | → | q3(1(x1)) | (11) |
| 1(q3(x1)) | → | q3(1(x1)) | (12) |
| 0(q3(x1)) | → | q4(0(x1)) | (13) |
| 1(q4(x1)) | → | q4(1(x1)) | (14) |
| 0(q4(0(x1))) | → | 1(0(q5(x1))) | (15) |
| 0(q4(1(x1))) | → | 1(1(q5(x1))) | (16) |
| 1(q5(0(x1))) | → | 0(0(q1(x1))) | (17) |
| 1(q5(1(x1))) | → | 0(1(q1(x1))) | (18) |
| 0(q5(x1)) | → | q6(0(x1)) | (19) |
| 1(q6(x1)) | → | q6(1(x1)) | (20) |
| 1(q7(0(x1))) | → | 0(0(q8(x1))) | (21) |
| 1(q7(1(x1))) | → | 0(1(q8(x1))) | (22) |
| 0(q8(x1)) | → | 0(q0(x1)) | (23) |
| 1(q8(0(x1))) | → | 1(0(q8(x1))) | (24) |
| 1(q8(1(x1))) | → | 1(1(q8(x1))) | (25) |
| 0(q6(x1)) | → | q9(0(x1)) | (26) |
| 0(q9(0(x1))) | → | 1(0(q7(x1))) | (27) |
| 0(q9(1(x1))) | → | 1(1(q7(x1))) | (28) |
| 1(q9(x1)) | → | q9(1(x1)) | (29) |
| h(q0(x1)) | → | h(0(q0(x1))) | (30) |
| q0(h(x1)) | → | q0(0(h(x1))) | (31) |
| h(q1(x1)) | → | h(0(q1(x1))) | (32) |
| q1(h(x1)) | → | q1(0(h(x1))) | (33) |
| h(q2(x1)) | → | h(0(q2(x1))) | (34) |
| q2(h(x1)) | → | q2(0(h(x1))) | (35) |
| h(q3(x1)) | → | h(0(q3(x1))) | (36) |
| q3(h(x1)) | → | q3(0(h(x1))) | (37) |
| h(q4(x1)) | → | h(0(q4(x1))) | (38) |
| q4(h(x1)) | → | q4(0(h(x1))) | (39) |
| h(q5(x1)) | → | h(0(q5(x1))) | (40) |
| q5(h(x1)) | → | q5(0(h(x1))) | (41) |
| h(q6(x1)) | → | h(0(q6(x1))) | (42) |
| q6(h(x1)) | → | q6(0(h(x1))) | (43) |
There is a looping derivation.
0 q0 0 h →+ 0 0 q0 0 h ε
The derivation can be derived as follows.