Term Rewriting System R:
[X, Y, M, N]
filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))

Termination of R to be shown. 



   R
     ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳OC
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
SIEVE(cons(0, Y)) -> SIEVE(Y)
SIEVE(cons(s(N), Y)) -> SIEVE(filter(Y, N, N))
SIEVE(cons(s(N), Y)) -> FILTER(Y, N, N)
NATS(N) -> NATS(s(N))
ZPRIMES -> SIEVE(nats(s(s(0))))
ZPRIMES -> NATS(s(s(0)))

Furthermore, R contains three SCCs. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Usable Rules (Innermost)
           →DP Problem 2
             ↳UsableRules


Dependency Pairs:

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


Rules:


filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))


Strategy:

innermost




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


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
             ...
               →DP Problem 4
                 ↳Size-Change Principle
           →DP Problem 2
             ↳UsableRules


Dependency Pairs:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. FILTER(cons(X, Y), s(N), M) -> FILTER(Y, N, M)
  2. FILTER(cons(X, Y), 0, M) -> FILTER(Y, M, M)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1>1
2>2
3=3
{1, 2} , {1, 2}
1>1
3=2
3=3

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1>1
2>2
3=3
{1, 2} , {1, 2}
1>1
3=2
3=3
{1, 2} , {1, 2}
1>1
3>2
3=3

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳Usable Rules (Innermost)


Dependency Pair:

NATS(N) -> NATS(s(N))


Rules:


filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
sieve(cons(0, Y)) -> cons(0, sieve(Y))
sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
nats(N) -> cons(N, nats(s(N)))
zprimes -> sieve(nats(s(s(0))))


Strategy:

innermost




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


   R
     ↳OC
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳UsableRules
           →DP Problem 2
             ↳UsableRules
             ...
               →DP Problem 5
                 ↳Non Termination


Dependency Pair:

NATS(N) -> NATS(s(N))


Rule:

none


Strategy:

innermost




Found an infinite P-chain over R:
P =

NATS(N) -> NATS(s(N))

R = none

s = NATS(N)
evaluates to t =NATS(s(N))

Thus, s starts an infinite chain as s matches t.

Non-Termination of R could be shown.
Duration:
0:01 minutes