Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/turing_mult)

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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

0 q0 0 h+ 0 0 q0 0 h ε

The derivation can be derived as follows.