Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex3_3_25_Bor03_Z)

The rewrite relation of the following TRS is considered.

app(nil,YS) → YS (1)
app(cons(X,XS),YS) → cons(X,n__app(activate(XS),YS)) (2)
from(X) → cons(X,n__from(s(X))) (3)
zWadr(nil,YS) → nil (4)
zWadr(XS,nil) → nil (5)
zWadr(cons(X,XS),cons(Y,YS)) → cons(app(Y,cons(X,n__nil)),n__zWadr(activate(XS),activate(YS))) (6)
prefix(L) → cons(nil,n__zWadr(L,prefix(L))) (7)
app(X1,X2) → n__app(X1,X2) (8)
from(X) → n__from(X) (9)
nil → n__nil (10)
zWadr(X1,X2) → n__zWadr(X1,X2) (11)
activate(n__app(X1,X2)) → app(X1,X2) (12)
activate(n__from(X)) → from(X) (13)
activate(n__nil) → nil (14)
activate(n__zWadr(X1,X2)) → zWadr(X1,X2) (15)
activate(X) → X (16)
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 = prefix(L)
→ cons(nil,n__zWadr(L,prefix(L)))
= t1
where t1 = C[t0] and C = cons(nil,n__zWadr(L,☐))