Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


   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)
   APP(cons(X, XS), YS) -> ACTIVATE(XS)
   ACTIVATE(n__from(X)) -> FROM(X)
   ACTIVATE(n__zWadr(X1, X2)) -> ZWADR(X1, X2)
   ACTIVATE(n__app(X1, X2)) -> APP(X1, X2)
   ACTIVATE(n__nil) -> NIL
   PREFIX(L) -> NIL
   PREFIX(L) -> PREFIX(L)

Furthermore, R contains two SCCs.


SCC1:

ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) -> APP(X1, X2)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ACTIVATE(n__zWadr(X1, X2)) -> ZWADR(X1, X2)
APP(cons(X, XS), YS) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, n__nil))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(APP(x_1, x_2)) = x_1 + x_2
POL(n__nil) = 0
POL(ACTIVATE(x_1)) = x_1
POL(ZWADR(x_1, x_2)) = x_1 + x_2
POL(n__app(x_1, x_2)) = x_1 + x_2
POL(cons(x_1, x_2)) = x_1 + x_2
POL(n__zWadr(x_1, x_2)) = x_1 + x_2

The following Dependency Pairs can be deleted:

   ACTIVATE(n__app(X1, X2)) -> APP(X1, X2)
   ACTIVATE(n__zWadr(X1, X2)) -> ZWADR(X1, X2)



 This transformation is resulting in no new subcycles.


SCC2:

PREFIX(L) -> PREFIX(L)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(PREFIX(x_1)) = 1 + x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

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


 This transformation is resulting in one new subcycle:


SCC2.MRR1:

PREFIX(L) -> PREFIX(L)

Applying the non-overlappingness check to the DPs.

The transformation is resulting in one subcycle:

SCC2.MRR1.NOC1:

PREFIX(L) -> PREFIX(L)

Found an infinite P-chain over R:
P = PREFIX(L) -> PREFIX(L)
R = []
s = PREFIX(L') evaluates to t = PREFIX(L')
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.903 seconds.