Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex6_15_AEL02_L)

The rewrite relation of the following TRS is considered.

sel(s(X),cons(Y)) → sel(X,Z) (1)
sel1(s(X),cons(Y)) → sel1(X,Z) (2)
first1(s(X),cons(Y)) → cons1(quote,first1(X,Z)) (3)
quote → sel1(X,Z) (4)
quote1 → first1(X,Z) (5)
sel(0,cons(X)) → X (6)
first(0,Z) → nil (7)
first(s(X),cons(Y)) → cons(Y) (8)
from(X) → cons(X) (9)
sel1(0,cons(X)) → quote (10)
first1(0,Z) → nil1 (11)
quote → 01 (12)
quote1 → cons1(quote,quote1) (13)
quote1 → nil1 (14)
quote → s1(quote) (15)
unquote(01) → 0 (16)
unquote(s1(X)) → s(unquote(X)) (17)
unquote1(nil1) → nil (18)
unquote1(cons1(X,Z)) → fcons(unquote(X),unquote1(Z)) (19)
fcons(X,Z) → cons(X) (20)
The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = sel(s(X),cons(Y))
→ sel(X,sel(s(X),cons(Y)))
= t1
where t1 = C[t0] and C = sel(X,☐)