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 matchbox @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	0(q0(h(q9(0(1(0(1(x1))))))))
	→	0(q0(0(h(q9(0(1(0(1(x1)))))))))
	→	0(0(q0(h(q9(0(1(0(1(x1)))))))))
	=	t₂

where t₂ = C[t₀σ] and σ = {x1/x1} and C = 0(☐)