Term Rewriting System R:
[X, Y, M, N, X1, X2, X3]
afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

AFILTER(cons(X, Y), s(N), M) -> MARK(X)
ASIEVE(cons(s(N), Y)) -> MARK(N)
ANATS(N) -> MARK(N)
AZPRIMES -> ASIEVE(anats(s(s(0))))
AZPRIMES -> ANATS(s(s(0)))
MARK(filter(X1, X2, X3)) -> AFILTER(mark(X1), mark(X2), mark(X3))
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(sieve(X)) -> ASIEVE(mark(X))
MARK(sieve(X)) -> MARK(X)
MARK(nats(X)) -> ANATS(mark(X))
MARK(nats(X)) -> MARK(X)
MARK(zprimes) -> AZPRIMES
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Polynomial Ordering


Dependency Pairs:

MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
AZPRIMES -> ANATS(s(s(0)))
AZPRIMES -> ASIEVE(anats(s(s(0))))
MARK(zprimes) -> AZPRIMES
MARK(nats(X)) -> MARK(X)
ANATS(N) -> MARK(N)
MARK(nats(X)) -> ANATS(mark(X))
MARK(sieve(X)) -> MARK(X)
ASIEVE(cons(s(N), Y)) -> MARK(N)
MARK(sieve(X)) -> ASIEVE(mark(X))
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> AFILTER(mark(X1), mark(X2), mark(X3))
AFILTER(cons(X, Y), s(N), M) -> MARK(X)


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

MARK(cons(X1, X2)) -> MARK(X1)
AZPRIMES -> ANATS(s(s(0)))
MARK(nats(X)) -> MARK(X)
MARK(nats(X)) -> ANATS(mark(X))
ASIEVE(cons(s(N), Y)) -> MARK(N)
AFILTER(cons(X, Y), s(N), M) -> MARK(X)


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

anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(A__ZPRIMES)=  1  
  POL(a__nats(x1))=  1 + x1  
  POL(filter(x1, x2, x3))=  x1 + x2 + x3  
  POL(MARK(x1))=  x1  
  POL(A__NATS(x1))=  x1  
  POL(A__FILTER(x1, x2, x3))=  x1  
  POL(mark(x1))=  x1  
  POL(zprimes)=  1  
  POL(A__SIEVE(x1))=  x1  
  POL(sieve(x1))=  x1  
  POL(0)=  0  
  POL(cons(x1, x2))=  1 + x1  
  POL(a__zprimes)=  1  
  POL(nats(x1))=  1 + x1  
  POL(s(x1))=  x1  
  POL(a__sieve(x1))=  x1  
  POL(a__filter(x1, x2, x3))=  x1 + x2 + x3  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 2
             ↳Dependency Graph


Dependency Pairs:

MARK(s(X)) -> MARK(X)
AZPRIMES -> ASIEVE(anats(s(s(0))))
MARK(zprimes) -> AZPRIMES
ANATS(N) -> MARK(N)
MARK(sieve(X)) -> MARK(X)
MARK(sieve(X)) -> ASIEVE(mark(X))
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(filter(X1, X2, X3)) -> AFILTER(mark(X1), mark(X2), mark(X3))


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




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


   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 2
             ↳DGraph
             ...
               →DP Problem 3
                 ↳Polynomial Ordering


Dependency Pairs:

MARK(sieve(X)) -> MARK(X)
MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(s(X)) -> MARK(X)


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MARK(sieve(X)) -> MARK(X)


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(x1, x2, x3))=  x1 + x2 + x3  
  POL(sieve(x1))=  1 + x1  
  POL(MARK(x1))=  x1  
  POL(s(x1))=  x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 2
             ↳DGraph
             ...
               →DP Problem 4
                 ↳Polynomial Ordering


Dependency Pairs:

MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)
MARK(s(X)) -> MARK(X)


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

MARK(filter(X1, X2, X3)) -> MARK(X3)
MARK(filter(X1, X2, X3)) -> MARK(X2)
MARK(filter(X1, X2, X3)) -> MARK(X1)


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(x1, x2, x3))=  1 + x1 + x2 + x3  
  POL(MARK(x1))=  x1  
  POL(s(x1))=  x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 2
             ↳DGraph
             ...
               →DP Problem 5
                 ↳Polynomial Ordering


Dependency Pair:

MARK(s(X)) -> MARK(X)


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MARK(s(X)) -> MARK(X)


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(MARK(x1))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 2
             ↳DGraph
             ...
               →DP Problem 6
                 ↳Dependency Graph


Dependency Pair:


Rules:


afilter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
afilter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M))
afilter(X1, X2, X3) -> filter(X1, X2, X3)
asieve(cons(0, Y)) -> cons(0, sieve(Y))
asieve(cons(s(N), Y)) -> cons(s(mark(N)), sieve(filter(Y, N, N)))
asieve(X) -> sieve(X)
anats(N) -> cons(mark(N), nats(s(N)))
anats(X) -> nats(X)
azprimes -> asieve(anats(s(s(0))))
azprimes -> zprimes
mark(filter(X1, X2, X3)) -> afilter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) -> asieve(mark(X))
mark(nats(X)) -> anats(mark(X))
mark(zprimes) -> azprimes
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(0) -> 0
mark(s(X)) -> s(mark(X))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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