Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 QDPOrderProof (⇔)
↳8 QDP
↳9 QDPOrderProof (⇔)
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 DependencyGraphProof (⇔)
↳20 QDP
↳21 Narrowing (⇔)
↳22 QDP
↳23 Narrowing (⇔)
↳24 QDP
↳25 Narrowing (⇔)
↳26 QDP
↳27 Narrowing (⇔)
↳28 QDP
↳29 Narrowing (⇔)
↳30 QDP
↳31 DependencyGraphProof (⇔)
↳32 QDP
↳33 Narrowing (⇔)
↳34 QDP
↳35 Narrowing (⇔)
↳36 QDP
↳37 Narrowing (⇔)
↳38 QDP
↳39 Narrowing (⇔)
↳40 QDP
↳41 DependencyGraphProof (⇔)
↳42 QDP
↳43 Narrowing (⇔)
↳44 QDP
↳45 DependencyGraphProof (⇔)
↳46 QDP
↳47 Narrowing (⇔)
↳48 QDP
↳49 DependencyGraphProof (⇔)
↳50 QDP
↳51 Narrowing (⇔)
↳52 QDP
↳53 DependencyGraphProof (⇔)
↳54 QDP
↳55 Narrowing (⇔)
↳56 QDP
↳57 DependencyGraphProof (⇔)
↳58 QDP
↳59 Narrowing (⇔)
↳60 QDP
↳61 DependencyGraphProof (⇔)
↳62 QDP
↳63 QDPOrderProof (⇔)
↳64 QDP
↳65 QDPOrderProof (⇔)
↳66 QDP
↳67 QDPOrderProof (⇔)
↳68 QDP
↳69 NonTerminationProof (⇔)
↳70 FALSE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
PREFIX(L) → NIL
ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → FROM(activate(X))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → PREFIX(activate(X))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 5 less nodes.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(5) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__prefix(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = 1A + 0A·x1

POL(n__app(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(APP(x1, x2)) = 1A + 0A·x1 + -I·x2

POL(activate(x1)) = 1A + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(n__from(x1)) = -I + 0A·x1

POL(n__s(x1)) = -I + 0A·x1

POL(n__zWadr(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(n__nil) = 0A

POL(n__prefix(x1)) = 2A + 1A·x1

POL(nil) = 0A

POL(s(x1)) = 1A + 0A·x1

POL(prefix(x1)) = 2A + 1A·x1

POL(zWadr(x1, x2)) = 1A + 0A·x1 + 0A·x2

POL(from(x1)) = -I + 0A·x1

POL(app(x1, x2)) = 1A + 0A·x1 + 0A·x2

The following usable rules [FROCOS05] were oriented:

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

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(7) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = -I + 0A·x1

POL(n__app(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(APP(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(activate(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(n__from(x1)) = -I + 0A·x1

POL(n__s(x1)) = -I + 0A·x1

POL(n__zWadr(x1, x2)) = 0A + 2A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(n__nil) = 0A

POL(nil) = 0A

POL(s(x1)) = -I + 0A·x1

POL(n__prefix(x1)) = 0A + 2A·x1

POL(prefix(x1)) = 0A + 2A·x1

POL(zWadr(x1, x2)) = 0A + 2A·x1 + 0A·x2

POL(from(x1)) = -I + 0A·x1

POL(app(x1, x2)) = 0A + 0A·x1 + 0A·x2

The following usable rules [FROCOS05] were oriented:

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

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = -I + 0A·x1

POL(n__app(x1, x2)) = -I + 0A·x1 + 1A·x2

POL(APP(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(activate(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(n__from(x1)) = 0A + 0A·x1

POL(n__s(x1)) = 0A + 0A·x1

POL(n__zWadr(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(n__nil) = 0A

POL(nil) = 0A

POL(s(x1)) = 0A + 0A·x1

POL(n__prefix(x1)) = 0A + 1A·x1

POL(prefix(x1)) = 0A + 1A·x1

POL(zWadr(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(from(x1)) = 0A + 0A·x1

POL(app(x1, x2)) = -I + 0A·x1 + 1A·x2

The following usable rules [FROCOS05] were oriented:

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

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__from(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = -I + 0A·x1

POL(n__app(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(APP(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(activate(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(n__from(x1)) = -I + 1A·x1

POL(n__s(x1)) = -I + 0A·x1

POL(n__zWadr(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(n__nil) = 0A

POL(nil) = 0A

POL(s(x1)) = -I + 0A·x1

POL(n__prefix(x1)) = 0A + 1A·x1

POL(prefix(x1)) = 0A + 1A·x1

POL(zWadr(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(from(x1)) = -I + 1A·x1

POL(app(x1, x2)) = 0A + 0A·x1 + 0A·x2

The following usable rules [FROCOS05] were oriented:

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

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = -I + 0A·x1

POL(n__app(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(APP(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(activate(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 0A·x1 + 0A·x2

POL(n__s(x1)) = -I + 0A·x1

POL(n__zWadr(x1, x2)) = 0A + 1A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = 0A + 1A·x1 + 0A·x2

POL(n__nil) = 0A

POL(nil) = 0A

POL(s(x1)) = -I + 0A·x1

POL(n__prefix(x1)) = 0A + 1A·x1

POL(prefix(x1)) = 0A + 1A·x1

POL(zWadr(x1, x2)) = 0A + 1A·x1 + 0A·x2

POL(n__from(x1)) = -I + 0A·x1

POL(from(x1)) = -I + 0A·x1

POL(app(x1, x2)) = 0A + 0A·x1 + 0A·x2

The following usable rules [FROCOS05] were oriented:

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

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVATE(x1)) = -I + 0A·x1

POL(n__app(x1, x2)) = 0A + 0A·x1 + 0A·x2

POL(APP(x1, x2)) = -I + 0A·x1 + -I·x2

POL(activate(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(n__s(x1)) = -I + 0A·x1

POL(n__zWadr(x1, x2)) = 1A + 1A·x1 + 0A·x2

POL(ZWADR(x1, x2)) = 0A + 1A·x1 + 0A·x2

POL(n__nil) = 0A

POL(nil) = 0A

POL(s(x1)) = -I + 0A·x1

POL(n__prefix(x1)) = 5A + 1A·x1

POL(prefix(x1)) = 5A + 1A·x1

POL(zWadr(x1, x2)) = 1A + 1A·x1 + 0A·x2

POL(n__from(x1)) = -I + 1A·x1

POL(from(x1)) = -I + 1A·x1

POL(app(x1, x2)) = 0A + 0A·x1 + 0A·x2

The following usable rules [FROCOS05] were oriented:

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

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(ACTIVATE(x1)) = x1   
POL(APP(x1, x2)) = x1   
POL(ZWADR(x1, x2)) = x2   
POL(activate(x1)) = x1   
POL(app(x1, x2)) = 1 + x1 + x2   
POL(cons(x1, x2)) = x2   
POL(from(x1)) = 0   
POL(n__app(x1, x2)) = 1 + x1 + x2   
POL(n__from(x1)) = 0   
POL(n__nil) = 0   
POL(n__prefix(x1)) = 0   
POL(n__s(x1)) = 1 + x1   
POL(n__zWadr(x1, x2)) = x2   
POL(nil) = 0   
POL(prefix(x1)) = 0   
POL(s(x1)) = 1 + x1   
POL(zWadr(x1, x2)) = x2   

The following usable rules [FROCOS05] were oriented:

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

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2)) at position [0] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(27) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__nil, y0)) → ZWADR(n__nil, activate(y0))

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__nil, y0)) → ZWADR(n__nil, activate(y0))

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(35) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(37) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1)) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), n__nil)

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(41) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(43) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), n__nil)

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(45) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), n__nil)

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), n__nil)

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(55) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), n__nil)

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(59) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil) at position [1] we obtained the following new rules [LPAR04]:

ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, n__nil)

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(61) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(63) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ACTIVATE(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(n__zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\11/
·x2

POL(n__app(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/10\
\01/
·x2

POL(ZWADR(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/01\
\00/
·x2

POL(app(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/10\
\01/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/10\
\01/
·x2

POL(n__from(x1)) =
/0\
\0/
 +
/11\
\01/
·x1

POL(from(x1)) =
/0\
\0/
 +
/11\
\01/
·x1

POL(n__s(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(s(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\11/
·x2

POL(n__prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

The following usable rules [FROCOS05] were oriented:

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

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ACTIVATE(x1)) =
/1\
\0/
 +
/01\
\00/
·x1

POL(n__zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(ZWADR(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/10\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/01\
\10/
·x2

POL(n__app(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(n__from(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(app(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(from(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(n__prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

The following usable rules [FROCOS05] were oriented:

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

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(67) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ACTIVATE(x1)) =
/0\
\1/
 +
/10\
\00/
·x1

POL(n__zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(ZWADR(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/01\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/01\
\10/
·x2

POL(n__app(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(n__from(x1)) =
/1\
\1/
 +
/01\
\10/
·x1

POL(app(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(from(x1)) =
/1\
\1/
 +
/01\
\10/
·x1

POL(zWadr(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(n__prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(prefix(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__s(x1)) =
/0\
\0/
 +
/01\
\10/
·x1

POL(s(x1)) =
/0\
\0/
 +
/01\
\10/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

The following usable rules [FROCOS05] were oriented:

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

(68) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(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, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(69) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ZWADR(from(X'), prefix(activate(n__from(y0)))) evaluates to t =ZWADR(from(activate(y0)), prefix(activate(n__from(y0))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [X' / activate(y0)]



Rewriting sequence

ZWADR(from(X'), prefix(activate(n__from(y0)))) → ZWADR(from(X'), prefix(n__from(y0)))
with rule activate(X) → X at position [1,0] and matcher [X / n__from(y0)]

ZWADR(from(X'), prefix(n__from(y0))) → ZWADR(from(X'), cons(nil, n__zWadr(n__from(y0), n__prefix(n__from(y0)))))
with rule prefix(L) → cons(nil, n__zWadr(L, n__prefix(L))) at position [1] and matcher [L / n__from(y0)]

ZWADR(from(X'), cons(nil, n__zWadr(n__from(y0), n__prefix(n__from(y0))))) → ZWADR(cons(X', n__from(n__s(X'))), cons(nil, n__zWadr(n__from(y0), n__prefix(n__from(y0)))))
with rule from(X'') → cons(X'', n__from(n__s(X''))) at position [0] and matcher [X'' / X']

ZWADR(cons(X', n__from(n__s(X'))), cons(nil, n__zWadr(n__from(y0), n__prefix(n__from(y0))))) → ACTIVATE(n__zWadr(n__from(y0), n__prefix(n__from(y0))))
with rule ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS) at position [] and matcher [X / X', XS / n__from(n__s(X')), Y / nil, YS / n__zWadr(n__from(y0), n__prefix(n__from(y0)))]

ACTIVATE(n__zWadr(n__from(y0), n__prefix(n__from(y0)))) → ZWADR(from(activate(y0)), prefix(activate(n__from(y0))))
with rule ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(70) FALSE