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