Termination Proof using AProVE

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))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_APP}(nil, YS) -> MARK(YS)
A_{_APP}(cons(X, XS), YS) -> MARK(X)
A_{_FROM}(X) -> MARK(X)
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(app(X1, X2)) -> A_{_APP}(mark(X1), mark(X2))
MARK(app(X1, X2)) -> MARK(X1)
MARK(app(X1, X2)) -> MARK(X2)
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(prefix(X)) -> A_{_PREFIX}(mark(X))
MARK(prefix(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Negative Polynomial Order

Dependency Pairs:

A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> MARK(X)
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(prefix(X)) -> MARK(X)
MARK(zWadr(X1, X2)) -> MARK(X2)
MARK(zWadr(X1, X2)) -> MARK(X1)
A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> MARK(Y)
A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> A_{_APP}(mark(Y), cons(mark(X), nil))
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(app(X1, X2)) -> MARK(X2)
MARK(app(X1, X2)) -> MARK(X1)
A_{_APP}(cons(X, XS), YS) -> MARK(X)
MARK(app(X1, X2)) -> A_{_APP}(mark(X1), mark(X2))
A_{_APP}(nil, YS) -> MARK(YS)

Rules:

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))

Strategy:

innermost

The following Dependency Pairs can be strictly oriented using the given order.

A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(prefix(X)) -> MARK(X)
A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> MARK(Y)
A_{_ZWADR}(cons(X, XS), cons(Y, YS)) -> A_{_APP}(mark(Y), cons(mark(X), nil))
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
A_{_APP}(cons(X, XS), YS) -> MARK(X)

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a_{_zWadr}(XS, nil) -> nil
mark(s(X)) -> s(mark(X))
mark(prefix(X)) -> a_{_prefix}(mark(X))
a_{_zWadr}(X1, X2) -> zWadr(X1, X2)
mark(nil) -> nil
a_{_app}(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(from(X)) -> a_{_from}(mark(X))
a_{_app}(nil, YS) -> mark(YS)
mark(zWadr(X1, X2)) -> a_{_zWadr}(mark(X1), mark(X2))
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_app}(X1, X2) -> app(X1, X2)
a_{_zWadr}(nil, YS) -> nil
a_{_from}(X) -> from(X)
a_{_prefix}(X) -> prefix(X)
a_{_zWadr}(cons(X, XS), cons(Y, YS)) -> cons(a_{_app}(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a_{_prefix}(L) -> cons(nil, zWadr(L, prefix(L)))
mark(app(X1, X2)) -> a_{_app}(mark(X1), mark(X2))

Used ordering:
Polynomial Order with Interpretation:

POL( A_{_ZWADR}(x₁, x₂) ) = x₁ + x₂

POL( cons(x₁, x₂) ) = x₁ + 1

POL( MARK(x₁) ) = x₁

POL( A_{_FROM}(x₁) ) = x₁

POL( app(x₁, x₂) ) = x₁ + x₂

POL( A_{_APP}(x₁, x₂) ) = x₁ + x₂

POL( mark(x₁) ) = x₁

POL( from(x₁) ) = x₁ + 1

POL( prefix(x₁) ) = x₁ + 1

POL( s(x₁) ) = x₁

POL( zWadr(x₁, x₂) ) = x₁ + x₂

POL( a_{_zWadr}(x₁, x₂) ) = x₁ + x₂

POL( nil ) = 0

POL( a_{_prefix}(x₁) ) = x₁ + 1

POL( a_{_app}(x₁, x₂) ) = x₁ + x₂

POL( a_{_from}(x₁) ) = x₁ + 1

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳Dependency Graph

Dependency Pairs:

MARK(s(X)) -> MARK(X)
MARK(zWadr(X1, X2)) -> MARK(X2)
MARK(zWadr(X1, X2)) -> MARK(X1)
MARK(zWadr(X1, X2)) -> A_{_ZWADR}(mark(X1), mark(X2))
A_{_FROM}(X) -> MARK(X)
MARK(app(X1, X2)) -> MARK(X2)
MARK(app(X1, X2)) -> MARK(X1)
MARK(app(X1, X2)) -> A_{_APP}(mark(X1), mark(X2))
A_{_APP}(nil, YS) -> MARK(YS)

Rules:

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))

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 3

                 ↳Negative Polynomial Order

Dependency Pairs:

MARK(zWadr(X1, X2)) -> MARK(X2)
MARK(zWadr(X1, X2)) -> MARK(X1)
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(s(X)) -> MARK(X)

Rules:

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))

Strategy:

innermost

The following Dependency Pairs can be strictly oriented using the given order.

MARK(zWadr(X1, X2)) -> MARK(X2)
MARK(zWadr(X1, X2)) -> MARK(X1)

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a_{_zWadr}(XS, nil) -> nil
mark(s(X)) -> s(mark(X))
mark(prefix(X)) -> a_{_prefix}(mark(X))
a_{_zWadr}(X1, X2) -> zWadr(X1, X2)
mark(nil) -> nil
a_{_app}(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(from(X)) -> a_{_from}(mark(X))
a_{_app}(nil, YS) -> mark(YS)
mark(zWadr(X1, X2)) -> a_{_zWadr}(mark(X1), mark(X2))
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_app}(X1, X2) -> app(X1, X2)
a_{_zWadr}(nil, YS) -> nil
a_{_from}(X) -> from(X)
a_{_prefix}(X) -> prefix(X)
a_{_zWadr}(cons(X, XS), cons(Y, YS)) -> cons(a_{_app}(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a_{_prefix}(L) -> cons(nil, zWadr(L, prefix(L)))
mark(app(X1, X2)) -> a_{_app}(mark(X1), mark(X2))

Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x₁) ) = x₁

POL( zWadr(x₁, x₂) ) = x₁ + x₂ + 1

POL( s(x₁) ) = x₁

POL( app(x₁, x₂) ) = x₁ + x₂

POL( A_{_APP}(x₁, x₂) ) = x₂

POL( mark(x₁) ) = x₁

POL( a_{_zWadr}(x₁, x₂) ) = x₁ + x₂ + 1

POL( nil ) = 0

POL( prefix(x₁) ) = 0

POL( a_{_prefix}(x₁) ) = 0

POL( a_{_app}(x₁, x₂) ) = x₁ + x₂

POL( cons(x₁, x₂) ) = 0

POL( from(x₁) ) = 0

POL( a_{_from}(x₁) ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 4

                 ↳Negative Polynomial Order

Dependency Pairs:

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(s(X)) -> MARK(X)

Rules:

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))

Strategy:

innermost

The following Dependency Pairs can be strictly oriented using the given order.

MARK(app(X1, X2)) -> MARK(X2)
MARK(app(X1, X2)) -> MARK(X1)
MARK(app(X1, X2)) -> A_{_APP}(mark(X1), mark(X2))

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a_{_zWadr}(XS, nil) -> nil
mark(s(X)) -> s(mark(X))
mark(prefix(X)) -> a_{_prefix}(mark(X))
a_{_zWadr}(X1, X2) -> zWadr(X1, X2)
mark(nil) -> nil
a_{_app}(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(from(X)) -> a_{_from}(mark(X))
a_{_app}(nil, YS) -> mark(YS)
mark(zWadr(X1, X2)) -> a_{_zWadr}(mark(X1), mark(X2))
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_app}(X1, X2) -> app(X1, X2)
a_{_zWadr}(nil, YS) -> nil
a_{_from}(X) -> from(X)
a_{_prefix}(X) -> prefix(X)
a_{_zWadr}(cons(X, XS), cons(Y, YS)) -> cons(a_{_app}(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a_{_prefix}(L) -> cons(nil, zWadr(L, prefix(L)))
mark(app(X1, X2)) -> a_{_app}(mark(X1), mark(X2))

Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x₁) ) = x₁

POL( app(x₁, x₂) ) = x₁ + x₂ + 1

POL( A_{_APP}(x₁, x₂) ) = x₂

POL( mark(x₁) ) = x₁

POL( s(x₁) ) = x₁

POL( a_{_zWadr}(x₁, x₂) ) = 0

POL( nil ) = 0

POL( prefix(x₁) ) = 0

POL( a_{_prefix}(x₁) ) = 0

POL( zWadr(x₁, x₂) ) = 0

POL( a_{_app}(x₁, x₂) ) = x₁ + x₂ + 1

POL( cons(x₁, x₂) ) = 0

POL( from(x₁) ) = 0

POL( a_{_from}(x₁) ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 5

                 ↳Dependency Graph

Dependency Pairs:

A_{_APP}(nil, YS) -> MARK(YS)
MARK(s(X)) -> MARK(X)

Rules:

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))

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 6

                 ↳Usable Rules (Innermost)

Dependency Pair:

MARK(s(X)) -> MARK(X)

Rules:

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))

Strategy:

innermost

As we are in the innermost case, we can delete all 18 non-usable-rules.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 7

                 ↳Size-Change Principle

Dependency Pair:

MARK(s(X)) -> MARK(X)

Rule:

none

Strategy:

innermost

We number the DPs as follows:

MARK(s(X)) -> MARK(X)

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1

D_P: empty set
Oriented Rules: none

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

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:18 minutes