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)}