The TRS could be proven non-terminating. The proof took 371 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 (0ms).
 | – Problem 2 was processed with processor BackwardInstantiation (2ms).
 |    | – Problem 6 was processed with processor BackwardInstantiation (4ms).
 |    |    | – Problem 8 was processed with processor BackwardInstantiation (1ms).
 |    |    |    | – Problem 10 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (2ms)].
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (0ms).
 | – Problem 5 was processed with processor BackwardInstantiation (2ms).
 |    | – Problem 7 was processed with processor BackwardInstantiation (1ms).
 |    |    | – Problem 9 was processed with processor BackwardInstantiation (2ms).
 |    |    |    | – Problem 11 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zWadr#(cons(X, XS), cons(Y, YS))app#(Y, cons(X, nil))prefix#(L)prefix#(L)
app#(cons(X, XS), YS)app#(XS, YS)from#(X)from#(s(X))
prefix#(L)zWadr#(L, prefix(L))zWadr#(cons(X, XS), cons(Y, YS))zWadr#(XS, YS)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons

Strategy


Parameters


The following SCCs where found

prefix#(L) → prefix#(L)

from#(X) → from#(s(X))

app#(cons(X, XS), YS) → app#(XS, YS)

zWadr#(cons(X, XS), cons(Y, YS)) → zWadr#(XS, YS)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

prefix#(L)prefix#(L)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, 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, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, 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 8: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

prefix#(__L)prefix#(__L)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, 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 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

zWadr#(cons(X, XS), cons(Y, YS))zWadr#(XS, YS)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

zWadr#(cons(X, XS), cons(Y, YS))zWadr#(XS, YS)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

app#(cons(X, XS), YS)app#(XS, YS)

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

app#(cons(X, XS), YS)app#(XS, YS)

Problem 5: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

from#(X)from#(s(X))

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons

Strategy


Instantiation

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

Problem 7: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

from#(s(_X))from#(s(s(_X)))

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, cons, nil

Strategy


Instantiation

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

Problem 9: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

from#(s(s(__X)))from#(s(s(s(__X))))

Rewrite Rules

app(nil, YS)YSapp(cons(X, XS), YS)cons(X, app(XS, YS))
from(X)cons(X, from(s(X)))zWadr(nil, YS)nil
zWadr(XS, nil)nilzWadr(cons(X, XS), cons(Y, YS))cons(app(Y, cons(X, nil)), zWadr(XS, YS))
prefix(L)cons(nil, zWadr(L, prefix(L)))

Original Signature

Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons

Strategy


Instantiation

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