Certification Problem
Input (TPDB TRS_Relative/Relative_05/rtL-evnz)
The relative rewrite relation R/S is considered where R is the following TRS
|
top(ok(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.
|
F(x,ok(y)) |
→ |
ok(F(x,y)) |
(9) |
| E |
→ |
N(E) |
(10) |
|
F(ok(x),y) |
→ |
ok(F(x,y)) |
(11) |
|
O(ok(x)) |
→ |
ok(O(x)) |
(12) |
|
U(ok(x),y) |
→ |
ok(U(x,y)) |
(13) |
|
check(U(x,y)) |
→ |
U(check(x),y) |
(14) |
|
check(N(x)) |
→ |
N(check(x)) |
(15) |
|
D(ok(x),y) |
→ |
ok(D(x,y)) |
(16) |
|
U(O(x),y) |
→ |
U(x,y) |
(17) |
|
check(D(x,y)) |
→ |
D(check(x),y) |
(18) |
|
check(F(x,y)) |
→ |
F(x,check(y)) |
(19) |
|
check(U(x,y)) |
→ |
U(x,check(y)) |
(20) |
|
U(N(x),y) |
→ |
U(x,y) |
(21) |
|
D(O(x),y) |
→ |
D(x,y) |
(22) |
|
check(O(x)) |
→ |
O(check(x)) |
(23) |
|
N(ok(x)) |
→ |
ok(N(x)) |
(24) |
|
D(N(x),y) |
→ |
D(x,y) |
(25) |
|
D(x,ok(y)) |
→ |
ok(D(x,y)) |
(26) |
|
check(O(x)) |
→ |
ok(O(x)) |
(27) |
|
check(F(x,y)) |
→ |
F(check(x),y) |
(28) |
|
U(x,ok(y)) |
→ |
ok(U(x,y)) |
(29) |
|
check(D(x,y)) |
→ |
D(x,check(y)) |
(30) |
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(O(x),B))) |
|
→S
|
top(D(check(O(x)),B)) |
|
→S
|
top(D(ok(O(x)),B)) |
|
→R
|
top(U(ok(O(x)),B)) |
|
→S
|
top(ok(U(O(x),B))) |
|
→R
|
top(check(D(O(x),B))) |
|
= |
t5
|
where t5 =
t0