NO

The TRS could be proven non-terminating. The proof took 665 ms.

The following reduction sequence is a witness for non-termination:

prefix#(___L) →* prefix#(___L)

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (64ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (214ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (97ms).
 |    |    | – Problem 5 was processed with processor DependencyGraph (5ms).
 | – Problem 3 was processed with processor BackwardInstantiation (1ms).
 |    | – Problem 6 was processed with processor BackwardInstantiation (1ms).
 |    |    | – Problem 7 was processed with processor BackwardInstantiation (1ms).
 |    |    |    | – Problem 8 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (2ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

prefix#(L)nil#activate#(n__nil)nil#
activate#(n__zWadr(X1, X2))zWadr#(X1, X2)zWadr#(cons(X, XS), cons(Y, YS))activate#(YS)
app#(cons(X, XS), YS)activate#(XS)zWadr#(XS, nil)nil#
zWadr#(cons(X, XS), cons(Y, YS))activate#(XS)prefix#(L)prefix#(L)
zWadr#(cons(X, XS), cons(Y, YS))app#(Y, cons(X, n__nil))activate#(n__from(X))from#(X)
zWadr#(nil, YS)nil#activate#(n__app(X1, X2))app#(X1, X2)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons

Strategy


The following SCCs where found

prefix#(L) → prefix#(L)

activate#(n__zWadr(X1, X2)) → zWadr#(X1, X2)zWadr#(cons(X, XS), cons(Y, YS)) → activate#(YS)
app#(cons(X, XS), YS) → activate#(XS)zWadr#(cons(X, XS), cons(Y, YS)) → activate#(XS)
zWadr#(cons(X, XS), cons(Y, YS)) → app#(Y, cons(X, n__nil))activate#(n__app(X1, X2)) → app#(X1, X2)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__zWadr(X1, X2))zWadr#(X1, X2)zWadr#(cons(X, XS), cons(Y, YS))activate#(YS)
app#(cons(X, XS), YS)activate#(XS)zWadr#(cons(X, XS), cons(Y, YS))activate#(XS)
zWadr#(cons(X, XS), cons(Y, YS))app#(Y, cons(X, n__nil))activate#(n__app(X1, X2))app#(X1, X2)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__app(X1, X2))app#(X1, X2)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__zWadr(X1, X2))zWadr#(X1, X2)zWadr#(cons(X, XS), cons(Y, YS))activate#(YS)
app#(cons(X, XS), YS)activate#(XS)zWadr#(cons(X, XS), cons(Y, YS))activate#(XS)
zWadr#(cons(X, XS), cons(Y, YS))app#(Y, cons(X, n__nil))

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, n__from, s, n__zWadr, prefix, n__app, n__nil, from, cons, nil

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__zWadr(X1, X2))zWadr#(X1, X2)

Problem 5: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zWadr#(cons(X, XS), cons(Y, YS))activate#(YS)app#(cons(X, XS), YS)activate#(XS)
zWadr#(cons(X, XS), cons(Y, YS))activate#(XS)zWadr#(cons(X, XS), cons(Y, YS))app#(Y, cons(X, n__nil))

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons

Strategy


There are no SCCs!

Problem 3: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

prefix#(L)prefix#(L)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons

Strategy


Instantiation

For all potential predecessors l → r of the rule prefix#(L) → prefix#(L) on dependency pair chains it holds that: Thus, prefix#(L) → prefix#(L) is replaced by instances determined through the above matching. These instances are:
prefix#(_L) → prefix#(_L)

Problem 6: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

prefix#(_L)prefix#(_L)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, n__from, s, n__zWadr, prefix, n__app, n__nil, from, cons, nil

Strategy


Instantiation

For all potential predecessors l → r of the rule prefix#(_L) → prefix#(_L) on dependency pair chains it holds that: Thus, prefix#(_L) → prefix#(_L) is replaced by instances determined through the above matching. These instances are:
prefix#(__L) → prefix#(__L)

Problem 7: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

prefix#(__L)prefix#(__L)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, n__app(activate(XS), YS))
from(X)cons(X, n__from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L)cons(nil, n__zWadr(L, prefix(L)))app(X1, X2)n__app(X1, X2)
from(X)n__from(X)niln__nil
zWadr(X1, X2)n__zWadr(X1, X2)activate(n__app(X1, X2))app(X1, X2)
activate(n__from(X))from(X)activate(n__nil)nil
activate(n__zWadr(X1, X2))zWadr(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, app, zWadr, s, n__from, n__zWadr, n__app, prefix, from, n__nil, nil, cons

Strategy


Instantiation

For all potential predecessors l → r of the rule prefix#(__L) → prefix#(__L) on dependency pair chains it holds that: Thus, prefix#(__L) → prefix#(__L) is replaced by instances determined through the above matching. These instances are:
prefix#(___L) → prefix#(___L)