Certification Problem
Input (TPDB TRS_Relative/Relative_05/rtL-evo)
The relative rewrite relation R/S is considered where R is the following TRS
|
top(U(x,y)) |
→ |
top(check(D(x,y))) |
(1) |
|
D(x,B) |
→ |
U(x,B) |
(2) |
|
F(x,U(O(y),z)) |
→ |
U(x,F(y,z)) |
(3) |
|
F(x,U(N(y),z)) |
→ |
U(x,F(y,z)) |
(4) |
|
D(O(x),F(y,z)) |
→ |
F(x,D(y,z)) |
(5) |
|
D(N(x),F(y,z)) |
→ |
F(x,D(y,z)) |
(6) |
|
F(x,U(E,y)) |
→ |
U(x,F(E,y)) |
(7) |
|
D(E,F(x,y)) |
→ |
F(E,D(x,y)) |
(8) |
and S is the following TRS.
|
check(O(x)) |
→ |
O(x) |
(9) |
|
check(D(x,y)) |
→ |
D(check(x),y) |
(10) |
| E |
→ |
N(E) |
(11) |
|
check(F(x,y)) |
→ |
F(x,check(y)) |
(12) |
|
check(U(x,y)) |
→ |
U(x,check(y)) |
(13) |
|
check(O(x)) |
→ |
O(check(x)) |
(14) |
|
check(U(x,y)) |
→ |
U(check(x),y) |
(15) |
|
check(F(x,y)) |
→ |
F(check(x),y) |
(16) |
|
check(N(x)) |
→ |
N(check(x)) |
(17) |
|
check(D(x,y)) |
→ |
D(x,check(y)) |
(18) |
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by AProVE @ termCOMP 2023)
1 Loop
The following loop proves that R/S is not relative terminating.
| t0
|
= |
top(check(D(x,B))) |
|
→S
|
top(D(check(x),B)) |
|
→R
|
top(U(check(x),B)) |
|
→R
|
top(check(D(check(x),B))) |
|
= |
t3
|
where t3 =
t0σ
and
σ =
{x/check(x)}