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