Termination Proof using AProVE

Term Rewriting System R:
[X, Y, L, X1, X2]
eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(0, X) -> nil
take(s(X), cons(Y, L)) -> cons(activate(Y), n_{_take}(activate(X), activate(L)))
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(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

take(0, X) -> nil
take(s(X), cons(Y, L)) -> cons(activate(Y), n_{_take}(activate(X), activate(L)))

     ↳RRRI

       →TRS2

         ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

EQ(n_{_s}(X), n_{_s}(Y)) -> EQ(activate(X), activate(Y))
EQ(n_{_s}(X), n_{_s}(Y)) -> ACTIVATE(X)
EQ(n_{_s}(X), n_{_s}(Y)) -> ACTIVATE(Y)
ACTIVATE(n_₀) -> 0'
ACTIVATE(n_{_s}(X)) -> S(X)
ACTIVATE(n_{_inf}(X)) -> INF(activate(X))
ACTIVATE(n_{_inf}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_take}(X1, X2)) -> TAKE(activate(X1), activate(X2))
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_length}(X)) -> LENGTH(activate(X))
ACTIVATE(n_{_length}(X)) -> ACTIVATE(X)
LENGTH(nil) -> 0'
LENGTH(cons(X, L)) -> S(n_{_length}(activate(L)))
LENGTH(cons(X, L)) -> ACTIVATE(L)

Furthermore, R contains two SCCs.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Negative Polynomial Order

           →DP Problem 2

             ↳Nar

Dependency Pairs:

ACTIVATE(n_{_length}(X)) -> ACTIVATE(X)
LENGTH(cons(X, L)) -> ACTIVATE(L)
ACTIVATE(n_{_length}(X)) -> LENGTH(activate(X))
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_inf}(X)) -> ACTIVATE(X)

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

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

ACTIVATE(n_{_length}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_length}(X)) -> LENGTH(activate(X))

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

activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
0 -> n_₀
s(X) -> n_{_s}(X)
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)

Used ordering:
Polynomial Order with Interpretation:

POL( ACTIVATE(x₁) ) = x₁

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

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

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

POL( LENGTH(x₁) ) = x₁

POL( activate(x₁) ) = x₁

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

POL( n_₀ ) = 0

POL( 0 ) = 0

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

POL( s(x₁) ) = 0

POL( inf(x₁) ) = x₁

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

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

This results in one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

...

               →DP Problem 3

                 ↳Dependency Graph

           →DP Problem 2

             ↳Nar

Dependency Pairs:

LENGTH(cons(X, L)) -> ACTIVATE(L)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_inf}(X)) -> ACTIVATE(X)

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

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

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

...

               →DP Problem 4

                 ↳Size-Change Principle

           →DP Problem 2

             ↳Nar

Dependency Pairs:

ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_inf}(X)) -> ACTIVATE(X)

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

We number the DPs as follows:

ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_take}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_inf}(X)) -> ACTIVATE(X)

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

{3, 2, 1}	,	{3, 2, 1}
1	>	1

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

{3, 2, 1}	,	{3, 2, 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:

n_{_inf}(x₁) -> n_{_inf}(x₁)
n_{_take}(x₁, x₂) -> n_{_take}(x₁, x₂)

We obtain no new DP problems.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pair:

EQ(n_{_s}(X), n_{_s}(Y)) -> EQ(activate(X), activate(Y))

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

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

EQ(n_{_s}(X), n_{_s}(Y)) -> EQ(activate(X), activate(Y))

12 new Dependency Pairs are created:

EQ(n_{_s}(n_₀), n_{_s}(Y)) -> EQ(0, activate(Y))
EQ(n_{_s}(n_{_s}(X'')), n_{_s}(Y)) -> EQ(s(X''), activate(Y))
EQ(n_{_s}(n_{_inf}(X'')), n_{_s}(Y)) -> EQ(inf(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_take}(X1', X2')), n_{_s}(Y)) -> EQ(take(activate(X1'), activate(X2')), activate(Y))
EQ(n_{_s}(n_{_length}(X'')), n_{_s}(Y)) -> EQ(length(activate(X'')), activate(Y))
EQ(n_{_s}(X''), n_{_s}(Y)) -> EQ(X'', activate(Y))
EQ(n_{_s}(X), n_{_s}(n_₀)) -> EQ(activate(X), 0)
EQ(n_{_s}(X), n_{_s}(n_{_s}(X''))) -> EQ(activate(X), s(X''))
EQ(n_{_s}(X), n_{_s}(n_{_inf}(X''))) -> EQ(activate(X), inf(activate(X'')))
EQ(n_{_s}(X), n_{_s}(n_{_take}(X1', X2'))) -> EQ(activate(X), take(activate(X1'), activate(X2')))
EQ(n_{_s}(X), n_{_s}(n_{_length}(X''))) -> EQ(activate(X), length(activate(X'')))
EQ(n_{_s}(X), n_{_s}(Y')) -> EQ(activate(X), Y')

The transformation is resulting in one new DP problem:

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Negative Polynomial Order

Dependency Pairs:

EQ(n_{_s}(X), n_{_s}(Y')) -> EQ(activate(X), Y')
EQ(n_{_s}(X), n_{_s}(n_{_length}(X''))) -> EQ(activate(X), length(activate(X'')))
EQ(n_{_s}(X), n_{_s}(n_{_take}(X1', X2'))) -> EQ(activate(X), take(activate(X1'), activate(X2')))
EQ(n_{_s}(X), n_{_s}(n_{_inf}(X''))) -> EQ(activate(X), inf(activate(X'')))
EQ(n_{_s}(X), n_{_s}(n_{_s}(X''))) -> EQ(activate(X), s(X''))
EQ(n_{_s}(X), n_{_s}(n_₀)) -> EQ(activate(X), 0)
EQ(n_{_s}(X''), n_{_s}(Y)) -> EQ(X'', activate(Y))
EQ(n_{_s}(n_{_length}(X'')), n_{_s}(Y)) -> EQ(length(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_take}(X1', X2')), n_{_s}(Y)) -> EQ(take(activate(X1'), activate(X2')), activate(Y))
EQ(n_{_s}(n_{_inf}(X'')), n_{_s}(Y)) -> EQ(inf(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_s}(X'')), n_{_s}(Y)) -> EQ(s(X''), activate(Y))
EQ(n_{_s}(n_₀), n_{_s}(Y)) -> EQ(0, activate(Y))

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

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

EQ(n_{_s}(X), n_{_s}(Y')) -> EQ(activate(X), Y')
EQ(n_{_s}(X), n_{_s}(n_{_take}(X1', X2'))) -> EQ(activate(X), take(activate(X1'), activate(X2')))
EQ(n_{_s}(X), n_{_s}(n_{_inf}(X''))) -> EQ(activate(X), inf(activate(X'')))
EQ(n_{_s}(X), n_{_s}(n_{_s}(X''))) -> EQ(activate(X), s(X''))
EQ(n_{_s}(X), n_{_s}(n_₀)) -> EQ(activate(X), 0)

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

activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
take(X1, X2) -> n_{_take}(X1, X2)
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
s(X) -> n_{_s}(X)
0 -> n_₀

Used ordering:
Polynomial Order with Interpretation:

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

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

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

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

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

POL( inf(x₁) ) = 0

POL( n_₀ ) = 0

POL( 0 ) = 0

POL( n_{_take}(x₁, x₂) ) = 0

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

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

POL( length(x₁) ) = 1

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

This results in one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Negative Polynomial Order

Dependency Pairs:

EQ(n_{_s}(X), n_{_s}(n_{_length}(X''))) -> EQ(activate(X), length(activate(X'')))
EQ(n_{_s}(X''), n_{_s}(Y)) -> EQ(X'', activate(Y))
EQ(n_{_s}(n_{_length}(X'')), n_{_s}(Y)) -> EQ(length(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_take}(X1', X2')), n_{_s}(Y)) -> EQ(take(activate(X1'), activate(X2')), activate(Y))
EQ(n_{_s}(n_{_inf}(X'')), n_{_s}(Y)) -> EQ(inf(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_s}(X'')), n_{_s}(Y)) -> EQ(s(X''), activate(Y))
EQ(n_{_s}(n_₀), n_{_s}(Y)) -> EQ(0, activate(Y))

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
s(X) -> n_{_s}(X)

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

EQ(n_{_s}(X''), n_{_s}(Y)) -> EQ(X'', activate(Y))
EQ(n_{_s}(n_{_take}(X1', X2')), n_{_s}(Y)) -> EQ(take(activate(X1'), activate(X2')), activate(Y))
EQ(n_{_s}(n_{_inf}(X'')), n_{_s}(Y)) -> EQ(inf(activate(X'')), activate(Y))
EQ(n_{_s}(n_{_s}(X'')), n_{_s}(Y)) -> EQ(s(X''), activate(Y))
EQ(n_{_s}(n_₀), n_{_s}(Y)) -> EQ(0, activate(Y))

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

activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
take(X1, X2) -> n_{_take}(X1, X2)
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
s(X) -> n_{_s}(X)
0 -> n_₀

Used ordering:
Polynomial Order with Interpretation:

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

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

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

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

POL( inf(x₁) ) = 0

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

POL( length(x₁) ) = 1

POL( n_{_take}(x₁, x₂) ) = 0

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

POL( n_₀ ) = 0

POL( 0 ) = 0

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

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

This results in one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Neg POLO

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

EQ(n_{_s}(X), n_{_s}(n_{_length}(X''))) -> EQ(activate(X), length(activate(X'')))
EQ(n_{_s}(n_{_length}(X'')), n_{_s}(Y)) -> EQ(length(activate(X'')), activate(Y))

Rules:

eq(n_₀, n_₀) -> true
eq(n_{_s}(X), n_{_s}(Y)) -> eq(activate(X), activate(Y))
eq(X, Y) -> false
activate(n_₀) -> 0
activate(n_{_s}(X)) -> s(X)
activate(n_{_inf}(X)) -> inf(activate(X))
activate(n_{_take}(X1, X2)) -> take(activate(X1), activate(X2))
activate(n_{_length}(X)) -> length(activate(X))
activate(X) -> X
inf(X) -> cons(X, n_{_inf}(n_{_s}(X)))
inf(X) -> n_{_inf}(X)
take(X1, X2) -> n_{_take}(X1, X2)
length(nil) -> 0
length(cons(X, L)) -> s(n_{_length}(activate(L)))
length(X) -> n_{_length}(X)
0 -> n_₀
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