Termination Proof using AProVE

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}(n_{_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, n_{_prefix}(L)))
prefix(X) -> n_{_prefix}(X)
s(X) -> n_{_s}(X)
nil -> n_{_nil}
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

Innermost Termination of R to be shown.

     ↳Removing Redundant Rules for Innermost Termination

Removing the following rules from R which left hand sides contain non normal subterms

app(nil, YS) -> YS
zWadr(nil, YS) -> nil
zWadr(XS, nil) -> nil

     ↳RRRI

       →TRS2

         ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APP(cons(X, XS), YS) -> ACTIVATE(XS)
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)
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

Furthermore, R contains one SCC.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Narrowing Transformation

Dependency Pairs:

ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ACTIVATE(n_{_prefix}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, n_{_nil}))
ACTIVATE(n_{_zWadr}(X1, X2)) -> ZWADR(activate(X1), activate(X2))
ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_app}(X1, X2)) -> APP(activate(X1), activate(X2))
APP(cons(X, XS), YS) -> ACTIVATE(XS)

Rules:

app(cons(X, XS), YS) -> cons(X, n_{_app}(activate(XS), YS))
app(X1, X2) -> n_{_app}(X1, X2)
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
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
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, n_{_prefix}(L)))
prefix(X) -> n_{_prefix}(X)
nil -> n_{_nil}
s(X) -> n_{_s}(X)

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(n_{_app}(X1, X2)) -> APP(activate(X1), activate(X2))

14 new Dependency Pairs are created:

ACTIVATE(n_{_app}(n_{_app}(X1'', X2''), X2)) -> APP(app(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_app}(n_{_from}(X'), X2)) -> APP(from(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_s}(X'), X2)) -> APP(s(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_nil}, X2)) -> APP(nil, activate(X2))
ACTIVATE(n_{_app}(n_{_zWadr}(X1'', X2''), X2)) -> APP(zWadr(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_app}(n_{_prefix}(X'), X2)) -> APP(prefix(activate(X')), activate(X2))
ACTIVATE(n_{_app}(X1', X2)) -> APP(X1', activate(X2))
ACTIVATE(n_{_app}(X1, n_{_app}(X1'', X2''))) -> APP(activate(X1), app(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1, n_{_from}(X'))) -> APP(activate(X1), from(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_s}(X'))) -> APP(activate(X1), s(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_nil})) -> APP(activate(X1), nil)
ACTIVATE(n_{_app}(X1, n_{_zWadr}(X1'', X2''))) -> APP(activate(X1), zWadr(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1, n_{_prefix}(X'))) -> APP(activate(X1), prefix(activate(X')))
ACTIVATE(n_{_app}(X1, X2')) -> APP(activate(X1), X2')

The transformation is resulting in one new DP problem:

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Nar

...

               →DP Problem 2

                 ↳Narrowing Transformation

Dependency Pairs:

ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ACTIVATE(n_{_app}(X1, X2')) -> APP(activate(X1), X2')
ACTIVATE(n_{_app}(X1, n_{_prefix}(X'))) -> APP(activate(X1), prefix(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_zWadr}(X1'', X2''))) -> APP(activate(X1), zWadr(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1, n_{_nil})) -> APP(activate(X1), nil)
ACTIVATE(n_{_app}(X1, n_{_s}(X'))) -> APP(activate(X1), s(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_from}(X'))) -> APP(activate(X1), from(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_app}(X1'', X2''))) -> APP(activate(X1), app(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1', X2)) -> APP(X1', activate(X2))
ACTIVATE(n_{_app}(n_{_prefix}(X'), X2)) -> APP(prefix(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_zWadr}(X1'', X2''), X2)) -> APP(zWadr(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_app}(n_{_nil}, X2)) -> APP(nil, activate(X2))
ACTIVATE(n_{_app}(n_{_s}(X'), X2)) -> APP(s(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_from}(X'), X2)) -> APP(from(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_app}(X1'', X2''), X2)) -> APP(app(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_prefix}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X1)
APP(cons(X, XS), YS) -> ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, n_{_nil}))
ACTIVATE(n_{_zWadr}(X1, X2)) -> ZWADR(activate(X1), activate(X2))
ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)

Rules:

app(cons(X, XS), YS) -> cons(X, n_{_app}(activate(XS), YS))
app(X1, X2) -> n_{_app}(X1, X2)
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
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
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, n_{_prefix}(L)))
prefix(X) -> n_{_prefix}(X)
nil -> n_{_nil}
s(X) -> n_{_s}(X)

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

ACTIVATE(n_{_zWadr}(X1, X2)) -> ZWADR(activate(X1), activate(X2))

14 new Dependency Pairs are created:

ACTIVATE(n_{_zWadr}(n_{_app}(X1'', X2''), X2)) -> ZWADR(app(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_from}(X'), X2)) -> ZWADR(from(activate(X')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_s}(X'), X2)) -> ZWADR(s(activate(X')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_nil}, X2)) -> ZWADR(nil, activate(X2))
ACTIVATE(n_{_zWadr}(n_{_zWadr}(X1'', X2''), X2)) -> ZWADR(zWadr(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_prefix}(X'), X2)) -> ZWADR(prefix(activate(X')), activate(X2))
ACTIVATE(n_{_zWadr}(X1', X2)) -> ZWADR(X1', activate(X2))
ACTIVATE(n_{_zWadr}(X1, n_{_app}(X1'', X2''))) -> ZWADR(activate(X1), app(activate(X1''), activate(X2'')))
ACTIVATE(n_{_zWadr}(X1, n_{_from}(X'))) -> ZWADR(activate(X1), from(activate(X')))
ACTIVATE(n_{_zWadr}(X1, n_{_s}(X'))) -> ZWADR(activate(X1), s(activate(X')))
ACTIVATE(n_{_zWadr}(X1, n_{_nil})) -> ZWADR(activate(X1), nil)
ACTIVATE(n_{_zWadr}(X1, n_{_zWadr}(X1'', X2''))) -> ZWADR(activate(X1), zWadr(activate(X1''), activate(X2'')))
ACTIVATE(n_{_zWadr}(X1, n_{_prefix}(X'))) -> ZWADR(activate(X1), prefix(activate(X')))
ACTIVATE(n_{_zWadr}(X1, X2')) -> ZWADR(activate(X1), X2')

The transformation is resulting in one new DP problem:

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Nar

...

               →DP Problem 3

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

ACTIVATE(n_{_zWadr}(X1, X2')) -> ZWADR(activate(X1), X2')
ACTIVATE(n_{_zWadr}(X1, n_{_prefix}(X'))) -> ZWADR(activate(X1), prefix(activate(X')))
ACTIVATE(n_{_zWadr}(X1, n_{_zWadr}(X1'', X2''))) -> ZWADR(activate(X1), zWadr(activate(X1''), activate(X2'')))
ACTIVATE(n_{_zWadr}(X1, n_{_nil})) -> ZWADR(activate(X1), nil)
ACTIVATE(n_{_zWadr}(X1, n_{_s}(X'))) -> ZWADR(activate(X1), s(activate(X')))
ACTIVATE(n_{_zWadr}(X1, n_{_from}(X'))) -> ZWADR(activate(X1), from(activate(X')))
ACTIVATE(n_{_zWadr}(X1, n_{_app}(X1'', X2''))) -> ZWADR(activate(X1), app(activate(X1''), activate(X2'')))
ACTIVATE(n_{_zWadr}(X1', X2)) -> ZWADR(X1', activate(X2))
ACTIVATE(n_{_zWadr}(n_{_prefix}(X'), X2)) -> ZWADR(prefix(activate(X')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_zWadr}(X1'', X2''), X2)) -> ZWADR(zWadr(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_nil}, X2)) -> ZWADR(nil, activate(X2))
ACTIVATE(n_{_zWadr}(n_{_s}(X'), X2)) -> ZWADR(s(activate(X')), activate(X2))
ACTIVATE(n_{_zWadr}(n_{_from}(X'), X2)) -> ZWADR(from(activate(X')), activate(X2))
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ZWADR(cons(X, XS), cons(Y, YS)) -> APP(Y, cons(X, n_{_nil}))
ACTIVATE(n_{_zWadr}(n_{_app}(X1'', X2''), X2)) -> ZWADR(app(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_app}(X1, X2')) -> APP(activate(X1), X2')
ACTIVATE(n_{_app}(X1, n_{_prefix}(X'))) -> APP(activate(X1), prefix(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_zWadr}(X1'', X2''))) -> APP(activate(X1), zWadr(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1, n_{_nil})) -> APP(activate(X1), nil)
ACTIVATE(n_{_app}(X1, n_{_s}(X'))) -> APP(activate(X1), s(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_from}(X'))) -> APP(activate(X1), from(activate(X')))
ACTIVATE(n_{_app}(X1, n_{_app}(X1'', X2''))) -> APP(activate(X1), app(activate(X1''), activate(X2'')))
ACTIVATE(n_{_app}(X1', X2)) -> APP(X1', activate(X2))
ACTIVATE(n_{_app}(n_{_prefix}(X'), X2)) -> APP(prefix(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_zWadr}(X1'', X2''), X2)) -> APP(zWadr(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_app}(n_{_nil}, X2)) -> APP(nil, activate(X2))
ACTIVATE(n_{_app}(n_{_s}(X'), X2)) -> APP(s(activate(X')), activate(X2))
ACTIVATE(n_{_app}(n_{_from}(X'), X2)) -> APP(from(activate(X')), activate(X2))
APP(cons(X, XS), YS) -> ACTIVATE(XS)
ACTIVATE(n_{_app}(n_{_app}(X1'', X2''), X2)) -> APP(app(activate(X1''), activate(X2'')), activate(X2))
ACTIVATE(n_{_prefix}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_zWadr}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_app}(X1, X2)) -> ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)

Rules:

app(cons(X, XS), YS) -> cons(X, n_{_app}(activate(XS), YS))
app(X1, X2) -> n_{_app}(X1, X2)
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
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
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, n_{_prefix}(L)))
prefix(X) -> n_{_prefix}(X)
nil -> n_{_nil}
s(X) -> n_{_s}(X)

The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:00 minutes