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