YES(O(1),O(n^1)) 5.40/2.17 YES(O(1),O(n^1)) 5.40/2.17 5.40/2.17 We are left with following problem, upon which TcT provides the 5.40/2.17 certificate YES(O(1),O(n^1)). 5.40/2.17 5.40/2.17 Strict Trs: 5.40/2.17 { primes() -> sieve(from(s(s(0())))) 5.40/2.17 , sieve(X) -> n__sieve(X) 5.40/2.17 , sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y)))) 5.40/2.17 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.17 , from(X) -> n__from(X) 5.40/2.17 , s(X) -> n__s(X) 5.40/2.17 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.17 , head(cons(X, Y)) -> X 5.40/2.17 , tail(cons(X, Y)) -> activate(Y) 5.40/2.17 , activate(X) -> X 5.40/2.17 , activate(n__from(X)) -> from(activate(X)) 5.40/2.17 , activate(n__s(X)) -> s(activate(X)) 5.40/2.17 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.17 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.17 , if(true(), X, Y) -> activate(X) 5.40/2.17 , if(false(), X, Y) -> activate(Y) 5.40/2.17 , filter(X1, X2) -> n__filter(X1, X2) 5.40/2.17 , filter(s(s(X)), cons(Y, Z)) -> 5.40/2.17 if(divides(s(s(X)), Y), 5.40/2.17 n__filter(n__s(n__s(X)), activate(Z)), 5.40/2.17 n__cons(Y, n__filter(X, n__sieve(Y)))) } 5.40/2.17 Obligation: 5.40/2.17 innermost runtime complexity 5.40/2.17 Answer: 5.40/2.17 YES(O(1),O(n^1)) 5.40/2.17 5.40/2.17 Arguments of following rules are not normal-forms: 5.40/2.17 5.40/2.17 { sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y)))) 5.40/2.17 , head(cons(X, Y)) -> X 5.40/2.17 , tail(cons(X, Y)) -> activate(Y) 5.40/2.17 , filter(s(s(X)), cons(Y, Z)) -> 5.40/2.17 if(divides(s(s(X)), Y), 5.40/2.17 n__filter(n__s(n__s(X)), activate(Z)), 5.40/2.17 n__cons(Y, n__filter(X, n__sieve(Y)))) } 5.40/2.17 5.40/2.17 All above mentioned rules can be savely removed. 5.40/2.17 5.40/2.17 We are left with following problem, upon which TcT provides the 5.40/2.17 certificate YES(O(1),O(n^1)). 5.40/2.17 5.40/2.17 Strict Trs: 5.40/2.17 { primes() -> sieve(from(s(s(0())))) 5.40/2.17 , sieve(X) -> n__sieve(X) 5.40/2.17 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.17 , from(X) -> n__from(X) 5.40/2.17 , s(X) -> n__s(X) 5.40/2.17 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.17 , activate(X) -> X 5.40/2.17 , activate(n__from(X)) -> from(activate(X)) 5.40/2.17 , activate(n__s(X)) -> s(activate(X)) 5.40/2.17 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.17 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.17 , if(true(), X, Y) -> activate(X) 5.40/2.17 , if(false(), X, Y) -> activate(Y) 5.40/2.17 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.17 Obligation: 5.40/2.17 innermost runtime complexity 5.40/2.17 Answer: 5.40/2.17 YES(O(1),O(n^1)) 5.40/2.17 5.40/2.17 We add the following weak dependency pairs: 5.40/2.17 5.40/2.17 Strict DPs: 5.40/2.17 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.17 , sieve^#(X) -> c_2() 5.40/2.17 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.17 , from^#(X) -> c_4() 5.40/2.17 , cons^#(X1, X2) -> c_6() 5.40/2.17 , s^#(X) -> c_5() 5.40/2.17 , activate^#(X) -> c_7() 5.40/2.17 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.17 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.17 , activate^#(n__filter(X1, X2)) -> 5.40/2.17 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.17 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.17 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.17 , filter^#(X1, X2) -> c_15() 5.40/2.17 , if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.17 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.17 5.40/2.17 and mark the set of starting terms. 5.40/2.17 5.40/2.17 We are left with following problem, upon which TcT provides the 5.40/2.17 certificate YES(O(1),O(n^1)). 5.40/2.17 5.40/2.17 Strict DPs: 5.40/2.17 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.17 , sieve^#(X) -> c_2() 5.40/2.17 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.17 , from^#(X) -> c_4() 5.40/2.17 , cons^#(X1, X2) -> c_6() 5.40/2.17 , s^#(X) -> c_5() 5.40/2.17 , activate^#(X) -> c_7() 5.40/2.17 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.17 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.17 , activate^#(n__filter(X1, X2)) -> 5.40/2.17 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.17 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.17 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.17 , filter^#(X1, X2) -> c_15() 5.40/2.17 , if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.17 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.17 Strict Trs: 5.40/2.17 { primes() -> sieve(from(s(s(0())))) 5.40/2.17 , sieve(X) -> n__sieve(X) 5.40/2.17 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.17 , from(X) -> n__from(X) 5.40/2.17 , s(X) -> n__s(X) 5.40/2.17 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.17 , activate(X) -> X 5.40/2.17 , activate(n__from(X)) -> from(activate(X)) 5.40/2.17 , activate(n__s(X)) -> s(activate(X)) 5.40/2.17 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.17 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.17 , if(true(), X, Y) -> activate(X) 5.40/2.17 , if(false(), X, Y) -> activate(Y) 5.40/2.17 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.17 Obligation: 5.40/2.17 innermost runtime complexity 5.40/2.17 Answer: 5.40/2.17 YES(O(1),O(n^1)) 5.40/2.17 5.40/2.17 We replace rewrite rules by usable rules: 5.40/2.17 5.40/2.17 Strict Usable Rules: 5.40/2.17 { sieve(X) -> n__sieve(X) 5.40/2.17 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.17 , from(X) -> n__from(X) 5.40/2.17 , s(X) -> n__s(X) 5.40/2.17 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.17 , activate(X) -> X 5.40/2.17 , activate(n__from(X)) -> from(activate(X)) 5.40/2.17 , activate(n__s(X)) -> s(activate(X)) 5.40/2.17 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.17 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.17 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.17 5.40/2.17 We are left with following problem, upon which TcT provides the 5.40/2.17 certificate YES(O(1),O(n^1)). 5.40/2.17 5.40/2.17 Strict DPs: 5.40/2.17 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.17 , sieve^#(X) -> c_2() 5.40/2.17 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.17 , from^#(X) -> c_4() 5.40/2.17 , cons^#(X1, X2) -> c_6() 5.40/2.17 , s^#(X) -> c_5() 5.40/2.17 , activate^#(X) -> c_7() 5.40/2.17 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.17 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.17 , activate^#(n__filter(X1, X2)) -> 5.40/2.17 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.17 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.17 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.17 , filter^#(X1, X2) -> c_15() 5.40/2.17 , if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.17 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.17 Strict Trs: 5.40/2.17 { sieve(X) -> n__sieve(X) 5.40/2.17 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.17 , from(X) -> n__from(X) 5.40/2.17 , s(X) -> n__s(X) 5.40/2.17 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.17 , activate(X) -> X 5.40/2.17 , activate(n__from(X)) -> from(activate(X)) 5.40/2.17 , activate(n__s(X)) -> s(activate(X)) 5.40/2.17 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.17 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.17 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.17 Obligation: 5.40/2.17 innermost runtime complexity 5.40/2.17 Answer: 5.40/2.17 YES(O(1),O(n^1)) 5.40/2.17 5.40/2.17 The weightgap principle applies (using the following constant 5.40/2.17 growth matrix-interpretation) 5.40/2.17 5.40/2.17 The following argument positions are usable: 5.40/2.17 Uargs(sieve) = {1}, Uargs(from) = {1}, Uargs(s) = {1}, 5.40/2.17 Uargs(cons) = {1}, Uargs(filter) = {1, 2}, Uargs(c_1) = {1}, 5.40/2.17 Uargs(sieve^#) = {1}, Uargs(from^#) = {1}, Uargs(c_3) = {1}, 5.40/2.17 Uargs(cons^#) = {1}, Uargs(s^#) = {1}, Uargs(c_8) = {1}, 5.40/2.17 Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(filter^#) = {1, 2}, 5.40/2.17 Uargs(c_11) = {1}, Uargs(c_12) = {1}, Uargs(c_13) = {1}, 5.40/2.17 Uargs(c_14) = {1} 5.40/2.17 5.40/2.17 TcT has computed the following constructor-restricted matrix 5.40/2.17 interpretation. 5.40/2.17 5.40/2.17 [sieve](x1) = [1 0] x1 + [2] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [from](x1) = [1 0] x1 + [2] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [s](x1) = [1 0] x1 + [1] 5.40/2.17 [0 1] [1] 5.40/2.17 5.40/2.17 [0] = [0] 5.40/2.17 [0] 5.40/2.17 5.40/2.17 [cons](x1, x2) = [1 0] x1 + [1] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [n__from](x1) = [1 0] x1 + [0] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [n__s](x1) = [1 0] x1 + [0] 5.40/2.17 [0 1] [1] 5.40/2.17 5.40/2.17 [activate](x1) = [1 2] x1 + [1] 5.40/2.17 [0 2] [0] 5.40/2.17 5.40/2.17 [true] = [1] 5.40/2.17 [2] 5.40/2.17 5.40/2.17 [false] = [1] 5.40/2.17 [1] 5.40/2.17 5.40/2.17 [filter](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 5.40/2.17 [0 1] [0 1] [2] 5.40/2.17 5.40/2.17 [n__filter](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 5.40/2.17 [0 1] [0 1] [2] 5.40/2.17 5.40/2.17 [n__cons](x1, x2) = [1 0] x1 + [0] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [n__sieve](x1) = [1 0] x1 + [0] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [primes^#] = [1] 5.40/2.17 [1] 5.40/2.17 5.40/2.17 [c_1](x1) = [1 0] x1 + [1] 5.40/2.17 [0 1] [2] 5.40/2.17 5.40/2.17 [sieve^#](x1) = [1 0] x1 + [1] 5.40/2.17 [0 0] [2] 5.40/2.17 5.40/2.17 [c_2] = [1] 5.40/2.17 [1] 5.40/2.17 5.40/2.18 [from^#](x1) = [1 0] x1 + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 5.40/2.18 [c_3](x1) = [1 0] x1 + [1] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [cons^#](x1, x2) = [1 0] x1 + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 5.40/2.18 [c_4] = [1] 5.40/2.18 [1] 5.40/2.18 5.40/2.18 [s^#](x1) = [1 0] x1 + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 5.40/2.18 [c_5] = [1] 5.40/2.18 [1] 5.40/2.18 5.40/2.18 [c_6] = [1] 5.40/2.18 [1] 5.40/2.18 5.40/2.18 [activate^#](x1) = [1 2] x1 + [0] 5.40/2.18 [0 0] [0] 5.40/2.18 5.40/2.18 [c_7] = [1] 5.40/2.18 [1] 5.40/2.18 5.40/2.18 [c_8](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [c_9](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [c_10](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [filter^#](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 5.40/2.18 [0 0] [0 0] [2] 5.40/2.18 5.40/2.18 [c_11](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [c_12](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [if^#](x1, x2, x3) = [1 1] x1 + [1 2] x2 + [1 2] x3 + [1] 5.40/2.18 [1 1] [2 2] [1 1] [1] 5.40/2.18 5.40/2.18 [c_13](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [c_14](x1) = [1 0] x1 + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 5.40/2.18 [c_15] = [2] 5.40/2.18 [1] 5.40/2.18 5.40/2.18 The order satisfies the following ordering constraints: 5.40/2.18 5.40/2.18 [sieve(X)] = [1 0] X + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 > [1 0] X + [0] 5.40/2.18 [0 1] [2] 5.40/2.18 = [n__sieve(X)] 5.40/2.18 5.40/2.18 [from(X)] = [1 0] X + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 > [1 0] X + [1] 5.40/2.18 [0 1] [2] 5.40/2.18 = [cons(X, n__from(n__s(X)))] 5.40/2.18 5.40/2.18 [from(X)] = [1 0] X + [2] 5.40/2.18 [0 1] [2] 5.40/2.18 > [1 0] X + [0] 5.40/2.18 [0 1] [2] 5.40/2.18 = [n__from(X)] 5.40/2.18 5.40/2.18 [s(X)] = [1 0] X + [1] 5.40/2.18 [0 1] [1] 5.40/2.18 > [1 0] X + [0] 5.40/2.18 [0 1] [1] 5.40/2.18 = [n__s(X)] 5.40/2.18 5.40/2.18 [cons(X1, X2)] = [1 0] X1 + [1] 5.40/2.18 [0 1] [2] 5.40/2.18 > [1 0] X1 + [0] 5.40/2.18 [0 1] [2] 5.40/2.18 = [n__cons(X1, X2)] 5.40/2.18 5.40/2.18 [activate(X)] = [1 2] X + [1] 5.40/2.18 [0 2] [0] 5.40/2.18 > [1 0] X + [0] 5.40/2.18 [0 1] [0] 5.40/2.18 = [X] 5.40/2.18 5.40/2.18 [activate(n__from(X))] = [1 2] X + [5] 5.40/2.18 [0 2] [4] 5.40/2.18 > [1 2] X + [3] 5.40/2.18 [0 2] [2] 5.40/2.18 = [from(activate(X))] 5.40/2.18 5.40/2.18 [activate(n__s(X))] = [1 2] X + [3] 5.40/2.18 [0 2] [2] 5.40/2.18 > [1 2] X + [2] 5.40/2.18 [0 2] [1] 5.40/2.18 = [s(activate(X))] 5.40/2.18 5.40/2.18 [activate(n__filter(X1, X2))] = [1 2] X1 + [1 2] X2 + [5] 5.40/2.18 [0 2] [0 2] [4] 5.40/2.18 > [1 2] X1 + [1 2] X2 + [3] 5.40/2.18 [0 2] [0 2] [2] 5.40/2.18 = [filter(activate(X1), activate(X2))] 5.40/2.18 5.40/2.18 [activate(n__cons(X1, X2))] = [1 2] X1 + [5] 5.40/2.18 [0 2] [4] 5.40/2.18 > [1 2] X1 + [2] 5.40/2.18 [0 2] [2] 5.40/2.18 = [cons(activate(X1), X2)] 5.40/2.18 5.40/2.18 [activate(n__sieve(X))] = [1 2] X + [5] 5.40/2.18 [0 2] [4] 5.40/2.18 > [1 2] X + [3] 5.40/2.18 [0 2] [2] 5.40/2.18 = [sieve(activate(X))] 5.40/2.18 5.40/2.18 [filter(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 5.40/2.18 [0 1] [0 1] [2] 5.40/2.18 > [1 0] X1 + [1 0] X2 + [0] 5.40/2.18 [0 1] [0 1] [2] 5.40/2.18 = [n__filter(X1, X2)] 5.40/2.18 5.40/2.18 [primes^#()] = [1] 5.40/2.18 [1] 5.40/2.18 ? [6] 5.40/2.18 [4] 5.40/2.18 = [c_1(sieve^#(from(s(s(0())))))] 5.40/2.18 5.40/2.18 [sieve^#(X)] = [1 0] X + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 >= [1] 5.40/2.18 [1] 5.40/2.18 = [c_2()] 5.40/2.18 5.40/2.18 [from^#(X)] = [1 0] X + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 ? [1 0] X + [2] 5.40/2.18 [0 0] [4] 5.40/2.18 = [c_3(cons^#(X, n__from(n__s(X))))] 5.40/2.18 5.40/2.18 [from^#(X)] = [1 0] X + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 >= [1] 5.40/2.18 [1] 5.40/2.18 = [c_4()] 5.40/2.18 5.40/2.18 [cons^#(X1, X2)] = [1 0] X1 + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 >= [1] 5.40/2.18 [1] 5.40/2.18 = [c_6()] 5.40/2.18 5.40/2.18 [s^#(X)] = [1 0] X + [1] 5.40/2.18 [0 0] [2] 5.40/2.18 >= [1] 5.40/2.18 [1] 5.40/2.18 = [c_5()] 5.40/2.18 5.40/2.18 [activate^#(X)] = [1 2] X + [0] 5.40/2.18 [0 0] [0] 5.40/2.18 ? [1] 5.40/2.18 [1] 5.40/2.18 = [c_7()] 5.40/2.18 5.40/2.18 [activate^#(n__from(X))] = [1 2] X + [4] 5.40/2.18 [0 0] [0] 5.40/2.18 ? [1 2] X + [4] 5.40/2.18 [0 0] [4] 5.40/2.18 = [c_8(from^#(activate(X)))] 5.40/2.18 5.40/2.18 [activate^#(n__s(X))] = [1 2] X + [2] 5.40/2.18 [0 0] [0] 5.40/2.18 ? [1 2] X + [4] 5.40/2.18 [0 0] [4] 5.40/2.18 = [c_9(s^#(activate(X)))] 5.40/2.18 5.40/2.18 [activate^#(n__filter(X1, X2))] = [1 2] X1 + [1 2] X2 + [4] 5.40/2.18 [0 0] [0 0] [0] 5.40/2.18 ? [1 2] X1 + [1 2] X2 + [6] 5.40/2.18 [0 0] [0 0] [4] 5.40/2.18 = [c_10(filter^#(activate(X1), activate(X2)))] 5.40/2.18 5.40/2.18 [activate^#(n__cons(X1, X2))] = [1 2] X1 + [4] 5.40/2.18 [0 0] [0] 5.40/2.18 ? [1 2] X1 + [4] 5.40/2.18 [0 0] [4] 5.40/2.18 = [c_11(cons^#(activate(X1), X2))] 5.40/2.18 5.40/2.18 [activate^#(n__sieve(X))] = [1 2] X + [4] 5.40/2.18 [0 0] [0] 5.40/2.18 ? [1 2] X + [4] 5.40/2.18 [0 0] [4] 5.40/2.18 = [c_12(sieve^#(activate(X)))] 5.40/2.18 5.40/2.18 [filter^#(X1, X2)] = [1 0] X1 + [1 0] X2 + [2] 5.40/2.18 [0 0] [0 0] [2] 5.40/2.18 >= [2] 5.40/2.18 [1] 5.40/2.18 = [c_15()] 5.40/2.18 5.40/2.18 [if^#(true(), X, Y)] = [1 2] X + [1 2] Y + [4] 5.40/2.18 [2 2] [1 1] [4] 5.40/2.18 > [1 2] X + [2] 5.40/2.18 [0 0] [2] 5.40/2.18 = [c_13(activate^#(X))] 5.40/2.18 5.40/2.18 [if^#(false(), X, Y)] = [1 2] X + [1 2] Y + [3] 5.40/2.18 [2 2] [1 1] [3] 5.40/2.18 > [1 2] Y + [2] 5.40/2.18 [0 0] [2] 5.40/2.18 = [c_14(activate^#(Y))] 5.40/2.18 5.40/2.18 5.40/2.18 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , sieve^#(X) -> c_2() 5.40/2.18 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , from^#(X) -> c_4() 5.40/2.18 , cons^#(X1, X2) -> c_6() 5.40/2.18 , s^#(X) -> c_5() 5.40/2.18 , activate^#(X) -> c_7() 5.40/2.18 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.18 , filter^#(X1, X2) -> c_15() } 5.40/2.18 Weak DPs: 5.40/2.18 { if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 Weak Trs: 5.40/2.18 { sieve(X) -> n__sieve(X) 5.40/2.18 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.18 , from(X) -> n__from(X) 5.40/2.18 , s(X) -> n__s(X) 5.40/2.18 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.18 , activate(X) -> X 5.40/2.18 , activate(n__from(X)) -> from(activate(X)) 5.40/2.18 , activate(n__s(X)) -> s(activate(X)) 5.40/2.18 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.18 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.18 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 We estimate the number of application of {2,4,5,6,13} by 5.40/2.18 applications of Pre({2,4,5,6,13}) = {1,3,8,9,10,11,12}. Here rules 5.40/2.18 are labeled as follows: 5.40/2.18 5.40/2.18 DPs: 5.40/2.18 { 1: primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , 2: sieve^#(X) -> c_2() 5.40/2.18 , 3: from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , 4: from^#(X) -> c_4() 5.40/2.18 , 5: cons^#(X1, X2) -> c_6() 5.40/2.18 , 6: s^#(X) -> c_5() 5.40/2.18 , 7: activate^#(X) -> c_7() 5.40/2.18 , 8: activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , 9: activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , 10: activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , 11: activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , 12: activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.18 , 13: filter^#(X1, X2) -> c_15() 5.40/2.18 , 14: if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , 15: if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , activate^#(X) -> c_7() 5.40/2.18 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) } 5.40/2.18 Weak DPs: 5.40/2.18 { sieve^#(X) -> c_2() 5.40/2.18 , from^#(X) -> c_4() 5.40/2.18 , cons^#(X1, X2) -> c_6() 5.40/2.18 , s^#(X) -> c_5() 5.40/2.18 , filter^#(X1, X2) -> c_15() 5.40/2.18 , if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 Weak Trs: 5.40/2.18 { sieve(X) -> n__sieve(X) 5.40/2.18 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.18 , from(X) -> n__from(X) 5.40/2.18 , s(X) -> n__s(X) 5.40/2.18 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.18 , activate(X) -> X 5.40/2.18 , activate(n__from(X)) -> from(activate(X)) 5.40/2.18 , activate(n__s(X)) -> s(activate(X)) 5.40/2.18 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.18 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.18 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 We estimate the number of application of {1,2} by applications of 5.40/2.18 Pre({1,2}) = {4}. Here rules are labeled as follows: 5.40/2.18 5.40/2.18 DPs: 5.40/2.18 { 1: primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , 2: from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , 3: activate^#(X) -> c_7() 5.40/2.18 , 4: activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , 5: activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , 6: activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , 7: activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , 8: activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) 5.40/2.18 , 9: sieve^#(X) -> c_2() 5.40/2.18 , 10: from^#(X) -> c_4() 5.40/2.18 , 11: cons^#(X1, X2) -> c_6() 5.40/2.18 , 12: s^#(X) -> c_5() 5.40/2.18 , 13: filter^#(X1, X2) -> c_15() 5.40/2.18 , 14: if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , 15: if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { activate^#(X) -> c_7() 5.40/2.18 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) } 5.40/2.18 Weak DPs: 5.40/2.18 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , sieve^#(X) -> c_2() 5.40/2.18 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , from^#(X) -> c_4() 5.40/2.18 , cons^#(X1, X2) -> c_6() 5.40/2.18 , s^#(X) -> c_5() 5.40/2.18 , filter^#(X1, X2) -> c_15() 5.40/2.18 , if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 Weak Trs: 5.40/2.18 { sieve(X) -> n__sieve(X) 5.40/2.18 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.18 , from(X) -> n__from(X) 5.40/2.18 , s(X) -> n__s(X) 5.40/2.18 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.18 , activate(X) -> X 5.40/2.18 , activate(n__from(X)) -> from(activate(X)) 5.40/2.18 , activate(n__s(X)) -> s(activate(X)) 5.40/2.18 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.18 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.18 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 The following weak DPs constitute a sub-graph of the DG that is 5.40/2.18 closed under successors. The DPs are removed. 5.40/2.18 5.40/2.18 { primes^#() -> c_1(sieve^#(from(s(s(0()))))) 5.40/2.18 , sieve^#(X) -> c_2() 5.40/2.18 , from^#(X) -> c_3(cons^#(X, n__from(n__s(X)))) 5.40/2.18 , from^#(X) -> c_4() 5.40/2.18 , cons^#(X1, X2) -> c_6() 5.40/2.18 , s^#(X) -> c_5() 5.40/2.18 , filter^#(X1, X2) -> c_15() } 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { activate^#(X) -> c_7() 5.40/2.18 , activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) } 5.40/2.18 Weak DPs: 5.40/2.18 { if^#(true(), X, Y) -> c_13(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_14(activate^#(Y)) } 5.40/2.18 Weak Trs: 5.40/2.18 { sieve(X) -> n__sieve(X) 5.40/2.18 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.18 , from(X) -> n__from(X) 5.40/2.18 , s(X) -> n__s(X) 5.40/2.18 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.18 , activate(X) -> X 5.40/2.18 , activate(n__from(X)) -> from(activate(X)) 5.40/2.18 , activate(n__s(X)) -> s(activate(X)) 5.40/2.18 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.18 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.18 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 Due to missing edges in the dependency-graph, the right-hand sides 5.40/2.18 of following rules could be simplified: 5.40/2.18 5.40/2.18 { activate^#(n__from(X)) -> c_8(from^#(activate(X))) 5.40/2.18 , activate^#(n__s(X)) -> c_9(s^#(activate(X))) 5.40/2.18 , activate^#(n__filter(X1, X2)) -> 5.40/2.18 c_10(filter^#(activate(X1), activate(X2))) 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2)) 5.40/2.18 , activate^#(n__sieve(X)) -> c_12(sieve^#(activate(X))) } 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { activate^#(X) -> c_1() 5.40/2.18 , activate^#(n__from(X)) -> c_2() 5.40/2.18 , activate^#(n__s(X)) -> c_3() 5.40/2.18 , activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 , activate^#(n__sieve(X)) -> c_6() } 5.40/2.18 Weak DPs: 5.40/2.18 { if^#(true(), X, Y) -> c_7(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_8(activate^#(Y)) } 5.40/2.18 Weak Trs: 5.40/2.18 { sieve(X) -> n__sieve(X) 5.40/2.18 , from(X) -> cons(X, n__from(n__s(X))) 5.40/2.18 , from(X) -> n__from(X) 5.40/2.18 , s(X) -> n__s(X) 5.40/2.18 , cons(X1, X2) -> n__cons(X1, X2) 5.40/2.18 , activate(X) -> X 5.40/2.18 , activate(n__from(X)) -> from(activate(X)) 5.40/2.18 , activate(n__s(X)) -> s(activate(X)) 5.40/2.18 , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2)) 5.40/2.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 5.40/2.18 , activate(n__sieve(X)) -> sieve(activate(X)) 5.40/2.18 , filter(X1, X2) -> n__filter(X1, X2) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 No rule is usable, rules are removed from the input problem. 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { activate^#(X) -> c_1() 5.40/2.18 , activate^#(n__from(X)) -> c_2() 5.40/2.18 , activate^#(n__s(X)) -> c_3() 5.40/2.18 , activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 , activate^#(n__sieve(X)) -> c_6() } 5.40/2.18 Weak DPs: 5.40/2.18 { if^#(true(), X, Y) -> c_7(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_8(activate^#(Y)) } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 Consider the dependency graph 5.40/2.18 5.40/2.18 1: activate^#(X) -> c_1() 5.40/2.18 5.40/2.18 2: activate^#(n__from(X)) -> c_2() 5.40/2.18 5.40/2.18 3: activate^#(n__s(X)) -> c_3() 5.40/2.18 5.40/2.18 4: activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 5.40/2.18 5: activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 5.40/2.18 6: activate^#(n__sieve(X)) -> c_6() 5.40/2.18 5.40/2.18 7: if^#(true(), X, Y) -> c_7(activate^#(X)) 5.40/2.18 -->_1 activate^#(n__sieve(X)) -> c_6() :6 5.40/2.18 -->_1 activate^#(n__cons(X1, X2)) -> c_5() :5 5.40/2.18 -->_1 activate^#(n__filter(X1, X2)) -> c_4() :4 5.40/2.18 -->_1 activate^#(n__s(X)) -> c_3() :3 5.40/2.18 -->_1 activate^#(n__from(X)) -> c_2() :2 5.40/2.18 -->_1 activate^#(X) -> c_1() :1 5.40/2.18 5.40/2.18 8: if^#(false(), X, Y) -> c_8(activate^#(Y)) 5.40/2.18 -->_1 activate^#(n__sieve(X)) -> c_6() :6 5.40/2.18 -->_1 activate^#(n__cons(X1, X2)) -> c_5() :5 5.40/2.18 -->_1 activate^#(n__filter(X1, X2)) -> c_4() :4 5.40/2.18 -->_1 activate^#(n__s(X)) -> c_3() :3 5.40/2.18 -->_1 activate^#(n__from(X)) -> c_2() :2 5.40/2.18 -->_1 activate^#(X) -> c_1() :1 5.40/2.18 5.40/2.18 5.40/2.18 Following roots of the dependency graph are removed, as the 5.40/2.18 considered set of starting terms is closed under reduction with 5.40/2.18 respect to these rules (modulo compound contexts). 5.40/2.18 5.40/2.18 { if^#(true(), X, Y) -> c_7(activate^#(X)) 5.40/2.18 , if^#(false(), X, Y) -> c_8(activate^#(Y)) } 5.40/2.18 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Strict DPs: 5.40/2.18 { activate^#(X) -> c_1() 5.40/2.18 , activate^#(n__from(X)) -> c_2() 5.40/2.18 , activate^#(n__s(X)) -> c_3() 5.40/2.18 , activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 , activate^#(n__sieve(X)) -> c_6() } 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 Consider the dependency graph 5.40/2.18 5.40/2.18 1: activate^#(X) -> c_1() 5.40/2.18 5.40/2.18 2: activate^#(n__from(X)) -> c_2() 5.40/2.18 5.40/2.18 3: activate^#(n__s(X)) -> c_3() 5.40/2.18 5.40/2.18 4: activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 5.40/2.18 5: activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 5.40/2.18 6: activate^#(n__sieve(X)) -> c_6() 5.40/2.18 5.40/2.18 5.40/2.18 Following roots of the dependency graph are removed, as the 5.40/2.18 considered set of starting terms is closed under reduction with 5.40/2.18 respect to these rules (modulo compound contexts). 5.40/2.18 5.40/2.18 { activate^#(X) -> c_1() 5.40/2.18 , activate^#(n__from(X)) -> c_2() 5.40/2.18 , activate^#(n__s(X)) -> c_3() 5.40/2.18 , activate^#(n__filter(X1, X2)) -> c_4() 5.40/2.18 , activate^#(n__cons(X1, X2)) -> c_5() 5.40/2.18 , activate^#(n__sieve(X)) -> c_6() } 5.40/2.18 5.40/2.18 5.40/2.18 We are left with following problem, upon which TcT provides the 5.40/2.18 certificate YES(O(1),O(1)). 5.40/2.18 5.40/2.18 Rules: Empty 5.40/2.18 Obligation: 5.40/2.18 innermost runtime complexity 5.40/2.18 Answer: 5.40/2.18 YES(O(1),O(1)) 5.40/2.18 5.40/2.18 Empty rules are trivially bounded 5.40/2.18 5.40/2.18 Hurray, we answered YES(O(1),O(n^1)) 5.40/2.19 EOF