YES(O(1),O(n^2)) 968.64/297.10 YES(O(1),O(n^2)) 968.64/297.10 968.64/297.10 We are left with following problem, upon which TcT provides the 968.64/297.10 certificate YES(O(1),O(n^2)). 968.64/297.10 968.64/297.10 Strict Trs: 968.64/297.10 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.10 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.10 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.10 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.10 , mark(0()) -> 0() 968.64/297.10 , mark(filter(X1, X2, X3)) -> 968.64/297.10 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.10 , mark(s(X)) -> s(mark(X)) 968.64/297.10 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.10 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.10 , mark(zprimes()) -> a__zprimes() 968.64/297.10 , a__sieve(X) -> sieve(X) 968.64/297.10 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.10 , a__sieve(cons(s(N), Y)) -> 968.64/297.10 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.10 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.10 , a__nats(X) -> nats(X) 968.64/297.10 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.10 , a__zprimes() -> zprimes() } 968.64/297.10 Obligation: 968.64/297.10 innermost runtime complexity 968.64/297.10 Answer: 968.64/297.10 YES(O(1),O(n^2)) 968.64/297.10 968.64/297.10 The weightgap principle applies (using the following nonconstant 968.64/297.10 growth matrix-interpretation) 968.64/297.10 968.64/297.10 The following argument positions are usable: 968.64/297.10 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.10 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.10 968.64/297.10 TcT has computed the following matrix interpretation satisfying 968.64/297.10 not(EDA) and not(IDA(1)). 968.64/297.10 968.64/297.10 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 968.64/297.10 968.64/297.10 [cons](x1, x2) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [0] = [0] 968.64/297.10 968.64/297.10 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3] 968.64/297.10 968.64/297.10 [s](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [mark](x1) = [0] 968.64/297.10 968.64/297.10 [a__sieve](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [sieve](x1) = [1] x1 + [7] 968.64/297.10 968.64/297.10 [a__nats](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [nats](x1) = [1] x1 + [7] 968.64/297.10 968.64/297.10 [a__zprimes] = [1] 968.64/297.10 968.64/297.10 [zprimes] = [6] 968.64/297.10 968.64/297.10 The order satisfies the following ordering constraints: 968.64/297.10 968.64/297.10 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [4] 968.64/297.10 > [1] X1 + [1] X2 + [1] X3 + [3] 968.64/297.10 = [filter(X1, X2, X3)] 968.64/297.10 968.64/297.10 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [4] 968.64/297.10 > [0] 968.64/297.10 = [cons(0(), filter(Y, M, M))] 968.64/297.10 968.64/297.10 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [4] 968.64/297.10 > [0] 968.64/297.10 = [cons(mark(X), filter(Y, N, M))] 968.64/297.10 968.64/297.10 [mark(cons(X1, X2))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(mark(X1), X2)] 968.64/297.10 968.64/297.10 [mark(0())] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [0()] 968.64/297.10 968.64/297.10 [mark(filter(X1, X2, X3))] = [0] 968.64/297.10 ? [4] 968.64/297.10 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.10 968.64/297.10 [mark(s(X))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [s(mark(X))] 968.64/297.10 968.64/297.10 [mark(sieve(X))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [a__sieve(mark(X))] 968.64/297.10 968.64/297.10 [mark(nats(X))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [a__nats(mark(X))] 968.64/297.10 968.64/297.10 [mark(zprimes())] = [0] 968.64/297.10 ? [1] 968.64/297.10 = [a__zprimes()] 968.64/297.10 968.64/297.10 [a__sieve(X)] = [1] X + [0] 968.64/297.10 ? [1] X + [7] 968.64/297.10 = [sieve(X)] 968.64/297.10 968.64/297.10 [a__sieve(cons(0(), Y))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(0(), sieve(Y))] 968.64/297.10 968.64/297.10 [a__sieve(cons(s(N), Y))] = [1] N + [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.10 968.64/297.10 [a__nats(N)] = [1] N + [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(mark(N), nats(s(N)))] 968.64/297.10 968.64/297.10 [a__nats(X)] = [1] X + [0] 968.64/297.10 ? [1] X + [7] 968.64/297.10 = [nats(X)] 968.64/297.10 968.64/297.10 [a__zprimes()] = [1] 968.64/297.10 > [0] 968.64/297.10 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.10 968.64/297.10 [a__zprimes()] = [1] 968.64/297.10 ? [6] 968.64/297.10 = [zprimes()] 968.64/297.10 968.64/297.10 968.64/297.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.10 968.64/297.10 We are left with following problem, upon which TcT provides the 968.64/297.10 certificate YES(O(1),O(n^2)). 968.64/297.10 968.64/297.10 Strict Trs: 968.64/297.10 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.10 , mark(0()) -> 0() 968.64/297.10 , mark(filter(X1, X2, X3)) -> 968.64/297.10 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.10 , mark(s(X)) -> s(mark(X)) 968.64/297.10 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.10 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.10 , mark(zprimes()) -> a__zprimes() 968.64/297.10 , a__sieve(X) -> sieve(X) 968.64/297.10 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.10 , a__sieve(cons(s(N), Y)) -> 968.64/297.10 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.10 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.10 , a__nats(X) -> nats(X) 968.64/297.10 , a__zprimes() -> zprimes() } 968.64/297.10 Weak Trs: 968.64/297.10 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.10 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.10 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.10 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) } 968.64/297.10 Obligation: 968.64/297.10 innermost runtime complexity 968.64/297.10 Answer: 968.64/297.10 YES(O(1),O(n^2)) 968.64/297.10 968.64/297.10 The weightgap principle applies (using the following nonconstant 968.64/297.10 growth matrix-interpretation) 968.64/297.10 968.64/297.10 The following argument positions are usable: 968.64/297.10 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.10 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.10 968.64/297.10 TcT has computed the following matrix interpretation satisfying 968.64/297.10 not(EDA) and not(IDA(1)). 968.64/297.10 968.64/297.10 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.10 968.64/297.10 [cons](x1, x2) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [0] = [0] 968.64/297.10 968.64/297.10 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.10 968.64/297.10 [s](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [mark](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [a__sieve](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [sieve](x1) = [1] x1 + [1] 968.64/297.10 968.64/297.10 [a__nats](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [nats](x1) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [a__zprimes] = [5] 968.64/297.10 968.64/297.10 [zprimes] = [1] 968.64/297.10 968.64/297.10 The order satisfies the following ordering constraints: 968.64/297.10 968.64/297.10 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.10 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.10 = [filter(X1, X2, X3)] 968.64/297.10 968.64/297.10 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(0(), filter(Y, M, M))] 968.64/297.10 968.64/297.10 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [0] 968.64/297.10 >= [1] X + [0] 968.64/297.10 = [cons(mark(X), filter(Y, N, M))] 968.64/297.10 968.64/297.10 [mark(cons(X1, X2))] = [1] X1 + [0] 968.64/297.10 >= [1] X1 + [0] 968.64/297.10 = [cons(mark(X1), X2)] 968.64/297.10 968.64/297.10 [mark(0())] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [0()] 968.64/297.10 968.64/297.10 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.10 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.10 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.10 968.64/297.10 [mark(s(X))] = [1] X + [0] 968.64/297.10 >= [1] X + [0] 968.64/297.10 = [s(mark(X))] 968.64/297.10 968.64/297.10 [mark(sieve(X))] = [1] X + [1] 968.64/297.10 > [1] X + [0] 968.64/297.10 = [a__sieve(mark(X))] 968.64/297.10 968.64/297.10 [mark(nats(X))] = [1] X + [0] 968.64/297.10 >= [1] X + [0] 968.64/297.10 = [a__nats(mark(X))] 968.64/297.10 968.64/297.10 [mark(zprimes())] = [1] 968.64/297.10 ? [5] 968.64/297.10 = [a__zprimes()] 968.64/297.10 968.64/297.10 [a__sieve(X)] = [1] X + [0] 968.64/297.10 ? [1] X + [1] 968.64/297.10 = [sieve(X)] 968.64/297.10 968.64/297.10 [a__sieve(cons(0(), Y))] = [0] 968.64/297.10 >= [0] 968.64/297.10 = [cons(0(), sieve(Y))] 968.64/297.10 968.64/297.10 [a__sieve(cons(s(N), Y))] = [1] N + [0] 968.64/297.10 >= [1] N + [0] 968.64/297.10 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.10 968.64/297.10 [a__nats(N)] = [1] N + [0] 968.64/297.10 >= [1] N + [0] 968.64/297.10 = [cons(mark(N), nats(s(N)))] 968.64/297.10 968.64/297.10 [a__nats(X)] = [1] X + [0] 968.64/297.10 >= [1] X + [0] 968.64/297.10 = [nats(X)] 968.64/297.10 968.64/297.10 [a__zprimes()] = [5] 968.64/297.10 > [0] 968.64/297.10 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.10 968.64/297.10 [a__zprimes()] = [5] 968.64/297.10 > [1] 968.64/297.10 = [zprimes()] 968.64/297.10 968.64/297.10 968.64/297.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.10 968.64/297.10 We are left with following problem, upon which TcT provides the 968.64/297.10 certificate YES(O(1),O(n^2)). 968.64/297.10 968.64/297.10 Strict Trs: 968.64/297.10 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.10 , mark(0()) -> 0() 968.64/297.10 , mark(filter(X1, X2, X3)) -> 968.64/297.10 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.10 , mark(s(X)) -> s(mark(X)) 968.64/297.10 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.10 , mark(zprimes()) -> a__zprimes() 968.64/297.10 , a__sieve(X) -> sieve(X) 968.64/297.10 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.10 , a__sieve(cons(s(N), Y)) -> 968.64/297.10 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.10 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.10 , a__nats(X) -> nats(X) } 968.64/297.10 Weak Trs: 968.64/297.10 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.10 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.10 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.10 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.10 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.10 , a__zprimes() -> zprimes() } 968.64/297.10 Obligation: 968.64/297.10 innermost runtime complexity 968.64/297.10 Answer: 968.64/297.10 YES(O(1),O(n^2)) 968.64/297.10 968.64/297.10 The weightgap principle applies (using the following nonconstant 968.64/297.10 growth matrix-interpretation) 968.64/297.10 968.64/297.10 The following argument positions are usable: 968.64/297.10 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.10 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.10 968.64/297.10 TcT has computed the following matrix interpretation satisfying 968.64/297.10 not(EDA) and not(IDA(1)). 968.64/297.10 968.64/297.10 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.10 968.64/297.10 [cons](x1, x2) = [1] x1 + [0] 968.64/297.10 968.64/297.10 [0] = [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [s](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [sieve](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [nats](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__zprimes] = [7] 968.64/297.11 968.64/297.11 [zprimes] = [1] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [0] 968.64/297.11 >= [0] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1] X1 + [0] 968.64/297.11 >= [1] X1 + [0] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [0] 968.64/297.11 >= [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.11 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.11 968.64/297.11 [mark(s(X))] = [1] X + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [s(mark(X))] 968.64/297.11 968.64/297.11 [mark(sieve(X))] = [1] X + [4] 968.64/297.11 > [1] X + [0] 968.64/297.11 = [a__sieve(mark(X))] 968.64/297.11 968.64/297.11 [mark(nats(X))] = [1] X + [4] 968.64/297.11 > [1] X + [0] 968.64/297.11 = [a__nats(mark(X))] 968.64/297.11 968.64/297.11 [mark(zprimes())] = [1] 968.64/297.11 ? [7] 968.64/297.11 = [a__zprimes()] 968.64/297.11 968.64/297.11 [a__sieve(X)] = [1] X + [0] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [sieve(X)] 968.64/297.11 968.64/297.11 [a__sieve(cons(0(), Y))] = [0] 968.64/297.11 >= [0] 968.64/297.11 = [cons(0(), sieve(Y))] 968.64/297.11 968.64/297.11 [a__sieve(cons(s(N), Y))] = [1] N + [0] 968.64/297.11 >= [1] N + [0] 968.64/297.11 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.11 968.64/297.11 [a__nats(N)] = [1] N + [0] 968.64/297.11 >= [1] N + [0] 968.64/297.11 = [cons(mark(N), nats(s(N)))] 968.64/297.11 968.64/297.11 [a__nats(X)] = [1] X + [0] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [nats(X)] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 > [0] 968.64/297.11 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 > [1] 968.64/297.11 = [zprimes()] 968.64/297.11 968.64/297.11 968.64/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.11 968.64/297.11 We are left with following problem, upon which TcT provides the 968.64/297.11 certificate YES(O(1),O(n^2)). 968.64/297.11 968.64/297.11 Strict Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(0()) -> 0() 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.11 , mark(s(X)) -> s(mark(X)) 968.64/297.11 , mark(zprimes()) -> a__zprimes() 968.64/297.11 , a__sieve(X) -> sieve(X) 968.64/297.11 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.11 , a__sieve(cons(s(N), Y)) -> 968.64/297.11 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.11 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.11 , a__nats(X) -> nats(X) } 968.64/297.11 Weak Trs: 968.64/297.11 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.11 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.11 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.11 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.11 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.11 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.11 , a__zprimes() -> zprimes() } 968.64/297.11 Obligation: 968.64/297.11 innermost runtime complexity 968.64/297.11 Answer: 968.64/297.11 YES(O(1),O(n^2)) 968.64/297.11 968.64/297.11 The weightgap principle applies (using the following nonconstant 968.64/297.11 growth matrix-interpretation) 968.64/297.11 968.64/297.11 The following argument positions are usable: 968.64/297.11 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.11 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.11 968.64/297.11 TcT has computed the following matrix interpretation satisfying 968.64/297.11 not(EDA) and not(IDA(1)). 968.64/297.11 968.64/297.11 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [cons](x1, x2) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [0] = [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [s](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [sieve](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1] x1 + [2] 968.64/297.11 968.64/297.11 [nats](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__zprimes] = [3] 968.64/297.11 968.64/297.11 [zprimes] = [1] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [0] 968.64/297.11 >= [0] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1] X1 + [0] 968.64/297.11 >= [1] X1 + [0] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [0] 968.64/297.11 >= [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.11 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.11 968.64/297.11 [mark(s(X))] = [1] X + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [s(mark(X))] 968.64/297.11 968.64/297.11 [mark(sieve(X))] = [1] X + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [a__sieve(mark(X))] 968.64/297.11 968.64/297.11 [mark(nats(X))] = [1] X + [4] 968.64/297.11 > [1] X + [2] 968.64/297.11 = [a__nats(mark(X))] 968.64/297.11 968.64/297.11 [mark(zprimes())] = [1] 968.64/297.11 ? [3] 968.64/297.11 = [a__zprimes()] 968.64/297.11 968.64/297.11 [a__sieve(X)] = [1] X + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [sieve(X)] 968.64/297.11 968.64/297.11 [a__sieve(cons(0(), Y))] = [0] 968.64/297.11 >= [0] 968.64/297.11 = [cons(0(), sieve(Y))] 968.64/297.11 968.64/297.11 [a__sieve(cons(s(N), Y))] = [1] N + [0] 968.64/297.11 >= [1] N + [0] 968.64/297.11 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.11 968.64/297.11 [a__nats(N)] = [1] N + [2] 968.64/297.11 > [1] N + [0] 968.64/297.11 = [cons(mark(N), nats(s(N)))] 968.64/297.11 968.64/297.11 [a__nats(X)] = [1] X + [2] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [nats(X)] 968.64/297.11 968.64/297.11 [a__zprimes()] = [3] 968.64/297.11 > [2] 968.64/297.11 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.11 968.64/297.11 [a__zprimes()] = [3] 968.64/297.11 > [1] 968.64/297.11 = [zprimes()] 968.64/297.11 968.64/297.11 968.64/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.11 968.64/297.11 We are left with following problem, upon which TcT provides the 968.64/297.11 certificate YES(O(1),O(n^2)). 968.64/297.11 968.64/297.11 Strict Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(0()) -> 0() 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.11 , mark(s(X)) -> s(mark(X)) 968.64/297.11 , mark(zprimes()) -> a__zprimes() 968.64/297.11 , a__sieve(X) -> sieve(X) 968.64/297.11 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.11 , a__sieve(cons(s(N), Y)) -> 968.64/297.11 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.11 , a__nats(X) -> nats(X) } 968.64/297.11 Weak Trs: 968.64/297.11 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.11 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.11 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.11 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.11 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.11 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.11 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.11 , a__zprimes() -> zprimes() } 968.64/297.11 Obligation: 968.64/297.11 innermost runtime complexity 968.64/297.11 Answer: 968.64/297.11 YES(O(1),O(n^2)) 968.64/297.11 968.64/297.11 The weightgap principle applies (using the following nonconstant 968.64/297.11 growth matrix-interpretation) 968.64/297.11 968.64/297.11 The following argument positions are usable: 968.64/297.11 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.11 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.11 968.64/297.11 TcT has computed the following matrix interpretation satisfying 968.64/297.11 not(EDA) and not(IDA(1)). 968.64/297.11 968.64/297.11 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [cons](x1, x2) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [0] = [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [s](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1] x1 + [1] 968.64/297.11 968.64/297.11 [sieve](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [nats](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__zprimes] = [4] 968.64/297.11 968.64/297.11 [zprimes] = [0] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [0] 968.64/297.11 >= [0] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1] X1 + [0] 968.64/297.11 >= [1] X1 + [0] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [0] 968.64/297.11 >= [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.11 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 >= [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.11 968.64/297.11 [mark(s(X))] = [1] X + [0] 968.64/297.11 >= [1] X + [0] 968.64/297.11 = [s(mark(X))] 968.64/297.11 968.64/297.11 [mark(sieve(X))] = [1] X + [4] 968.64/297.11 > [1] X + [1] 968.64/297.11 = [a__sieve(mark(X))] 968.64/297.11 968.64/297.11 [mark(nats(X))] = [1] X + [4] 968.64/297.11 > [1] X + [0] 968.64/297.11 = [a__nats(mark(X))] 968.64/297.11 968.64/297.11 [mark(zprimes())] = [0] 968.64/297.11 ? [4] 968.64/297.11 = [a__zprimes()] 968.64/297.11 968.64/297.11 [a__sieve(X)] = [1] X + [1] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [sieve(X)] 968.64/297.11 968.64/297.11 [a__sieve(cons(0(), Y))] = [1] 968.64/297.11 > [0] 968.64/297.11 = [cons(0(), sieve(Y))] 968.64/297.11 968.64/297.11 [a__sieve(cons(s(N), Y))] = [1] N + [1] 968.64/297.11 > [1] N + [0] 968.64/297.11 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.11 968.64/297.11 [a__nats(N)] = [1] N + [0] 968.64/297.11 >= [1] N + [0] 968.64/297.11 = [cons(mark(N), nats(s(N)))] 968.64/297.11 968.64/297.11 [a__nats(X)] = [1] X + [0] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [nats(X)] 968.64/297.11 968.64/297.11 [a__zprimes()] = [4] 968.64/297.11 > [1] 968.64/297.11 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.11 968.64/297.11 [a__zprimes()] = [4] 968.64/297.11 > [0] 968.64/297.11 = [zprimes()] 968.64/297.11 968.64/297.11 968.64/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.11 968.64/297.11 We are left with following problem, upon which TcT provides the 968.64/297.11 certificate YES(O(1),O(n^2)). 968.64/297.11 968.64/297.11 Strict Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(0()) -> 0() 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.11 , mark(s(X)) -> s(mark(X)) 968.64/297.11 , mark(zprimes()) -> a__zprimes() 968.64/297.11 , a__sieve(X) -> sieve(X) 968.64/297.11 , a__nats(X) -> nats(X) } 968.64/297.11 Weak Trs: 968.64/297.11 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.11 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.11 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.11 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.11 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.11 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.11 , a__sieve(cons(s(N), Y)) -> 968.64/297.11 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.11 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.11 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.11 , a__zprimes() -> zprimes() } 968.64/297.11 Obligation: 968.64/297.11 innermost runtime complexity 968.64/297.11 Answer: 968.64/297.11 YES(O(1),O(n^2)) 968.64/297.11 968.64/297.11 The weightgap principle applies (using the following nonconstant 968.64/297.11 growth matrix-interpretation) 968.64/297.11 968.64/297.11 The following argument positions are usable: 968.64/297.11 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.11 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.11 968.64/297.11 TcT has computed the following matrix interpretation satisfying 968.64/297.11 not(EDA) and not(IDA(1)). 968.64/297.11 968.64/297.11 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [5] 968.64/297.11 968.64/297.11 [cons](x1, x2) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [0] = [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [s](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1] x1 + [1] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [sieve](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1] x1 + [3] 968.64/297.11 968.64/297.11 [nats](x1) = [1] x1 + [3] 968.64/297.11 968.64/297.11 [a__zprimes] = [7] 968.64/297.11 968.64/297.11 [zprimes] = [0] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [5] 968.64/297.11 > [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [5] 968.64/297.11 > [0] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [5] 968.64/297.11 > [1] X + [1] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1] X1 + [1] 968.64/297.11 >= [1] X1 + [1] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [1] 968.64/297.11 > [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.11 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [1] 968.64/297.11 ? [1] X1 + [1] X2 + [1] X3 + [8] 968.64/297.11 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.11 968.64/297.11 [mark(s(X))] = [1] X + [1] 968.64/297.11 >= [1] X + [1] 968.64/297.11 = [s(mark(X))] 968.64/297.11 968.64/297.11 [mark(sieve(X))] = [1] X + [5] 968.64/297.11 >= [1] X + [5] 968.64/297.11 = [a__sieve(mark(X))] 968.64/297.11 968.64/297.11 [mark(nats(X))] = [1] X + [4] 968.64/297.11 >= [1] X + [4] 968.64/297.11 = [a__nats(mark(X))] 968.64/297.11 968.64/297.11 [mark(zprimes())] = [1] 968.64/297.11 ? [7] 968.64/297.11 = [a__zprimes()] 968.64/297.11 968.64/297.11 [a__sieve(X)] = [1] X + [4] 968.64/297.11 >= [1] X + [4] 968.64/297.11 = [sieve(X)] 968.64/297.11 968.64/297.11 [a__sieve(cons(0(), Y))] = [4] 968.64/297.11 > [0] 968.64/297.11 = [cons(0(), sieve(Y))] 968.64/297.11 968.64/297.11 [a__sieve(cons(s(N), Y))] = [1] N + [4] 968.64/297.11 > [1] N + [1] 968.64/297.11 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.11 968.64/297.11 [a__nats(N)] = [1] N + [3] 968.64/297.11 > [1] N + [1] 968.64/297.11 = [cons(mark(N), nats(s(N)))] 968.64/297.11 968.64/297.11 [a__nats(X)] = [1] X + [3] 968.64/297.11 >= [1] X + [3] 968.64/297.11 = [nats(X)] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 >= [7] 968.64/297.11 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 > [0] 968.64/297.11 = [zprimes()] 968.64/297.11 968.64/297.11 968.64/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.11 968.64/297.11 We are left with following problem, upon which TcT provides the 968.64/297.11 certificate YES(O(1),O(n^2)). 968.64/297.11 968.64/297.11 Strict Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.11 , mark(s(X)) -> s(mark(X)) 968.64/297.11 , mark(zprimes()) -> a__zprimes() 968.64/297.11 , a__sieve(X) -> sieve(X) 968.64/297.11 , a__nats(X) -> nats(X) } 968.64/297.11 Weak Trs: 968.64/297.11 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.11 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.11 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.11 , mark(0()) -> 0() 968.64/297.11 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.11 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.11 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.11 , a__sieve(cons(s(N), Y)) -> 968.64/297.11 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.11 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.11 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.11 , a__zprimes() -> zprimes() } 968.64/297.11 Obligation: 968.64/297.11 innermost runtime complexity 968.64/297.11 Answer: 968.64/297.11 YES(O(1),O(n^2)) 968.64/297.11 968.64/297.11 The weightgap principle applies (using the following nonconstant 968.64/297.11 growth matrix-interpretation) 968.64/297.11 968.64/297.11 The following argument positions are usable: 968.64/297.11 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.11 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.11 968.64/297.11 TcT has computed the following matrix interpretation satisfying 968.64/297.11 not(EDA) and not(IDA(1)). 968.64/297.11 968.64/297.11 [a__filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [5] 968.64/297.11 968.64/297.11 [cons](x1, x2) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [0] = [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 968.64/297.11 968.64/297.11 [s](x1) = [1] x1 + [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1] x1 + [1] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [sieve](x1) = [1] x1 + [7] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1] x1 + [1] 968.64/297.11 968.64/297.11 [nats](x1) = [1] x1 + [4] 968.64/297.11 968.64/297.11 [a__zprimes] = [7] 968.64/297.11 968.64/297.11 [zprimes] = [7] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [5] 968.64/297.11 > [1] X1 + [1] X2 + [1] X3 + [0] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1] X + [1] M + [5] 968.64/297.11 > [0] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1] X + [1] M + [1] N + [5] 968.64/297.11 > [1] X + [1] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1] X1 + [1] 968.64/297.11 >= [1] X1 + [1] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [1] 968.64/297.11 > [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.11 [mark(filter(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [1] 968.64/297.11 ? [1] X1 + [1] X2 + [1] X3 + [8] 968.64/297.11 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.11 968.64/297.11 [mark(s(X))] = [1] X + [1] 968.64/297.11 >= [1] X + [1] 968.64/297.11 = [s(mark(X))] 968.64/297.11 968.64/297.11 [mark(sieve(X))] = [1] X + [8] 968.64/297.11 > [1] X + [5] 968.64/297.11 = [a__sieve(mark(X))] 968.64/297.11 968.64/297.11 [mark(nats(X))] = [1] X + [5] 968.64/297.11 > [1] X + [2] 968.64/297.11 = [a__nats(mark(X))] 968.64/297.11 968.64/297.11 [mark(zprimes())] = [8] 968.64/297.11 > [7] 968.64/297.11 = [a__zprimes()] 968.64/297.11 968.64/297.11 [a__sieve(X)] = [1] X + [4] 968.64/297.11 ? [1] X + [7] 968.64/297.11 = [sieve(X)] 968.64/297.11 968.64/297.11 [a__sieve(cons(0(), Y))] = [4] 968.64/297.11 > [0] 968.64/297.11 = [cons(0(), sieve(Y))] 968.64/297.11 968.64/297.11 [a__sieve(cons(s(N), Y))] = [1] N + [4] 968.64/297.11 > [1] N + [1] 968.64/297.11 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.11 968.64/297.11 [a__nats(N)] = [1] N + [1] 968.64/297.11 >= [1] N + [1] 968.64/297.11 = [cons(mark(N), nats(s(N)))] 968.64/297.11 968.64/297.11 [a__nats(X)] = [1] X + [1] 968.64/297.11 ? [1] X + [4] 968.64/297.11 = [nats(X)] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 > [5] 968.64/297.11 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.11 968.64/297.11 [a__zprimes()] = [7] 968.64/297.11 >= [7] 968.64/297.11 = [zprimes()] 968.64/297.11 968.64/297.11 968.64/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 968.64/297.11 968.64/297.11 We are left with following problem, upon which TcT provides the 968.64/297.11 certificate YES(O(1),O(n^2)). 968.64/297.11 968.64/297.11 Strict Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.11 , mark(s(X)) -> s(mark(X)) 968.64/297.11 , a__sieve(X) -> sieve(X) 968.64/297.11 , a__nats(X) -> nats(X) } 968.64/297.11 Weak Trs: 968.64/297.11 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.11 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.11 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.11 , mark(0()) -> 0() 968.64/297.11 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.11 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.11 , mark(zprimes()) -> a__zprimes() 968.64/297.11 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.11 , a__sieve(cons(s(N), Y)) -> 968.64/297.11 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.11 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.11 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.11 , a__zprimes() -> zprimes() } 968.64/297.11 Obligation: 968.64/297.11 innermost runtime complexity 968.64/297.11 Answer: 968.64/297.11 YES(O(1),O(n^2)) 968.64/297.11 968.64/297.11 We use the processor 'matrix interpretation of dimension 2' to 968.64/297.11 orient following rules strictly. 968.64/297.11 968.64/297.11 Trs: 968.64/297.11 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.11 , mark(filter(X1, X2, X3)) -> 968.64/297.11 a__filter(mark(X1), mark(X2), mark(X3)) } 968.64/297.11 968.64/297.11 The induced complexity on above rules (modulo remaining rules) is 968.64/297.11 YES(?,O(n^2)) . These rules are moved into the corresponding weak 968.64/297.11 component(s). 968.64/297.11 968.64/297.11 Sub-proof: 968.64/297.11 ---------- 968.64/297.11 The following argument positions are usable: 968.64/297.11 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.11 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.11 968.64/297.11 TcT has computed the following constructor-based matrix 968.64/297.11 interpretation satisfying not(EDA). 968.64/297.11 968.64/297.11 [a__filter](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [7] 968.64/297.11 [0 1] [0 1] [0 1] [1] 968.64/297.11 968.64/297.11 [cons](x1, x2) = [1 0] x1 + [0] 968.64/297.11 [0 1] [4] 968.64/297.11 968.64/297.11 [0] = [0] 968.64/297.11 [0] 968.64/297.11 968.64/297.11 [filter](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [7] 968.64/297.11 [0 1] [0 1] [0 1] [1] 968.64/297.11 968.64/297.11 [s](x1) = [1 0] x1 + [0] 968.64/297.11 [0 1] [0] 968.64/297.11 968.64/297.11 [mark](x1) = [1 1] x1 + [0] 968.64/297.11 [0 1] [0] 968.64/297.11 968.64/297.11 [a__sieve](x1) = [1 1] x1 + [3] 968.64/297.11 [0 1] [1] 968.64/297.11 968.64/297.11 [sieve](x1) = [1 1] x1 + [3] 968.64/297.11 [0 1] [1] 968.64/297.11 968.64/297.11 [a__nats](x1) = [1 1] x1 + [0] 968.64/297.11 [0 1] [4] 968.64/297.11 968.64/297.11 [nats](x1) = [1 1] x1 + [0] 968.64/297.11 [0 1] [4] 968.64/297.11 968.64/297.11 [a__zprimes] = [7] 968.64/297.11 [7] 968.64/297.11 968.64/297.11 [zprimes] = [0] 968.64/297.11 [7] 968.64/297.11 968.64/297.11 The order satisfies the following ordering constraints: 968.64/297.11 968.64/297.11 [a__filter(X1, X2, X3)] = [1 1] X1 + [1 0] X2 + [1 0] X3 + [7] 968.64/297.11 [0 1] [0 1] [0 1] [1] 968.64/297.11 >= [1 1] X1 + [1 0] X2 + [1 0] X3 + [7] 968.64/297.11 [0 1] [0 1] [0 1] [1] 968.64/297.11 = [filter(X1, X2, X3)] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), 0(), M)] = [1 1] X + [1 0] M + [11] 968.64/297.11 [0 1] [0 1] [5] 968.64/297.11 > [0] 968.64/297.11 [4] 968.64/297.11 = [cons(0(), filter(Y, M, M))] 968.64/297.11 968.64/297.11 [a__filter(cons(X, Y), s(N), M)] = [1 1] X + [1 0] M + [1 0] N + [11] 968.64/297.11 [0 1] [0 1] [0 1] [5] 968.64/297.11 > [1 1] X + [0] 968.64/297.11 [0 1] [4] 968.64/297.11 = [cons(mark(X), filter(Y, N, M))] 968.64/297.11 968.64/297.11 [mark(cons(X1, X2))] = [1 1] X1 + [4] 968.64/297.11 [0 1] [4] 968.64/297.11 > [1 1] X1 + [0] 968.64/297.11 [0 1] [4] 968.64/297.11 = [cons(mark(X1), X2)] 968.64/297.11 968.64/297.11 [mark(0())] = [0] 968.64/297.11 [0] 968.64/297.11 >= [0] 968.64/297.11 [0] 968.64/297.11 = [0()] 968.64/297.11 968.64/297.12 [mark(filter(X1, X2, X3))] = [1 2] X1 + [1 1] X2 + [1 1] X3 + [8] 968.64/297.12 [0 1] [0 1] [0 1] [1] 968.64/297.12 > [1 2] X1 + [1 1] X2 + [1 1] X3 + [7] 968.64/297.12 [0 1] [0 1] [0 1] [1] 968.64/297.12 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.12 968.64/297.12 [mark(s(X))] = [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [s(mark(X))] 968.64/297.12 968.64/297.12 [mark(sieve(X))] = [1 2] X + [4] 968.64/297.12 [0 1] [1] 968.64/297.12 > [1 2] X + [3] 968.64/297.12 [0 1] [1] 968.64/297.12 = [a__sieve(mark(X))] 968.64/297.12 968.64/297.12 [mark(nats(X))] = [1 2] X + [4] 968.64/297.12 [0 1] [4] 968.64/297.12 > [1 2] X + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 = [a__nats(mark(X))] 968.64/297.12 968.64/297.12 [mark(zprimes())] = [7] 968.64/297.12 [7] 968.64/297.12 >= [7] 968.64/297.12 [7] 968.64/297.12 = [a__zprimes()] 968.64/297.12 968.64/297.12 [a__sieve(X)] = [1 1] X + [3] 968.64/297.12 [0 1] [1] 968.64/297.12 >= [1 1] X + [3] 968.64/297.12 [0 1] [1] 968.64/297.12 = [sieve(X)] 968.64/297.12 968.64/297.12 [a__sieve(cons(0(), Y))] = [7] 968.64/297.12 [5] 968.64/297.12 > [0] 968.64/297.12 [4] 968.64/297.12 = [cons(0(), sieve(Y))] 968.64/297.12 968.64/297.12 [a__sieve(cons(s(N), Y))] = [1 1] N + [7] 968.64/297.12 [0 1] [5] 968.64/297.12 > [1 1] N + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.12 968.64/297.12 [a__nats(N)] = [1 1] N + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 >= [1 1] N + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 = [cons(mark(N), nats(s(N)))] 968.64/297.12 968.64/297.12 [a__nats(X)] = [1 1] X + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 = [nats(X)] 968.64/297.12 968.64/297.12 [a__zprimes()] = [7] 968.64/297.12 [7] 968.64/297.12 >= [7] 968.64/297.12 [5] 968.64/297.12 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.12 968.64/297.12 [a__zprimes()] = [7] 968.64/297.12 [7] 968.64/297.12 > [0] 968.64/297.12 [7] 968.64/297.12 = [zprimes()] 968.64/297.12 968.64/297.12 968.64/297.12 We return to the main proof. 968.64/297.12 968.64/297.12 We are left with following problem, upon which TcT provides the 968.64/297.12 certificate YES(O(1),O(n^2)). 968.64/297.12 968.64/297.12 Strict Trs: 968.64/297.12 { mark(s(X)) -> s(mark(X)) 968.64/297.12 , a__sieve(X) -> sieve(X) 968.64/297.12 , a__nats(X) -> nats(X) } 968.64/297.12 Weak Trs: 968.64/297.12 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.12 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.12 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.12 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.12 , mark(0()) -> 0() 968.64/297.12 , mark(filter(X1, X2, X3)) -> 968.64/297.12 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.12 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.12 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.12 , mark(zprimes()) -> a__zprimes() 968.64/297.12 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.12 , a__sieve(cons(s(N), Y)) -> 968.64/297.12 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.12 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.12 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.12 , a__zprimes() -> zprimes() } 968.64/297.12 Obligation: 968.64/297.12 innermost runtime complexity 968.64/297.12 Answer: 968.64/297.12 YES(O(1),O(n^2)) 968.64/297.12 968.64/297.12 We use the processor 'matrix interpretation of dimension 2' to 968.64/297.12 orient following rules strictly. 968.64/297.12 968.64/297.12 Trs: { a__nats(X) -> nats(X) } 968.64/297.12 968.64/297.12 The induced complexity on above rules (modulo remaining rules) is 968.64/297.12 YES(?,O(n^2)) . These rules are moved into the corresponding weak 968.64/297.12 component(s). 968.64/297.12 968.64/297.12 Sub-proof: 968.64/297.12 ---------- 968.64/297.12 The following argument positions are usable: 968.64/297.12 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.12 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.12 968.64/297.12 TcT has computed the following constructor-based matrix 968.64/297.12 interpretation satisfying not(EDA). 968.64/297.12 968.64/297.12 [a__filter](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [cons](x1, x2) = [1 0] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [0] = [0] 968.64/297.12 [0] 968.64/297.12 968.64/297.12 [filter](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [s](x1) = [1 0] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [mark](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__sieve](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [sieve](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__nats](x1) = [1 4] x1 + [1] 968.64/297.12 [0 1] [4] 968.64/297.12 968.64/297.12 [nats](x1) = [1 4] x1 + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 968.64/297.12 [a__zprimes] = [5] 968.64/297.12 [4] 968.64/297.12 968.64/297.12 [zprimes] = [4] 968.64/297.12 [4] 968.64/297.12 968.64/297.12 The order satisfies the following ordering constraints: 968.64/297.12 968.64/297.12 [a__filter(X1, X2, X3)] = [1 2] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 2] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [filter(X1, X2, X3)] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), 0(), M)] = [1 2] X + [1 0] M + [0] 968.64/297.12 [0 1] [0 1] [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), filter(Y, M, M))] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), s(N), M)] = [1 2] X + [1 0] M + [1 0] N + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X), filter(Y, N, M))] 968.64/297.12 968.64/297.12 [mark(cons(X1, X2))] = [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X1), X2)] 968.64/297.12 968.64/297.12 [mark(0())] = [0] 968.64/297.12 [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [0()] 968.64/297.12 968.64/297.12 [mark(filter(X1, X2, X3))] = [1 3] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 3] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.12 968.64/297.12 [mark(s(X))] = [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [s(mark(X))] 968.64/297.12 968.64/297.12 [mark(sieve(X))] = [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [a__sieve(mark(X))] 968.64/297.12 968.64/297.12 [mark(nats(X))] = [1 5] X + [4] 968.64/297.12 [0 1] [4] 968.64/297.12 > [1 5] X + [1] 968.64/297.12 [0 1] [4] 968.64/297.12 = [a__nats(mark(X))] 968.64/297.12 968.64/297.12 [mark(zprimes())] = [8] 968.64/297.12 [4] 968.64/297.12 > [5] 968.64/297.12 [4] 968.64/297.12 = [a__zprimes()] 968.64/297.12 968.64/297.12 [a__sieve(X)] = [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [sieve(X)] 968.64/297.12 968.64/297.12 [a__sieve(cons(0(), Y))] = [0] 968.64/297.12 [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), sieve(Y))] 968.64/297.12 968.64/297.12 [a__sieve(cons(s(N), Y))] = [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.12 968.64/297.12 [a__nats(N)] = [1 4] N + [1] 968.64/297.12 [0 1] [4] 968.64/297.12 > [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(N), nats(s(N)))] 968.64/297.12 968.64/297.12 [a__nats(X)] = [1 4] X + [1] 968.64/297.12 [0 1] [4] 968.64/297.12 > [1 4] X + [0] 968.64/297.12 [0 1] [4] 968.64/297.12 = [nats(X)] 968.64/297.12 968.64/297.12 [a__zprimes()] = [5] 968.64/297.12 [4] 968.64/297.12 >= [5] 968.64/297.12 [4] 968.64/297.12 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.12 968.64/297.12 [a__zprimes()] = [5] 968.64/297.12 [4] 968.64/297.12 > [4] 968.64/297.12 [4] 968.64/297.12 = [zprimes()] 968.64/297.12 968.64/297.12 968.64/297.12 We return to the main proof. 968.64/297.12 968.64/297.12 We are left with following problem, upon which TcT provides the 968.64/297.12 certificate YES(O(1),O(n^2)). 968.64/297.12 968.64/297.12 Strict Trs: 968.64/297.12 { mark(s(X)) -> s(mark(X)) 968.64/297.12 , a__sieve(X) -> sieve(X) } 968.64/297.12 Weak Trs: 968.64/297.12 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.12 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.12 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.12 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.12 , mark(0()) -> 0() 968.64/297.12 , mark(filter(X1, X2, X3)) -> 968.64/297.12 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.12 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.12 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.12 , mark(zprimes()) -> a__zprimes() 968.64/297.12 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.12 , a__sieve(cons(s(N), Y)) -> 968.64/297.12 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.12 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.12 , a__nats(X) -> nats(X) 968.64/297.12 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.12 , a__zprimes() -> zprimes() } 968.64/297.12 Obligation: 968.64/297.12 innermost runtime complexity 968.64/297.12 Answer: 968.64/297.12 YES(O(1),O(n^2)) 968.64/297.12 968.64/297.12 We use the processor 'matrix interpretation of dimension 2' to 968.64/297.12 orient following rules strictly. 968.64/297.12 968.64/297.12 Trs: { a__sieve(X) -> sieve(X) } 968.64/297.12 968.64/297.12 The induced complexity on above rules (modulo remaining rules) is 968.64/297.12 YES(?,O(n^2)) . These rules are moved into the corresponding weak 968.64/297.12 component(s). 968.64/297.12 968.64/297.12 Sub-proof: 968.64/297.12 ---------- 968.64/297.12 The following argument positions are usable: 968.64/297.12 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.12 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.12 968.64/297.12 TcT has computed the following constructor-based matrix 968.64/297.12 interpretation satisfying not(EDA). 968.64/297.12 968.64/297.12 [a__filter](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [cons](x1, x2) = [1 0] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [0] = [0] 968.64/297.12 [0] 968.64/297.12 968.64/297.12 [filter](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [s](x1) = [1 0] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [mark](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__sieve](x1) = [1 4] x1 + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 968.64/297.12 [sieve](x1) = [1 4] x1 + [0] 968.64/297.12 [0 1] [1] 968.64/297.12 968.64/297.12 [a__nats](x1) = [1 2] x1 + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [nats](x1) = [1 2] x1 + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__zprimes] = [7] 968.64/297.12 [1] 968.64/297.12 968.64/297.12 [zprimes] = [7] 968.64/297.12 [1] 968.64/297.12 968.64/297.12 The order satisfies the following ordering constraints: 968.64/297.12 968.64/297.12 [a__filter(X1, X2, X3)] = [1 2] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 2] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [filter(X1, X2, X3)] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), 0(), M)] = [1 2] X + [1 0] M + [0] 968.64/297.12 [0 1] [0 1] [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), filter(Y, M, M))] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), s(N), M)] = [1 2] X + [1 0] M + [1 0] N + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X), filter(Y, N, M))] 968.64/297.12 968.64/297.12 [mark(cons(X1, X2))] = [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X1), X2)] 968.64/297.12 968.64/297.12 [mark(0())] = [0] 968.64/297.12 [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [0()] 968.64/297.12 968.64/297.12 [mark(filter(X1, X2, X3))] = [1 3] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 3] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.12 968.64/297.12 [mark(s(X))] = [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [s(mark(X))] 968.64/297.12 968.64/297.12 [mark(sieve(X))] = [1 5] X + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 >= [1 5] X + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 = [a__sieve(mark(X))] 968.64/297.12 968.64/297.12 [mark(nats(X))] = [1 3] X + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 3] X + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 = [a__nats(mark(X))] 968.64/297.12 968.64/297.12 [mark(zprimes())] = [8] 968.64/297.12 [1] 968.64/297.12 > [7] 968.64/297.12 [1] 968.64/297.12 = [a__zprimes()] 968.64/297.12 968.64/297.12 [a__sieve(X)] = [1 4] X + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 > [1 4] X + [0] 968.64/297.12 [0 1] [1] 968.64/297.12 = [sieve(X)] 968.64/297.12 968.64/297.12 [a__sieve(cons(0(), Y))] = [1] 968.64/297.12 [1] 968.64/297.12 > [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), sieve(Y))] 968.64/297.12 968.64/297.12 [a__sieve(cons(s(N), Y))] = [1 4] N + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 > [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.12 968.64/297.12 [a__nats(N)] = [1 2] N + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 > [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(N), nats(s(N)))] 968.64/297.12 968.64/297.12 [a__nats(X)] = [1 2] X + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 2] X + [4] 968.64/297.12 [0 1] [0] 968.64/297.12 = [nats(X)] 968.64/297.12 968.64/297.12 [a__zprimes()] = [7] 968.64/297.12 [1] 968.64/297.12 > [5] 968.64/297.12 [1] 968.64/297.12 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.12 968.64/297.12 [a__zprimes()] = [7] 968.64/297.12 [1] 968.64/297.12 >= [7] 968.64/297.12 [1] 968.64/297.12 = [zprimes()] 968.64/297.12 968.64/297.12 968.64/297.12 We return to the main proof. 968.64/297.12 968.64/297.12 We are left with following problem, upon which TcT provides the 968.64/297.12 certificate YES(O(1),O(n^2)). 968.64/297.12 968.64/297.12 Strict Trs: { mark(s(X)) -> s(mark(X)) } 968.64/297.12 Weak Trs: 968.64/297.12 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.12 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.12 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.12 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.12 , mark(0()) -> 0() 968.64/297.12 , mark(filter(X1, X2, X3)) -> 968.64/297.12 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.12 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.12 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.12 , mark(zprimes()) -> a__zprimes() 968.64/297.12 , a__sieve(X) -> sieve(X) 968.64/297.12 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.12 , a__sieve(cons(s(N), Y)) -> 968.64/297.12 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.12 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.12 , a__nats(X) -> nats(X) 968.64/297.12 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.12 , a__zprimes() -> zprimes() } 968.64/297.12 Obligation: 968.64/297.12 innermost runtime complexity 968.64/297.12 Answer: 968.64/297.12 YES(O(1),O(n^2)) 968.64/297.12 968.64/297.12 We use the processor 'matrix interpretation of dimension 2' to 968.64/297.12 orient following rules strictly. 968.64/297.12 968.64/297.12 Trs: { mark(s(X)) -> s(mark(X)) } 968.64/297.12 968.64/297.12 The induced complexity on above rules (modulo remaining rules) is 968.64/297.12 YES(?,O(n^2)) . These rules are moved into the corresponding weak 968.64/297.12 component(s). 968.64/297.12 968.64/297.12 Sub-proof: 968.64/297.12 ---------- 968.64/297.12 The following argument positions are usable: 968.64/297.12 Uargs(a__filter) = {1, 2, 3}, Uargs(cons) = {1}, Uargs(s) = {1}, 968.64/297.12 Uargs(a__sieve) = {1}, Uargs(a__nats) = {1} 968.64/297.12 968.64/297.12 TcT has computed the following constructor-based matrix 968.64/297.12 interpretation satisfying not(EDA). 968.64/297.12 968.64/297.12 [a__filter](x1, x2, x3) = [1 4] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [cons](x1, x2) = [1 0] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [0] = [0] 968.64/297.12 [0] 968.64/297.12 968.64/297.12 [filter](x1, x2, x3) = [1 4] x1 + [1 0] x2 + [1 0] x3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 968.64/297.12 [s](x1) = [1 0] x1 + [0] 968.64/297.12 [0 1] [1] 968.64/297.12 968.64/297.12 [mark](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__sieve](x1) = [1 2] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [sieve](x1) = [1 2] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__nats](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [nats](x1) = [1 1] x1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 968.64/297.12 [a__zprimes] = [6] 968.64/297.12 [5] 968.64/297.12 968.64/297.12 [zprimes] = [3] 968.64/297.12 [5] 968.64/297.12 968.64/297.12 The order satisfies the following ordering constraints: 968.64/297.12 968.64/297.12 [a__filter(X1, X2, X3)] = [1 4] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 4] X1 + [1 0] X2 + [1 0] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [filter(X1, X2, X3)] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), 0(), M)] = [1 4] X + [1 0] M + [0] 968.64/297.12 [0 1] [0 1] [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), filter(Y, M, M))] 968.64/297.12 968.64/297.12 [a__filter(cons(X, Y), s(N), M)] = [1 4] X + [1 0] M + [1 0] N + [0] 968.64/297.12 [0 1] [0 1] [0 1] [1] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X), filter(Y, N, M))] 968.64/297.12 968.64/297.12 [mark(cons(X1, X2))] = [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X1 + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(X1), X2)] 968.64/297.12 968.64/297.12 [mark(0())] = [0] 968.64/297.12 [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [0()] 968.64/297.12 968.64/297.12 [mark(filter(X1, X2, X3))] = [1 5] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 >= [1 5] X1 + [1 1] X2 + [1 1] X3 + [0] 968.64/297.12 [0 1] [0 1] [0 1] [0] 968.64/297.12 = [a__filter(mark(X1), mark(X2), mark(X3))] 968.64/297.12 968.64/297.12 [mark(s(X))] = [1 1] X + [1] 968.64/297.12 [0 1] [1] 968.64/297.12 > [1 1] X + [0] 968.64/297.12 [0 1] [1] 968.64/297.12 = [s(mark(X))] 968.64/297.12 968.64/297.12 [mark(sieve(X))] = [1 3] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 3] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [a__sieve(mark(X))] 968.64/297.12 968.64/297.12 [mark(nats(X))] = [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [a__nats(mark(X))] 968.64/297.12 968.64/297.12 [mark(zprimes())] = [8] 968.64/297.12 [5] 968.64/297.12 > [6] 968.64/297.12 [5] 968.64/297.12 = [a__zprimes()] 968.64/297.12 968.64/297.12 [a__sieve(X)] = [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 2] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [sieve(X)] 968.64/297.12 968.64/297.12 [a__sieve(cons(0(), Y))] = [0] 968.64/297.12 [0] 968.64/297.12 >= [0] 968.64/297.12 [0] 968.64/297.12 = [cons(0(), sieve(Y))] 968.64/297.12 968.64/297.12 [a__sieve(cons(s(N), Y))] = [1 2] N + [2] 968.64/297.12 [0 1] [1] 968.64/297.12 > [1 1] N + [0] 968.64/297.12 [0 1] [1] 968.64/297.12 = [cons(s(mark(N)), sieve(filter(Y, N, N)))] 968.64/297.12 968.64/297.12 [a__nats(N)] = [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] N + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [cons(mark(N), nats(s(N)))] 968.64/297.12 968.64/297.12 [a__nats(X)] = [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 >= [1 1] X + [0] 968.64/297.12 [0 1] [0] 968.64/297.12 = [nats(X)] 968.64/297.12 968.64/297.12 [a__zprimes()] = [6] 968.64/297.12 [5] 968.64/297.12 >= [6] 968.64/297.12 [2] 968.64/297.12 = [a__sieve(a__nats(s(s(0()))))] 968.64/297.12 968.64/297.12 [a__zprimes()] = [6] 968.64/297.12 [5] 968.64/297.12 > [3] 968.64/297.12 [5] 968.64/297.12 = [zprimes()] 968.64/297.12 968.64/297.12 968.64/297.12 We return to the main proof. 968.64/297.12 968.64/297.12 We are left with following problem, upon which TcT provides the 968.64/297.12 certificate YES(O(1),O(1)). 968.64/297.12 968.64/297.12 Weak Trs: 968.64/297.12 { a__filter(X1, X2, X3) -> filter(X1, X2, X3) 968.64/297.12 , a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 968.64/297.12 , a__filter(cons(X, Y), s(N), M) -> cons(mark(X), filter(Y, N, M)) 968.64/297.12 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 968.64/297.12 , mark(0()) -> 0() 968.64/297.12 , mark(filter(X1, X2, X3)) -> 968.64/297.12 a__filter(mark(X1), mark(X2), mark(X3)) 968.64/297.12 , mark(s(X)) -> s(mark(X)) 968.64/297.12 , mark(sieve(X)) -> a__sieve(mark(X)) 968.64/297.12 , mark(nats(X)) -> a__nats(mark(X)) 968.64/297.12 , mark(zprimes()) -> a__zprimes() 968.64/297.12 , a__sieve(X) -> sieve(X) 968.64/297.12 , a__sieve(cons(0(), Y)) -> cons(0(), sieve(Y)) 968.64/297.12 , a__sieve(cons(s(N), Y)) -> 968.64/297.12 cons(s(mark(N)), sieve(filter(Y, N, N))) 968.64/297.12 , a__nats(N) -> cons(mark(N), nats(s(N))) 968.64/297.12 , a__nats(X) -> nats(X) 968.64/297.12 , a__zprimes() -> a__sieve(a__nats(s(s(0())))) 968.64/297.12 , a__zprimes() -> zprimes() } 968.64/297.12 Obligation: 968.64/297.12 innermost runtime complexity 968.64/297.12 Answer: 968.64/297.12 YES(O(1),O(1)) 968.64/297.12 968.64/297.12 Empty rules are trivially bounded 968.64/297.12 968.64/297.12 Hurray, we answered YES(O(1),O(n^2)) 968.79/297.24 EOF