Termination Proof using AProVE

Term Rewriting System R:
[X, XS, N, Y, YS, X1, X2]
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))
SEL(s(N), cons(X, XS)) -> ACTIVATE(XS)
MINUS(s(X), s(Y)) -> MINUS(X, Y)
QUOT(s(X), s(Y)) -> S(quot(minus(X, Y), s(Y)))
QUOT(s(X), s(Y)) -> QUOT(minus(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MINUS(X, Y)
ZWQUOT(cons(X, XS), cons(Y, YS)) -> QUOT(X, Y)
ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
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_{_zWquot}(X1, X2)) -> ZWQUOT(activate(X1), activate(X2))
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X1)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X2)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Size-Change Principle

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Neg POLO

       →DP Problem 4

         ↳SCP

Dependency Pair:

MINUS(s(X), s(Y)) -> MINUS(X, Y)

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

We number the DPs as follows:

MINUS(s(X), s(Y)) -> MINUS(X, Y)

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

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

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

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

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.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Negative Polynomial Order

       →DP Problem 3

         ↳Neg POLO

       →DP Problem 4

         ↳SCP

Dependency Pair:

QUOT(s(X), s(Y)) -> QUOT(minus(X, Y), s(Y))

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

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

QUOT(s(X), s(Y)) -> QUOT(minus(X, Y), s(Y))

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

minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
s(X) -> n_{_s}(X)

Used ordering:
Polynomial Order with Interpretation:

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

POL( s(x₁) ) = 1

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

POL( 0 ) = 0

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

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 3

         ↳Neg POLO

       →DP Problem 4

         ↳SCP

Dependency Pair:

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Negative Polynomial Order

       →DP Problem 4

         ↳SCP

Dependency Pairs:

ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X1)
ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ZWQUOT(activate(X1), activate(X2))
ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

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

ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(YS)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X2)
ACTIVATE(n_{_zWquot}(X1, X2)) -> ACTIVATE(X1)
ZWQUOT(cons(X, XS), cons(Y, YS)) -> ACTIVATE(XS)

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

activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X
from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
s(X) -> n_{_s}(X)
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)

Used ordering:
Polynomial Order with Interpretation:

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

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

POL( ACTIVATE(x₁) ) = x₁

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

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

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

POL( activate(x₁) ) = x₁

POL( from(x₁) ) = x₁

POL( s(x₁) ) = x₁

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

POL( nil ) = 0

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

POL( 0 ) = 0

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

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Neg POLO

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 4

         ↳SCP

Dependency Pairs:

ACTIVATE(n_{_zWquot}(X1, X2)) -> ZWQUOT(activate(X1), activate(X2))
ACTIVATE(n_{_s}(X)) -> ACTIVATE(X)
ACTIVATE(n_{_from}(X)) -> ACTIVATE(X)

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

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

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Neg POLO

           →DP Problem 6

             ↳DGraph

...

               →DP Problem 7

                 ↳Size-Change Principle

       →DP Problem 4

         ↳SCP

Dependency Pairs:

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

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

We number the DPs as follows:

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

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

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

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

{1, 2}	,	{1, 2}
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_{_from}(x₁) -> n_{_from}(x₁)
n_{_s}(x₁) -> n_{_s}(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Neg POLO

       →DP Problem 4

         ↳Size-Change Principle

Dependency Pair:

SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))

Rules:

from(X) -> cons(X, n_{_from}(n_{_s}(X)))
from(X) -> n_{_from}(X)
sel(0, cons(X, XS)) -> X
sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
minus(X, 0) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
zWquot(XS, nil) -> nil
zWquot(nil, XS) -> nil
zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n_{_zWquot}(activate(XS), activate(YS)))
zWquot(X1, X2) -> n_{_zWquot}(X1, X2)
s(X) -> n_{_s}(X)
activate(n_{_from}(X)) -> from(activate(X))
activate(n_{_s}(X)) -> s(activate(X))
activate(n_{_zWquot}(X1, X2)) -> zWquot(activate(X1), activate(X2))
activate(X) -> X

We number the DPs as follows:

SEL(s(N), cons(X, XS)) -> SEL(N, activate(XS))

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:

cons(x₁, x₂) -> cons(x₁, x₂)
s(x₁) -> s(x₁)

We obtain no new DP problems.

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