Termination Proof using AProVE

Term Rewriting System R:
[X, Y, M, N, X1, X2, X3]
filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)
SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
ZPRIMES -> SIEVE(nats(s(s(0))))
ZPRIMES -> NATS(s(s(0)))
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
ACTIVATE(n_{_nats}(X)) -> NATS(X)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

Dependency Pairs:

SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)
ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

The following dependency pairs can be strictly oriented:

SIEVE(cons(s(N), Y)) -> ACTIVATE(Y)
SIEVE(cons(s(N), Y)) -> FILTER(activate(Y), N, N)
SIEVE(cons(0, Y)) -> ACTIVATE(Y)

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(filter(x₁, x₂, x₃)) = x₁

POL(activate(x₁)) = x₁

POL(FILTER(x₁, x₂, x₃)) = x₁

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

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

POL(ACTIVATE(x₁)) = x₁

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

POL(0) = 0

POL(n__filter(x₁, x₂, x₃)) = x₁

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

POL(n__nats(x₁)) = 0

POL(nats(x₁)) = 0

POL(s(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳Dependency Graph

Dependency Pairs:

ACTIVATE(n_{_sieve}(X)) -> SIEVE(X)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 3

                 ↳Polynomial Ordering

Dependency Pairs:

FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)
ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

The following dependency pair can be strictly oriented:

FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(FILTER(x₁, x₂, x₃)) = x₁ + x₂

POL(0) = 1

POL(n__filter(x₁, x₂, x₃)) = x₁ + x₂

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

POL(s(x₁)) = 0

POL(ACTIVATE(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 4

                 ↳Polynomial Ordering

Dependency Pairs:

ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)
FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

The following dependency pair can be strictly oriented:

ACTIVATE(n_{_filter}(X1, X2, X3)) -> FILTER(X1, X2, X3)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(n__filter(x₁, x₂, x₃)) = 1 + x₁

POL(FILTER(x₁, x₂, x₃)) = x₁

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

POL(s(x₁)) = 0

POL(ACTIVATE(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 5

                 ↳Dependency Graph

Dependency Pair:

FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y)

Rules:

filter(cons(X, Y), 0, M) -> cons(0, n_{_filter}(activate(Y), M, M))
filter(cons(X, Y), s(N), M) -> cons(X, n_{_filter}(activate(Y), N, M))
filter(X1, X2, X3) -> n_{_filter}(X1, X2, X3)
sieve(cons(0, Y)) -> cons(0, n_{_sieve}(activate(Y)))
sieve(cons(s(N), Y)) -> cons(s(N), n_{_sieve}(filter(activate(Y), N, N)))
sieve(X) -> n_{_sieve}(X)
nats(N) -> cons(N, n_{_nats}(s(N)))
nats(X) -> n_{_nats}(X)
zprimes -> sieve(nats(s(s(0))))
activate(n_{_filter}(X1, X2, X3)) -> filter(X1, X2, X3)
activate(n_{_sieve}(X)) -> sieve(X)
activate(n_{_nats}(X)) -> nats(X)
activate(X) -> X

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

POL(filter(x₁, x₂, x₃))	= x₁
POL(activate(x₁))	= x₁
POL(FILTER(x₁, x₂, x₃))	= x₁
POL(SIEVE(x₁))	= 1 + x₁
POL(n__sieve(x₁))	= 1 + x₁
POL(ACTIVATE(x₁))	= x₁
POL(sieve(x₁))	= 1 + x₁
POL(0)	= 0
POL(n__filter(x₁, x₂, x₃))	= x₁
POL(cons(x₁, x₂))	= x₂
POL(n__nats(x₁))	= 0
POL(nats(x₁))	= 0
POL(s(x₁))	= 0

POL(FILTER(x₁, x₂, x₃))	= x₁ + x₂
POL(0)	= 1
POL(n__filter(x₁, x₂, x₃))	= x₁ + x₂
POL(cons(x₁, x₂))	= x₂
POL(s(x₁))	= 0
POL(ACTIVATE(x₁))	= x₁