Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex6_15_AEL02_Z)

The rewrite relation of the following TRS is considered.

sel(s(X),cons(Y,Z)) → sel(X,activate(Z)) (1)
sel(0,cons(X,Z)) → X (2)
first(0,Z) → nil (3)
first(s(X),cons(Y,Z)) → cons(Y,n__first(X,activate(Z))) (4)
from(X) → cons(X,n__from(s(X))) (5)
sel1(s(X),cons(Y,Z)) → sel1(X,activate(Z)) (6)
sel1(0,cons(X,Z)) → quote(X) (7)
first1(0,Z) → nil1 (8)
first1(s(X),cons(Y,Z)) → cons1(quote(Y),first1(X,activate(Z))) (9)
quote(n__0) → 01 (10)
quote1(n__cons(X,Z)) → cons1(quote(activate(X)),quote1(activate(Z))) (11)
quote1(n__nil) → nil1 (12)
quote(n__s(X)) → s1(quote(activate(X))) (13)
quote(n__sel(X,Z)) → sel1(activate(X),activate(Z)) (14)
quote1(n__first(X,Z)) → first1(activate(X),activate(Z)) (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,Z) (20)
first(X1,X2) → n__first(X1,X2) (21)
from(X) → n__from(X) (22)
0 → n__0 (23)
cons(X1,X2) → n__cons(X1,X2) (24)
nil → n__nil (25)
s(X) → n__s(X) (26)
sel(X1,X2) → n__sel(X1,X2) (27)
activate(n__first(X1,X2)) → first(X1,X2) (28)
activate(n__from(X)) → from(X) (29)
activate(n__0) → 0 (30)
activate(n__cons(X1,X2)) → cons(X1,X2) (31)
activate(n__nil) → nil (32)
activate(n__s(X)) → s(X) (33)
activate(n__sel(X1,X2)) → sel(X1,X2) (34)
activate(X) → X (35)
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 = quote1(activate(n__from(X')))
→ quote1(from(X'))
→ quote1(cons(X',n__from(s(X'))))
→ quote1(n__cons(X',n__from(s(X'))))
→ cons1(quote(activate(X')),quote1(activate(n__from(s(X')))))
= t4
where t4 = C[t0σ] and σ = {X'/s(X')} and C = cons1(quote(activate(X')),☐)