YES(?,O(n^1)) 12.38/7.07 YES(?,O(n^1)) 12.38/7.07 12.38/7.07 We are left with following problem, upon which TcT provides the 12.38/7.07 certificate YES(?,O(n^1)). 12.38/7.07 12.38/7.07 Strict Trs: 12.38/7.07 { terms(N) -> cons(recip(sqr(N))) 12.38/7.07 , sqr(0()) -> 0() 12.38/7.07 , sqr(s()) -> s() 12.38/7.07 , dbl(0()) -> 0() 12.38/7.07 , dbl(s()) -> s() 12.38/7.07 , add(0(), X) -> X 12.38/7.07 , add(s(), Y) -> s() 12.38/7.07 , first(0(), X) -> nil() 12.38/7.07 , first(s(), cons(Y)) -> cons(Y) } 12.38/7.07 Obligation: 12.38/7.07 derivational complexity 12.38/7.07 Answer: 12.38/7.07 YES(?,O(n^1)) 12.38/7.07 12.38/7.07 TcT has computed the following matrix interpretation satisfying 12.38/7.07 not(EDA) and not(IDA(1)). 12.38/7.07 12.38/7.07 [1 1 0 0] [1] 12.38/7.07 [terms](x1) = [0 0 0 1] x1 + [1] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 12.38/7.07 [1 0 0 0] [0] 12.38/7.07 [cons](x1) = [0 0 0 0] x1 + [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 12.38/7.07 [1 0 0 0] [0] 12.38/7.07 [recip](x1) = [0 0 0 0] x1 + [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 12.38/7.07 [1 1 0 0] [0] 12.38/7.07 [sqr](x1) = [0 0 0 1] x1 + [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 12.38/7.07 [0] 12.38/7.07 [0] = [1] 12.38/7.07 [0] 12.38/7.07 [1] 12.38/7.07 12.38/7.07 [0] 12.38/7.07 [s] = [1] 12.38/7.07 [0] 12.38/7.07 [1] 12.38/7.07 12.38/7.07 [1 1 0 0] [1] 12.38/7.07 [dbl](x1) = [0 0 0 1] x1 + [0] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 12.38/7.07 [1 0 0 0] [1 0 0 0] [1] 12.38/7.07 [add](x1, x2) = [0 0 0 0] x1 + [0 1 0 0] x2 + [1] 12.38/7.07 [0 0 0 0] [0 0 1 0] [1] 12.38/7.07 [0 0 0 0] [0 0 0 1] [1] 12.38/7.07 12.38/7.07 [1 0 0 0] [1 1 0 0] [1] 12.38/7.07 [first](x1, x2) = [0 0 0 0] x1 + [0 0 0 1] x2 + [1] 12.38/7.07 [0 0 0 0] [0 0 0 0] [1] 12.38/7.07 [0 0 0 0] [0 0 0 0] [1] 12.38/7.07 12.38/7.07 [0] 12.38/7.07 [nil] = [1] 12.38/7.07 [1] 12.38/7.07 [1] 12.38/7.07 12.38/7.07 The order satisfies the following ordering constraints: 12.38/7.07 12.38/7.07 [terms(N)] = [1 1 0 0] [1] 12.38/7.07 [0 0 0 1] N + [1] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 [0 0 0 0] [1] 12.38/7.07 > [1 1 0 0] [0] 12.38/7.07 [0 0 0 0] N + [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 [0 0 0 0] [0] 12.38/7.07 = [cons(recip(sqr(N)))] 12.38/7.07 12.38/7.07 [sqr(0())] = [1] 12.38/7.07 [1] 12.38/7.07 [0] 12.38/7.07 [1] 12.38/7.07 > [0] 12.38/7.07 [1] 12.38/7.07 [0] 12.38/7.07 [1] 12.38/7.07 = [0()] 12.38/7.08 12.38/7.08 [sqr(s())] = [1] 12.38/7.08 [1] 12.38/7.08 [0] 12.38/7.08 [1] 12.38/7.08 > [0] 12.38/7.08 [1] 12.38/7.08 [0] 12.38/7.08 [1] 12.38/7.08 = [s()] 12.38/7.08 12.38/7.08 [dbl(0())] = [2] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 > [0] 12.38/7.08 [1] 12.38/7.08 [0] 12.38/7.08 [1] 12.38/7.08 = [0()] 12.38/7.08 12.38/7.08 [dbl(s())] = [2] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 > [0] 12.38/7.08 [1] 12.38/7.08 [0] 12.38/7.08 [1] 12.38/7.08 = [s()] 12.38/7.08 12.38/7.08 [add(0(), X)] = [1 0 0 0] [1] 12.38/7.08 [0 1 0 0] X + [1] 12.38/7.08 [0 0 1 0] [1] 12.38/7.08 [0 0 0 1] [1] 12.38/7.08 > [1 0 0 0] [0] 12.38/7.08 [0 1 0 0] X + [0] 12.38/7.08 [0 0 1 0] [0] 12.38/7.08 [0 0 0 1] [0] 12.38/7.08 = [X] 12.38/7.08 12.38/7.08 [add(s(), Y)] = [1 0 0 0] [1] 12.38/7.08 [0 1 0 0] Y + [1] 12.38/7.08 [0 0 1 0] [1] 12.38/7.08 [0 0 0 1] [1] 12.38/7.08 > [0] 12.38/7.08 [1] 12.38/7.08 [0] 12.38/7.08 [1] 12.38/7.08 = [s()] 12.38/7.08 12.38/7.08 [first(0(), X)] = [1 1 0 0] [1] 12.38/7.08 [0 0 0 1] X + [1] 12.38/7.08 [0 0 0 0] [1] 12.38/7.08 [0 0 0 0] [1] 12.38/7.08 > [0] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 [1] 12.38/7.08 = [nil()] 12.38/7.08 12.38/7.08 [first(s(), cons(Y))] = [1 0 0 0] [1] 12.38/7.08 [0 0 0 0] Y + [1] 12.38/7.08 [0 0 0 0] [1] 12.38/7.08 [0 0 0 0] [1] 12.38/7.08 > [1 0 0 0] [0] 12.38/7.08 [0 0 0 0] Y + [0] 12.38/7.08 [0 0 0 0] [0] 12.38/7.08 [0 0 0 0] [0] 12.38/7.08 = [cons(Y)] 12.38/7.08 12.38/7.08 12.38/7.08 Hurray, we answered YES(?,O(n^1)) 12.38/7.09 EOF