MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
zprimes() -> sieve(nats(s(s(0()))))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0} / {0/0,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,filter,nats,sieve,zprimes} and constructors {0
,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
activate#(X) -> c_1()
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__nats(X)) -> c_3(nats#(X))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(X1,X2,X3) -> c_5()
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
activate#(X) -> c_1()
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__nats(X)) -> c_3(nats#(X))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(X1,X2,X3) -> c_5()
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
zprimes() -> sieve(nats(s(s(0()))))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
activate#(X) -> c_1()
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__nats(X)) -> c_3(nats#(X))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(X1,X2,X3) -> c_5()
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
activate#(X) -> c_1()
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__nats(X)) -> c_3(nats#(X))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(X1,X2,X3) -> c_5()
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,5,8,9,10}
by application of
Pre({1,5,8,9,10}) = {2,3,4,6,7,11,12,13}.
Here rules are labelled as follows:
1: activate#(X) -> c_1()
2: activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
3: activate#(n__nats(X)) -> c_3(nats#(X))
4: activate#(n__sieve(X)) -> c_4(sieve#(X))
5: filter#(X1,X2,X3) -> c_5()
6: filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
7: filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
8: nats#(N) -> c_8()
9: nats#(X) -> c_9()
10: sieve#(X) -> c_10()
11: sieve#(cons(0(),Y)) -> c_11(activate#(Y))
12: sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
13: zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__nats(X)) -> c_3(nats#(X))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak DPs:
activate#(X) -> c_1()
filter#(X1,X2,X3) -> c_5()
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2}
by application of
Pre({2}) = {4,5,6,7}.
Here rules are labelled as follows:
1: activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
2: activate#(n__nats(X)) -> c_3(nats#(X))
3: activate#(n__sieve(X)) -> c_4(sieve#(X))
4: filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
5: filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
6: sieve#(cons(0(),Y)) -> c_11(activate#(Y))
7: sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
8: zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
9: activate#(X) -> c_1()
10: filter#(X1,X2,X3) -> c_5()
11: nats#(N) -> c_8()
12: nats#(X) -> c_9()
13: sieve#(X) -> c_10()
* Step 5: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak DPs:
activate#(X) -> c_1()
activate#(n__nats(X)) -> c_3(nats#(X))
filter#(X1,X2,X3) -> c_5()
nats#(N) -> c_8()
nats#(X) -> c_9()
sieve#(X) -> c_10()
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
-->_1 filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y)):4
-->_1 filter#(cons(X,Y),0(),M) -> c_6(activate#(Y)):3
-->_1 filter#(X1,X2,X3) -> c_5():10
2:S:activate#(n__sieve(X)) -> c_4(sieve#(X))
-->_1 sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y)):6
-->_1 sieve#(cons(0(),Y)) -> c_11(activate#(Y)):5
-->_1 sieve#(X) -> c_10():13
3:S:filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
-->_1 activate#(n__nats(X)) -> c_3(nats#(X)):9
-->_1 activate#(X) -> c_1():8
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
4:S:filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
-->_1 activate#(n__nats(X)) -> c_3(nats#(X)):9
-->_1 activate#(X) -> c_1():8
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
5:S:sieve#(cons(0(),Y)) -> c_11(activate#(Y))
-->_1 activate#(n__nats(X)) -> c_3(nats#(X)):9
-->_1 activate#(X) -> c_1():8
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
6:S:sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
-->_2 activate#(n__nats(X)) -> c_3(nats#(X)):9
-->_1 filter#(X1,X2,X3) -> c_5():10
-->_2 activate#(X) -> c_1():8
-->_1 filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y)):4
-->_1 filter#(cons(X,Y),0(),M) -> c_6(activate#(Y)):3
-->_2 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_2 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
7:S:zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
-->_1 sieve#(X) -> c_10():13
-->_2 nats#(X) -> c_9():12
-->_2 nats#(N) -> c_8():11
-->_1 sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y)):6
-->_1 sieve#(cons(0(),Y)) -> c_11(activate#(Y)):5
8:W:activate#(X) -> c_1()
9:W:activate#(n__nats(X)) -> c_3(nats#(X))
-->_1 nats#(X) -> c_9():12
-->_1 nats#(N) -> c_8():11
10:W:filter#(X1,X2,X3) -> c_5()
11:W:nats#(N) -> c_8()
12:W:nats#(X) -> c_9()
13:W:sieve#(X) -> c_10()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
13: sieve#(X) -> c_10()
10: filter#(X1,X2,X3) -> c_5()
8: activate#(X) -> c_1()
9: activate#(n__nats(X)) -> c_3(nats#(X))
11: nats#(N) -> c_8()
12: nats#(X) -> c_9()
* Step 6: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
-->_1 filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y)):4
-->_1 filter#(cons(X,Y),0(),M) -> c_6(activate#(Y)):3
2:S:activate#(n__sieve(X)) -> c_4(sieve#(X))
-->_1 sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y)):6
-->_1 sieve#(cons(0(),Y)) -> c_11(activate#(Y)):5
3:S:filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
4:S:filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
5:S:sieve#(cons(0(),Y)) -> c_11(activate#(Y))
-->_1 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_1 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
6:S:sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
-->_1 filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y)):4
-->_1 filter#(cons(X,Y),0(),M) -> c_6(activate#(Y)):3
-->_2 activate#(n__sieve(X)) -> c_4(sieve#(X)):2
-->_2 activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3)):1
7:S:zprimes#() -> c_13(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
-->_1 sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y)):6
-->_1 sieve#(cons(0(),Y)) -> c_11(activate#(Y)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
zprimes#() -> c_13(sieve#(nats(s(s(0())))))
* Step 7: NaturalMI MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
zprimes#() -> c_13(sieve#(nats(s(s(0())))))
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_7) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1,2},
uargs(c_13) = {1}
Following symbols are considered usable:
{activate#,filter#,nats#,sieve#,zprimes#}
TcT has computed the following interpretation:
p(0) = [0]
p(activate) = [0]
p(cons) = [0]
p(filter) = [0]
p(n__filter) = [0]
p(n__nats) = [0]
p(n__sieve) = [0]
p(nats) = [0]
p(s) = [0]
p(sieve) = [0]
p(zprimes) = [0]
p(activate#) = [0]
p(filter#) = [0]
p(nats#) = [0]
p(sieve#) = [0]
p(zprimes#) = [3]
p(c_1) = [0]
p(c_2) = [4] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [2] x1 + [0]
p(c_5) = [1]
p(c_6) = [4] x1 + [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [0]
p(c_9) = [4]
p(c_10) = [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [2] x1 + [4] x2 + [0]
p(c_13) = [1] x1 + [0]
Following rules are strictly oriented:
zprimes#() = [3]
> [0]
= c_13(sieve#(nats(s(s(0())))))
Following rules are (at-least) weakly oriented:
activate#(n__filter(X1,X2,X3)) = [0]
>= [0]
= c_2(filter#(X1,X2,X3))
activate#(n__sieve(X)) = [0]
>= [0]
= c_4(sieve#(X))
filter#(cons(X,Y),0(),M) = [0]
>= [0]
= c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) = [0]
>= [0]
= c_7(activate#(Y))
sieve#(cons(0(),Y)) = [0]
>= [0]
= c_11(activate#(Y))
sieve#(cons(s(N),Y)) = [0]
>= [0]
= c_12(filter#(activate(Y),N,N),activate#(Y))
* Step 8: Failure MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__filter(X1,X2,X3)) -> c_2(filter#(X1,X2,X3))
activate#(n__sieve(X)) -> c_4(sieve#(X))
filter#(cons(X,Y),0(),M) -> c_6(activate#(Y))
filter#(cons(X,Y),s(N),M) -> c_7(activate#(Y))
sieve#(cons(0(),Y)) -> c_11(activate#(Y))
sieve#(cons(s(N),Y)) -> c_12(filter#(activate(Y),N,N),activate#(Y))
- Weak DPs:
zprimes#() -> c_13(sieve#(nats(s(s(0())))))
- Weak TRS:
activate(X) -> X
activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
activate(n__nats(X)) -> nats(X)
activate(n__sieve(X)) -> sieve(X)
filter(X1,X2,X3) -> n__filter(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))
nats(N) -> cons(N,n__nats(s(N)))
nats(X) -> n__nats(X)
sieve(X) -> n__sieve(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)))
- Signature:
{activate/1,filter/3,nats/1,sieve/1,zprimes/0,activate#/1,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0
,cons/2,n__filter/3,n__nats/1,n__sieve/1,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0
,c_11/1,c_12/2,c_13/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate#,filter#,nats#,sieve#
,zprimes#} and constructors {0,cons,n__filter,n__nats,n__sieve,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE