Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

app: {1, 2}
nil: empty set
cons: {1}
from: {1}
s: {1}
zWadr: {1, 2}
prefix: {1}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

app: {1, 2}
nil: empty set
cons: {1}
from: {1}
s: {1}
zWadr: {1, 2}
prefix: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {app, from, s, zWadr, prefix, APP, ZWADR, FROM, PREFIX} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, nil))


The hidden terms of R are:

app(XS, YS)
from(s(X))
zWadr(XS, YS)
zWadr(L, prefix(L))
prefix(L)

Every hiding context is built from:

app on positions {1, 2}
s on positions {1}
from on positions {1}
zWadr on positions {1, 2}
prefix on positions {1}

Hence, the new unhiding pairs DPu are :

U(app(x_0, x_1)) → U(x_0)
U(app(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_1)
U(prefix(x_0)) → U(x_0)
U(app(XS, YS)) → APP(XS, YS)
U(from(s(X))) → FROM(s(X))
U(zWadr(XS, YS)) → ZWADR(XS, YS)
U(zWadr(L, prefix(L))) → ZWADR(L, prefix(L))
U(prefix(L)) → PREFIX(L)

The TRS R consists of the following rules:

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

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 6 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {app, from, s, zWadr, prefix} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(app(x_0, x_1)) → U(x_0)
U(app(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_1)
U(prefix(x_0)) → U(x_0)

The TRS R consists of the following rules:

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

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(app(x_0, x_1)) → U(x_0)
U(app(x_0, x_1)) → U(x_1)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_0)
U(zWadr(x_0, x_1)) → U(x_1)
U(prefix(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof
            ↳ QCSDP
              ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {app, from, s, zWadr, prefix} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.