YES(?,O(n^1)) 5.33/2.37 YES(?,O(n^1)) 5.33/2.37 5.33/2.37 We are left with following problem, upon which TcT provides the 5.33/2.37 certificate YES(?,O(n^1)). 5.33/2.37 5.33/2.37 Strict Trs: 5.33/2.37 { filter(cons(X), 0(), M) -> cons(0()) 5.33/2.37 , filter(cons(X), s(N), M) -> cons(X) 5.33/2.37 , sieve(cons(0())) -> cons(0()) 5.33/2.37 , sieve(cons(s(N))) -> cons(s(N)) 5.33/2.37 , nats(N) -> cons(N) 5.33/2.37 , zprimes() -> sieve(nats(s(s(0())))) } 5.33/2.37 Obligation: 5.33/2.37 derivational complexity 5.33/2.37 Answer: 5.33/2.37 YES(?,O(n^1)) 5.33/2.37 5.33/2.37 The problem is match-bounded by 2. The enriched problem is 5.33/2.37 compatible with the following automaton. 5.33/2.37 { filter_0(1, 1, 1) -> 1 5.33/2.37 , cons_0(1) -> 1 5.33/2.37 , cons_1(1) -> 1 5.33/2.37 , cons_1(2) -> 1 5.33/2.37 , cons_1(4) -> 1 5.33/2.37 , cons_1(6) -> 1 5.33/2.37 , cons_2(4) -> 3 5.33/2.37 , cons_2(6) -> 1 5.33/2.37 , 0_0() -> 1 5.33/2.37 , 0_1() -> 2 5.33/2.37 , s_0(1) -> 1 5.33/2.37 , s_1(1) -> 1 5.33/2.37 , s_1(2) -> 5 5.33/2.37 , s_1(5) -> 4 5.33/2.37 , s_2(5) -> 6 5.33/2.37 , sieve_0(1) -> 1 5.33/2.37 , sieve_1(3) -> 1 5.33/2.37 , nats_0(1) -> 1 5.33/2.37 , nats_1(4) -> 3 5.33/2.37 , zprimes_0() -> 1 } 5.33/2.37 5.33/2.37 Hurray, we answered YES(?,O(n^1)) 5.33/2.38 EOF