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