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 matchbox @ termCOMP 2023)
1 Loop
The following loop proves nontermination.
| t0
|
= |
0(q0(h(1(0(q5(1(x1))))))) |
|
→
|
0(0(q0(h(1(0(q5(1(x1)))))))) |
|
= |
t1
|
where t1 =
C[t0σ]
and
σ =
{x1/x1}
and
C = 0(☐)