(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__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)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(activate(x1)) = | 0A | + | 0A | · | x1 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(n__from(x1)) = | 1A | + | 1A | · | x1 |
POL(n__s(x1)) = | -I | + | 0A | · | x1 |
POL(n__zWadr(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(ZWADR(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(n__prefix(x1)) = | -I | + | 0A | · | x1 |
POL(zWadr(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(prefix(x1)) = | 0A | + | 0A | · | x1 |
POL(from(x1)) = | 1A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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__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.
(7) 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)) = | 0A | + | 0A | · | x1 |
POL(n__app(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(APP(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(activate(x1)) = | 0A | + | 0A | · | x1 |
POL(cons(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
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__prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(zWadr(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(from(x1)) = | 0A | + | 0A | · | x1 |
POL(n__from(x1)) = | -I | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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__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.
(9) 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)) = | -I | + | 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)) = | 0A | + | 0A | · | x1 |
POL(n__zWadr(x1, x2)) = | 0A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(ZWADR(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(zWadr(x1, x2)) = | 0A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(prefix(x1)) = | 0A | + | 1A | · | x1 |
POL(n__prefix(x1)) = | 0A | + | 1A | · | x1 |
POL(from(x1)) = | 1A | + | 0A | · | x1 |
POL(n__from(x1)) = | 1A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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__app(X1, X2)) → ACTIVATE(X2)
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__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)) = | 0A | + | 0A | · | x1 |
POL(n__app(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(APP(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(activate(x1)) = | 0A | + | 0A | · | x1 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(n__s(x1)) = | 0A | + | 0A | · | x1 |
POL(n__zWadr(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(ZWADR(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(zWadr(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | 1A | + | 0A | · | x1 | + | 1A | · | x2 |
POL(prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(n__prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(from(x1)) = | 3A | + | 0A | · | x1 |
POL(n__from(x1)) = | 3A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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)) = | 0A | + | 0A | · | x1 |
POL(n__app(x1, x2)) = | -I | + | 0A | · | x1 | + | 1A | · | x2 |
POL(APP(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(activate(x1)) = | -I | + | 0A | · | x1 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(n__s(x1)) = | -I | + | 0A | · | x1 |
POL(n__zWadr(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(ZWADR(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(zWadr(x1, x2)) = | -I | + | 1A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | -I | + | 0A | · | x1 | + | 1A | · | x2 |
POL(prefix(x1)) = | 0A | + | 1A | · | x1 |
POL(n__prefix(x1)) = | 0A | + | 1A | · | x1 |
POL(from(x1)) = | 1A | + | 0A | · | x1 |
POL(n__from(x1)) = | 1A | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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 | + | 0A | · | x2 |
POL(activate(x1)) = | 0A | + | 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)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(zWadr(x1, x2)) = | 1A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(app(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(n__prefix(x1)) = | 1A | + | 1A | · | x1 |
POL(from(x1)) = | 1A | + | 1A | · | x1 |
POL(n__from(x1)) = | 1A | + | 1A | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(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__s(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(ACTIVATE(x1)) = | | + | | · | x1 |
POL(n__app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(APP(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ZWADR(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__prefix(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(X))
(18) 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__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) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(ACTIVATE(x1)) = x1
POL(APP(x1, x2)) = 1 + 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)) = x1
POL(n__s(x1)) = 0
POL(n__zWadr(x1, x2)) = x2
POL(nil) = 0
POL(prefix(x1)) = x1
POL(s(x1)) = 0
POL(zWadr(x1, x2)) = x2
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(X))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
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.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
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.
(23) 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))
(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__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.
(25) 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)
(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__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.
(27) 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)
(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__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.
(29) 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)
(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__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.
(31) 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))
(32) 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.
(33) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(34) 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.
(35) 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)
(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(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.
(37) 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)
(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(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.
(39) 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)
(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__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.
(41) 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)
(42) 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.
(43) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(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__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.
(45) 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)
(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)
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.
(47) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(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__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.
(49) 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)
(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)
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.
(51) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(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__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.
(53) 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)
(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)
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.
(55) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(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__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.
(57) 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)
(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)
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.
(59) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(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__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.
(61) 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)
(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)
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.
(63) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(64) 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.
(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)) = | | + | | · | x1 |
POL(n__zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ZWADR(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__prefix(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(X))
(66) 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__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__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__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__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__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__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__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)) = | | + | | · | x1 |
POL(n__zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ZWADR(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__prefix(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(X))
(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__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.
(69) 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)) = | | + | | · | x1 |
POL(n__zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ZWADR(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(app(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(zWadr(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__prefix(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
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)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
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(n__from(X)) → from(activate(X))
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
prefix(X) → n__prefix(X)
zWadr(X1, X2) → n__zWadr(X1, X2)
nil → n__nil
s(X) → n__s(X)
from(X) → n__from(X)
app(X1, X2) → n__app(X1, X2)
activate(X) → X
activate(n__prefix(X)) → prefix(activate(X))
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__nil) → nil
activate(n__s(X)) → s(activate(X))
(70) 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.
(71) 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 sequenceZWADR(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.
(72) FALSE