Termination Proof using AProVE

Term Rewriting System R:
[X, Y, Z, X1, X2]
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FIRST(s(X), cons(Y, Z)) -> ACTIVATE(Z)
ACTIVATE(n_{_first}(X1, X2)) -> FIRST(activate(X1), activate(X2))
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_first}(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)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Negative Polynomial Order

Dependency Pairs:

ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_first}(X1, X2)) -> FIRST(activate(X1), activate(X2))
FIRST(s(X), cons(Y, Z)) -> ACTIVATE(Z)

Rules:

first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X

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

ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)

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

activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)

Used ordering:
Polynomial Order with Interpretation:

POL( ACTIVATE(x₁) ) = x₁

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

POL( n_{_first}(x₁, x₂) ) = x₁ + x₂

POL( FIRST(x₁, x₂) ) = x₂

POL( activate(x₁) ) = x₁

POL( n_{_s}(x₁) ) = x₁

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

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

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

POL( s(x₁) ) = x₁

POL( 0 ) = 0

POL( nil ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳Negative Polynomial Order

Dependency Pairs:

ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_first}(X1, X2)) -> FIRST(activate(X1), activate(X2))
FIRST(s(X), cons(Y, Z)) -> ACTIVATE(Z)

Rules:

first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X

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

ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)

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

activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)

Used ordering:
Polynomial Order with Interpretation:

POL( ACTIVATE(x₁) ) = x₁

POL( n_{_s}(x₁) ) = x₁ + 1

POL( n_{_first}(x₁, x₂) ) = x₁ + x₂

POL( FIRST(x₁, x₂) ) = x₂

POL( activate(x₁) ) = x₁

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

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

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

POL( from(x₁) ) = 0

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

POL( 0 ) = 0

POL( nil ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 3

                 ↳Negative Polynomial Order

Dependency Pairs:

ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_first}(X1, X2)) -> FIRST(activate(X1), activate(X2))
FIRST(s(X), cons(Y, Z)) -> ACTIVATE(Z)

Rules:

first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X

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

ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_first}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_first}(X1, X2)) -> FIRST(activate(X1), activate(X2))

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

activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X
first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)

Used ordering:
Polynomial Order with Interpretation:

POL( ACTIVATE(x₁) ) = x₁

POL( n_{_first}(x₁, x₂) ) = x₁ + x₂ + 1

POL( FIRST(x₁, x₂) ) = x₂

POL( activate(x₁) ) = x₁

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

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

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

POL( from(x₁) ) = 0

POL( n_{_s}(x₁) ) = x₁

POL( s(x₁) ) = x₁

POL( 0 ) = 0

POL( nil ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Neg POLO

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 4

                 ↳Dependency Graph

Dependency Pair:

FIRST(s(X), cons(Y, Z)) -> ACTIVATE(Z)

Rules:

first(0, X) -> nil
first(s(X), cons(Y, Z)) -> cons(Y, n_{_first}(X, activate(Z)))
first(X1, X2) -> n_{_first}(X1, X2)
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
activate(n_{_first}(X1, X2)) -> first(activate(X1), activate(X2))
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(X) -> X

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes