Term Rewriting System R:

   [YS, X, XS, X1, X2, Y, L]
   a__app(nil, YS) -> mark(YS)
   a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
   a__app(X1, X2) -> app(X1, X2)
   a__from(X) -> cons(mark(X), from(s(X)))
   a__from(X) -> from(X)
   a__zWadr(nil, YS) -> nil
   a__zWadr(XS, nil) -> nil
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
   a__zWadr(X1, X2) -> zWadr(X1, X2)
   a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))
   a__prefix(X) -> prefix(X)
   mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   A__ZWADR(cons(X, XS), cons(Y, YS)) -> A__APP(mark(Y), cons(mark(X), nil))
   A__ZWADR(cons(X, XS), cons(Y, YS)) -> MARK(Y)
   A__ZWADR(cons(X, XS), cons(Y, YS)) -> MARK(X)
   MARK(s(X)) -> MARK(X)
   MARK(prefix(X)) -> A__PREFIX(mark(X))
   MARK(prefix(X)) -> MARK(X)
   MARK(cons(X1, X2)) -> MARK(X1)
   MARK(from(X)) -> A__FROM(mark(X))
   MARK(from(X)) -> MARK(X)
   MARK(zWadr(X1, X2)) -> A__ZWADR(mark(X1), mark(X2))
   MARK(zWadr(X1, X2)) -> MARK(X1)
   MARK(zWadr(X1, X2)) -> MARK(X2)
   MARK(app(X1, X2)) -> A__APP(mark(X1), mark(X2))
   MARK(app(X1, X2)) -> MARK(X1)
   MARK(app(X1, X2)) -> MARK(X2)
   A__APP(cons(X, XS), YS) -> MARK(X)
   A__APP(nil, YS) -> MARK(YS)
   A__FROM(X) -> MARK(X)

Furthermore, R contains one SCC.


SCC1:

A__ZWADR(cons(X, XS), cons(Y, YS)) -> MARK(X)
MARK(app(X1, X2)) -> MARK(X2)
MARK(app(X1, X2)) -> MARK(X1)
A__APP(nil, YS) -> MARK(YS)
MARK(app(X1, X2)) -> A__APP(mark(X1), mark(X2))
MARK(zWadr(X1, X2)) -> MARK(X2)
MARK(zWadr(X1, X2)) -> MARK(X1)
A__ZWADR(cons(X, XS), cons(Y, YS)) -> MARK(Y)
MARK(zWadr(X1, X2)) -> A__ZWADR(mark(X1), mark(X2))
MARK(from(X)) -> MARK(X)
A__FROM(X) -> MARK(X)
MARK(from(X)) -> A__FROM(mark(X))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(prefix(X)) -> MARK(X)
MARK(s(X)) -> MARK(X)
A__APP(cons(X, XS), YS) -> MARK(X)
A__ZWADR(cons(X, XS), cons(Y, YS)) -> A__APP(mark(Y), cons(mark(X), nil))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zWadr(XS, nil) -> nil
   a__zWadr(X1, X2) -> zWadr(X1, X2)
   a__zWadr(nil, YS) -> nil
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
   a__from(X) -> cons(mark(X), from(s(X)))
   a__from(X) -> from(X)
   mark(s(X)) -> s(mark(X))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
   mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
   a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
   a__app(nil, YS) -> mark(YS)
   a__app(X1, X2) -> app(X1, X2)
   a__prefix(X) -> prefix(X)
   a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(prefix(x_1)) = x_1
POL(nil) = 0
POL(A__FROM(x_1)) = x_1
POL(s(x_1)) = x_1
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(zWadr(x_1, x_2)) = 1 + x_1 + x_2
POL(a__app(x_1, x_2)) = x_1 + x_2
POL(A__ZWADR(x_1, x_2)) = 1 + x_1 + x_2
POL(a__prefix(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1
POL(a__zWadr(x_1, x_2)) = 1 + x_1 + x_2
POL(A__APP(x_1, x_2)) = x_1 + x_2
POL(a__from(x_1)) = x_1
POL(from(x_1)) = x_1
POL(app(x_1, x_2)) = x_1 + x_2

 resulting in one subcycle.


SCC1.Polo1:

A__APP(nil, YS) -> MARK(YS)
MARK(app(X1, X2)) -> MARK(X1)
A__APP(cons(X, XS), YS) -> MARK(X)
MARK(app(X1, X2)) -> A__APP(mark(X1), mark(X2))
MARK(from(X)) -> MARK(X)
A__FROM(X) -> MARK(X)
MARK(from(X)) -> A__FROM(mark(X))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(prefix(X)) -> MARK(X)
MARK(s(X)) -> MARK(X)
MARK(app(X1, X2)) -> MARK(X2)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zWadr(XS, nil) -> nil
   a__zWadr(X1, X2) -> zWadr(X1, X2)
   a__zWadr(nil, YS) -> nil
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
   a__from(X) -> cons(mark(X), from(s(X)))
   a__from(X) -> from(X)
   mark(s(X)) -> s(mark(X))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
   mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
   a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
   a__app(nil, YS) -> mark(YS)
   a__app(X1, X2) -> app(X1, X2)
   a__prefix(X) -> prefix(X)
   a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(prefix(x_1)) = 1 + x_1
POL(nil) = 1
POL(A__FROM(x_1)) = x_1
POL(s(x_1)) = x_1
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(zWadr(x_1, x_2)) = x_1 + x_2
POL(a__app(x_1, x_2)) = x_1 + x_2
POL(a__prefix(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = x_1
POL(a__zWadr(x_1, x_2)) = x_1 + x_2
POL(A__APP(x_1, x_2)) = x_1 + x_2
POL(a__from(x_1)) = x_1
POL(from(x_1)) = x_1
POL(app(x_1, x_2)) = x_1 + x_2

 resulting in one subcycle.


SCC1.Polo1.Polo1:

MARK(app(X1, X2)) -> MARK(X2)
A__APP(cons(X, XS), YS) -> MARK(X)
MARK(app(X1, X2)) -> A__APP(mark(X1), mark(X2))
MARK(from(X)) -> MARK(X)
A__FROM(X) -> MARK(X)
MARK(from(X)) -> A__FROM(mark(X))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
MARK(app(X1, X2)) -> MARK(X1)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zWadr(XS, nil) -> nil
   a__zWadr(X1, X2) -> zWadr(X1, X2)
   a__zWadr(nil, YS) -> nil
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
   a__from(X) -> cons(mark(X), from(s(X)))
   a__from(X) -> from(X)
   mark(s(X)) -> s(mark(X))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
   mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
   a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
   a__app(nil, YS) -> mark(YS)
   a__app(X1, X2) -> app(X1, X2)
   a__prefix(X) -> prefix(X)
   a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(prefix(x_1)) = 0
POL(nil) = 0
POL(A__FROM(x_1)) = x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(MARK(x_1)) = x_1
POL(zWadr(x_1, x_2)) = 1 + x_1 + x_2
POL(a__app(x_1, x_2)) = 1 + x_1 + x_2
POL(a__prefix(x_1)) = 0
POL(cons(x_1, x_2)) = x_1
POL(a__zWadr(x_1, x_2)) = 1 + x_1 + x_2
POL(A__APP(x_1, x_2)) = x_1
POL(a__from(x_1)) = x_1
POL(from(x_1)) = x_1
POL(app(x_1, x_2)) = 1 + x_1 + x_2

 resulting in one subcycle.


SCC1.Polo1.Polo1.Polo1:

MARK(from(X)) -> MARK(X)
A__FROM(X) -> MARK(X)
MARK(from(X)) -> A__FROM(mark(X))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   a__zWadr(XS, nil) -> nil
   a__zWadr(X1, X2) -> zWadr(X1, X2)
   a__zWadr(nil, YS) -> nil
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
   a__from(X) -> cons(mark(X), from(s(X)))
   a__from(X) -> from(X)
   mark(s(X)) -> s(mark(X))
   mark(prefix(X)) -> a__prefix(mark(X))
   mark(nil) -> nil
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(from(X)) -> a__from(mark(X))
   mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
   mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
   a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
   a__app(nil, YS) -> mark(YS)
   a__app(X1, X2) -> app(X1, X2)
   a__prefix(X) -> prefix(X)
   a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(prefix(x_1)) = 0
POL(nil) = 0
POL(A__FROM(x_1)) = x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(MARK(x_1)) = x_1
POL(zWadr(x_1, x_2)) = x_1 + x_2
POL(a__app(x_1, x_2)) = x_1 + x_2
POL(a__prefix(x_1)) = 0
POL(cons(x_1, x_2)) = x_1
POL(a__zWadr(x_1, x_2)) = x_1 + x_2
POL(a__from(x_1)) = 1 + x_1
POL(from(x_1)) = 1 + x_1
POL(app(x_1, x_2)) = x_1 + x_2

 resulting in one subcycle.


SCC1.Polo1.Polo1.Polo1.Polo1:

MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

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(s(x_1)) = 1 + x_1
POL(MARK(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MARK(cons(X1, X2)) -> MARK(X1)
   MARK(s(X)) -> MARK(X)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 13.856 seconds.