Term Rewriting System R:
[YS, X, XS, X1, X2, Y, L]
app(nil, YS) -> YS
app(cons(X, XS), YS) -> cons(X, napp(activate(XS), YS))
app(X1, X2) -> napp(X1, X2)
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
zWadr(nil, YS) -> nil
zWadr(XS, nil) -> nil
zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nnil)), nzWadr(activate(XS), activate(YS)))
zWadr(X1, X2) -> nzWadr(X1, X2)
prefix(L) -> cons(nil, nzWadr(L, prefix(L)))
nil -> nnil
activate(napp(X1, X2)) -> app(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(nzWadr(X1, X2)) -> zWadr(X1, X2)
activate(X) -> X

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(cons(X, XS), YS) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, nnil))
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
PREFIX(L) -> NIL
PREFIX(L) -> PREFIX(L)
ACTIVATE(napp(X1, X2)) -> APP(X1, X2)
ACTIVATE(nfrom(X)) -> FROM(X)
ACTIVATE(nnil) -> NIL
ACTIVATE(nzWadr(X1, X2)) -> ZWADR(X1, X2)

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Size-Change Principle
       →DP Problem 2
         ↳MRR


Dependency Pairs:

ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, nnil))
ACTIVATE(nzWadr(X1, X2)) -> ZWADR(X1, X2)
ACTIVATE(napp(X1, X2)) -> APP(X1, X2)
APP(cons(X, XS), YS) -> ACTIVATE(XS)


Rules:


app(nil, YS) -> YS
app(cons(X, XS), YS) -> cons(X, napp(activate(XS), YS))
app(X1, X2) -> napp(X1, X2)
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
zWadr(nil, YS) -> nil
zWadr(XS, nil) -> nil
zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nnil)), nzWadr(activate(XS), activate(YS)))
zWadr(X1, X2) -> nzWadr(X1, X2)
prefix(L) -> cons(nil, nzWadr(L, prefix(L)))
nil -> nnil
activate(napp(X1, X2)) -> app(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(nzWadr(X1, X2)) -> zWadr(X1, X2)
activate(X) -> X





We number the DPs as follows:
  1. ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
  2. ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
  3. ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, nnil))
  4. ACTIVATE(nzWadr(X1, X2)) -> ZWADR(X1, X2)
  5. ACTIVATE(napp(X1, X2)) -> APP(X1, X2)
  6. APP(cons(X, XS), YS) -> ACTIVATE(XS)
and get the following Size-Change Graph(s):
{2, 1} , {2, 1}
2>1
{2, 1} , {2, 1}
1>1
{3} , {3}
2>1
{4} , {4}
1>1
1>2
{5} , {5}
1>1
1>2
{6} , {6}
1>1

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {4}
2>1
2>2
{6} , {5}
1>1
1>2
{5} , {6}
1>1
{4} , {2, 1}
1>1
{2, 1} , {4}
1>1
1>2
{6} , {3}
1>1
{4} , {6}
1>1
{3} , {4}
2>1
2>2
{5} , {2, 1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
nzWadr(x1, x2) -> nzWadr(x1, x2)
napp(x1, x2) -> napp(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Modular Removal of Rules


Dependency Pair:

PREFIX(L) -> PREFIX(L)


Rules:


app(nil, YS) -> YS
app(cons(X, XS), YS) -> cons(X, napp(activate(XS), YS))
app(X1, X2) -> napp(X1, X2)
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
zWadr(nil, YS) -> nil
zWadr(XS, nil) -> nil
zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, nnil)), nzWadr(activate(XS), activate(YS)))
zWadr(X1, X2) -> nzWadr(X1, X2)
prefix(L) -> cons(nil, nzWadr(L, prefix(L)))
nil -> nnil
activate(napp(X1, X2)) -> app(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(nzWadr(X1, X2)) -> zWadr(X1, X2)
activate(X) -> X





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(PREFIX(x1))=  x1  

We have the following set D of usable symbols: {PREFIX}
No Dependency Pairs can be deleted.
16 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳MRR
           →DP Problem 3
             ↳Non-Overlappingness Check


Dependency Pair:

PREFIX(L) -> PREFIX(L)


Rule:

none





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle: 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳MRR
           →DP Problem 3
             ↳NOC
             ...
               →DP Problem 4
                 ↳Non Termination


Dependency Pair:

PREFIX(L) -> PREFIX(L)


Rule:

none


Strategy:

innermost




Found an infinite P-chain over R:
P =

PREFIX(L) -> PREFIX(L)

R = none

s = PREFIX(L')
evaluates to t =PREFIX(L')

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:04 minutes