Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/turing_copy)

The rewrite relation of the following TRS is considered.

0(q0(0(x1))) 0(0(q0(x1))) (1)
0(q0(h(x1))) 0(0(q0(h(x1)))) (2)
0(q0(1(x1))) 0(1(q0(x1))) (3)
1(q0(0(x1))) 0(0(q1(x1))) (4)
1(q0(h(x1))) 0(0(q1(h(x1)))) (5)
1(q0(1(x1))) 0(1(q1(x1))) (6)
1(q1(0(x1))) 1(0(q1(x1))) (7)
1(q1(h(x1))) 1(0(q1(h(x1)))) (8)
1(q1(1(x1))) 1(1(q1(x1))) (9)
0(q1(0(x1))) 0(0(q2(x1))) (10)
0(q1(h(x1))) 0(0(q2(h(x1)))) (11)
0(q1(1(x1))) 0(1(q2(x1))) (12)
1(q2(0(x1))) 1(0(q2(x1))) (13)
1(q2(h(x1))) 1(0(q2(h(x1)))) (14)
1(q2(1(x1))) 1(1(q2(x1))) (15)
0(q2(x1)) q3(1(x1)) (16)
1(q3(x1)) q3(1(x1)) (17)
0(q3(x1)) q4(0(x1)) (18)
1(q4(x1)) q4(1(x1)) (19)
0(q4(0(x1))) 1(0(q5(x1))) (20)
0(q4(h(x1))) 1(0(q5(h(x1)))) (21)
0(q4(1(x1))) 1(1(q5(x1))) (22)
1(q5(0(x1))) 0(0(q1(x1))) (23)
1(q5(h(x1))) 0(0(q1(h(x1)))) (24)
1(q5(1(x1))) 0(1(q1(x1))) (25)
h(q0(x1)) h(0(q0(x1))) (26)
h(q1(x1)) h(0(q1(x1))) (27)
h(q2(x1)) h(0(q2(x1))) (28)
h(q3(x1)) h(0(q3(x1))) (29)
h(q4(x1)) h(0(q4(x1))) (30)
h(q5(x1)) h(0(q5(x1))) (31)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = 0(q0(h(x1)))
0(0(q0(h(x1))))
= t1
where t1 = C[t0σ] and σ = {x1/x1} and C = 0()