YES(O(1),O(n^2)) 70.26/30.95 YES(O(1),O(n^2)) 70.26/30.95 70.26/30.95 We are left with following problem, upon which TcT provides the 70.26/30.95 certificate YES(O(1),O(n^2)). 70.26/30.95 70.26/30.95 Strict Trs: 70.26/30.95 { a__app(X1, X2) -> app(X1, X2) 70.26/30.95 , a__app(nil(), YS) -> mark(YS) 70.26/30.95 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.95 , mark(nil()) -> nil() 70.26/30.95 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.95 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.95 , mark(from(X)) -> a__from(mark(X)) 70.26/30.95 , mark(s(X)) -> s(mark(X)) 70.26/30.95 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.95 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.95 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.95 , a__from(X) -> from(X) 70.26/30.95 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.95 , a__zWadr(XS, nil()) -> nil() 70.26/30.95 , a__zWadr(nil(), YS) -> nil() 70.26/30.95 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.95 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.95 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.95 , a__prefix(X) -> prefix(X) } 70.26/30.95 Obligation: 70.26/30.95 innermost runtime complexity 70.26/30.95 Answer: 70.26/30.95 YES(O(1),O(n^2)) 70.26/30.95 70.26/30.95 The weightgap principle applies (using the following nonconstant 70.26/30.95 growth matrix-interpretation) 70.26/30.95 70.26/30.95 The following argument positions are usable: 70.26/30.95 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.95 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.95 70.26/30.95 TcT has computed the following matrix interpretation satisfying 70.26/30.95 not(EDA) and not(IDA(1)). 70.26/30.95 70.26/30.95 [a__app](x1, x2) = [1] x1 + [1] x2 + [1] 70.26/30.95 70.26/30.95 [nil] = [0] 70.26/30.95 70.26/30.95 [mark](x1) = [0] 70.26/30.95 70.26/30.95 [cons](x1, x2) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [a__from](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [from](x1) = [1] x1 + [7] 70.26/30.95 70.26/30.95 [s](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [zWadr](x1, x2) = [1] x1 + [1] x2 + [7] 70.26/30.95 70.26/30.95 [a__prefix](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [prefix](x1) = [1] x1 + [7] 70.26/30.95 70.26/30.95 The order satisfies the following ordering constraints: 70.26/30.95 70.26/30.95 [a__app(X1, X2)] = [1] X1 + [1] X2 + [1] 70.26/30.95 > [1] X1 + [1] X2 + [0] 70.26/30.95 = [app(X1, X2)] 70.26/30.95 70.26/30.95 [a__app(nil(), YS)] = [1] YS + [1] 70.26/30.95 > [0] 70.26/30.95 = [mark(YS)] 70.26/30.95 70.26/30.95 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [1] 70.26/30.95 > [0] 70.26/30.95 = [cons(mark(X), app(XS, YS))] 70.26/30.95 70.26/30.95 [mark(nil())] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [mark(cons(X1, X2))] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [cons(mark(X1), X2)] 70.26/30.95 70.26/30.95 [mark(app(X1, X2))] = [0] 70.26/30.95 ? [1] 70.26/30.95 = [a__app(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(from(X))] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [a__from(mark(X))] 70.26/30.95 70.26/30.95 [mark(s(X))] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [s(mark(X))] 70.26/30.95 70.26/30.95 [mark(zWadr(X1, X2))] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(prefix(X))] = [0] 70.26/30.95 >= [0] 70.26/30.95 = [a__prefix(mark(X))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 >= [0] 70.26/30.95 = [cons(mark(X), from(s(X)))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 ? [1] X + [7] 70.26/30.95 = [from(X)] 70.26/30.95 70.26/30.95 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 ? [1] X1 + [1] X2 + [7] 70.26/30.95 = [zWadr(X1, X2)] 70.26/30.95 70.26/30.95 [a__zWadr(XS, nil())] = [1] XS + [0] 70.26/30.95 >= [0] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(nil(), YS)] = [1] YS + [0] 70.26/30.95 >= [0] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [0] 70.26/30.95 ? [1] 70.26/30.95 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.95 70.26/30.95 [a__prefix(L)] = [1] L + [0] 70.26/30.95 >= [0] 70.26/30.95 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.95 70.26/30.95 [a__prefix(X)] = [1] X + [0] 70.26/30.95 ? [1] X + [7] 70.26/30.95 = [prefix(X)] 70.26/30.95 70.26/30.95 70.26/30.95 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.95 70.26/30.95 We are left with following problem, upon which TcT provides the 70.26/30.95 certificate YES(O(1),O(n^2)). 70.26/30.95 70.26/30.95 Strict Trs: 70.26/30.95 { mark(nil()) -> nil() 70.26/30.95 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.95 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.95 , mark(from(X)) -> a__from(mark(X)) 70.26/30.95 , mark(s(X)) -> s(mark(X)) 70.26/30.95 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.95 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.95 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.95 , a__from(X) -> from(X) 70.26/30.95 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.95 , a__zWadr(XS, nil()) -> nil() 70.26/30.95 , a__zWadr(nil(), YS) -> nil() 70.26/30.95 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.95 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.95 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.95 , a__prefix(X) -> prefix(X) } 70.26/30.95 Weak Trs: 70.26/30.95 { a__app(X1, X2) -> app(X1, X2) 70.26/30.95 , a__app(nil(), YS) -> mark(YS) 70.26/30.95 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) } 70.26/30.95 Obligation: 70.26/30.95 innermost runtime complexity 70.26/30.95 Answer: 70.26/30.95 YES(O(1),O(n^2)) 70.26/30.95 70.26/30.95 The weightgap principle applies (using the following nonconstant 70.26/30.95 growth matrix-interpretation) 70.26/30.95 70.26/30.95 The following argument positions are usable: 70.26/30.95 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.95 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.95 70.26/30.95 TcT has computed the following matrix interpretation satisfying 70.26/30.95 not(EDA) and not(IDA(1)). 70.26/30.95 70.26/30.95 [a__app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [nil] = [4] 70.26/30.95 70.26/30.95 [mark](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [cons](x1, x2) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [a__from](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [from](x1) = [1] x1 + [4] 70.26/30.95 70.26/30.95 [s](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [a__prefix](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [prefix](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 The order satisfies the following ordering constraints: 70.26/30.95 70.26/30.95 [a__app(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [app(X1, X2)] 70.26/30.95 70.26/30.95 [a__app(nil(), YS)] = [1] YS + [4] 70.26/30.95 > [1] YS + [0] 70.26/30.95 = [mark(YS)] 70.26/30.95 70.26/30.95 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [cons(mark(X), app(XS, YS))] 70.26/30.95 70.26/30.95 [mark(nil())] = [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [mark(cons(X1, X2))] = [1] X1 + [0] 70.26/30.95 >= [1] X1 + [0] 70.26/30.95 = [cons(mark(X1), X2)] 70.26/30.95 70.26/30.95 [mark(app(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [a__app(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(from(X))] = [1] X + [4] 70.26/30.95 > [1] X + [0] 70.26/30.95 = [a__from(mark(X))] 70.26/30.95 70.26/30.95 [mark(s(X))] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [s(mark(X))] 70.26/30.95 70.26/30.95 [mark(zWadr(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(prefix(X))] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [a__prefix(mark(X))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [cons(mark(X), from(s(X)))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 ? [1] X + [4] 70.26/30.95 = [from(X)] 70.26/30.95 70.26/30.95 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [zWadr(X1, X2)] 70.26/30.95 70.26/30.95 [a__zWadr(XS, nil())] = [1] XS + [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(nil(), YS)] = [1] YS + [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [0] 70.26/30.95 >= [1] X + [1] Y + [0] 70.26/30.95 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.95 70.26/30.95 [a__prefix(L)] = [1] L + [0] 70.26/30.95 ? [4] 70.26/30.95 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.95 70.26/30.95 [a__prefix(X)] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [prefix(X)] 70.26/30.95 70.26/30.95 70.26/30.95 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.95 70.26/30.95 We are left with following problem, upon which TcT provides the 70.26/30.95 certificate YES(O(1),O(n^2)). 70.26/30.95 70.26/30.95 Strict Trs: 70.26/30.95 { mark(nil()) -> nil() 70.26/30.95 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.95 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.95 , mark(s(X)) -> s(mark(X)) 70.26/30.95 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.95 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.95 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.95 , a__from(X) -> from(X) 70.26/30.95 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.95 , a__zWadr(XS, nil()) -> nil() 70.26/30.95 , a__zWadr(nil(), YS) -> nil() 70.26/30.95 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.95 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.95 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.95 , a__prefix(X) -> prefix(X) } 70.26/30.95 Weak Trs: 70.26/30.95 { a__app(X1, X2) -> app(X1, X2) 70.26/30.95 , a__app(nil(), YS) -> mark(YS) 70.26/30.95 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.95 , mark(from(X)) -> a__from(mark(X)) } 70.26/30.95 Obligation: 70.26/30.95 innermost runtime complexity 70.26/30.95 Answer: 70.26/30.95 YES(O(1),O(n^2)) 70.26/30.95 70.26/30.95 The weightgap principle applies (using the following nonconstant 70.26/30.95 growth matrix-interpretation) 70.26/30.95 70.26/30.95 The following argument positions are usable: 70.26/30.95 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.95 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.95 70.26/30.95 TcT has computed the following matrix interpretation satisfying 70.26/30.95 not(EDA) and not(IDA(1)). 70.26/30.95 70.26/30.95 [a__app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [nil] = [4] 70.26/30.95 70.26/30.95 [mark](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [cons](x1, x2) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [a__from](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [from](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [s](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [zWadr](x1, x2) = [1] x1 + [1] x2 + [1] 70.26/30.95 70.26/30.95 [a__prefix](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [prefix](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 The order satisfies the following ordering constraints: 70.26/30.95 70.26/30.95 [a__app(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [app(X1, X2)] 70.26/30.95 70.26/30.95 [a__app(nil(), YS)] = [1] YS + [4] 70.26/30.95 > [1] YS + [0] 70.26/30.95 = [mark(YS)] 70.26/30.95 70.26/30.95 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [cons(mark(X), app(XS, YS))] 70.26/30.95 70.26/30.95 [mark(nil())] = [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [mark(cons(X1, X2))] = [1] X1 + [0] 70.26/30.95 >= [1] X1 + [0] 70.26/30.95 = [cons(mark(X1), X2)] 70.26/30.95 70.26/30.95 [mark(app(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.95 = [a__app(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(from(X))] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [a__from(mark(X))] 70.26/30.95 70.26/30.95 [mark(s(X))] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [s(mark(X))] 70.26/30.95 70.26/30.95 [mark(zWadr(X1, X2))] = [1] X1 + [1] X2 + [1] 70.26/30.95 > [1] X1 + [1] X2 + [0] 70.26/30.95 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.95 70.26/30.95 [mark(prefix(X))] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [a__prefix(mark(X))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [cons(mark(X), from(s(X)))] 70.26/30.95 70.26/30.95 [a__from(X)] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [from(X)] 70.26/30.95 70.26/30.95 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 ? [1] X1 + [1] X2 + [1] 70.26/30.95 = [zWadr(X1, X2)] 70.26/30.95 70.26/30.95 [a__zWadr(XS, nil())] = [1] XS + [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(nil(), YS)] = [1] YS + [4] 70.26/30.95 >= [4] 70.26/30.95 = [nil()] 70.26/30.95 70.26/30.95 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [0] 70.26/30.95 >= [1] X + [1] Y + [0] 70.26/30.95 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.95 70.26/30.95 [a__prefix(L)] = [1] L + [0] 70.26/30.95 ? [4] 70.26/30.95 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.95 70.26/30.95 [a__prefix(X)] = [1] X + [0] 70.26/30.95 >= [1] X + [0] 70.26/30.95 = [prefix(X)] 70.26/30.95 70.26/30.95 70.26/30.95 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.95 70.26/30.95 We are left with following problem, upon which TcT provides the 70.26/30.95 certificate YES(O(1),O(n^2)). 70.26/30.95 70.26/30.95 Strict Trs: 70.26/30.95 { mark(nil()) -> nil() 70.26/30.95 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.95 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.95 , mark(s(X)) -> s(mark(X)) 70.26/30.95 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.95 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.95 , a__from(X) -> from(X) 70.26/30.95 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.95 , a__zWadr(XS, nil()) -> nil() 70.26/30.95 , a__zWadr(nil(), YS) -> nil() 70.26/30.95 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.95 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.95 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.95 , a__prefix(X) -> prefix(X) } 70.26/30.95 Weak Trs: 70.26/30.95 { a__app(X1, X2) -> app(X1, X2) 70.26/30.95 , a__app(nil(), YS) -> mark(YS) 70.26/30.95 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.95 , mark(from(X)) -> a__from(mark(X)) 70.26/30.95 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) } 70.26/30.95 Obligation: 70.26/30.95 innermost runtime complexity 70.26/30.95 Answer: 70.26/30.95 YES(O(1),O(n^2)) 70.26/30.95 70.26/30.95 The weightgap principle applies (using the following nonconstant 70.26/30.95 growth matrix-interpretation) 70.26/30.95 70.26/30.95 The following argument positions are usable: 70.26/30.95 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.95 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.95 70.26/30.95 TcT has computed the following matrix interpretation satisfying 70.26/30.95 not(EDA) and not(IDA(1)). 70.26/30.95 70.26/30.95 [a__app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [nil] = [0] 70.26/30.95 70.26/30.95 [mark](x1) = [0] 70.26/30.95 70.26/30.95 [cons](x1, x2) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [a__from](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [from](x1) = [1] x1 + [7] 70.26/30.95 70.26/30.95 [s](x1) = [1] x1 + [0] 70.26/30.95 70.26/30.95 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.95 70.26/30.95 [zWadr](x1, x2) = [1] x1 + [1] x2 + [7] 70.26/30.95 70.26/30.95 [a__prefix](x1) = [1] x1 + [4] 70.26/30.95 70.26/30.95 [prefix](x1) = [1] x1 + [3] 70.26/30.95 70.26/30.95 The order satisfies the following ordering constraints: 70.26/30.95 70.26/30.95 [a__app(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.95 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [app(X1, X2)] 70.26/30.96 70.26/30.96 [a__app(nil(), YS)] = [1] YS + [0] 70.26/30.96 >= [0] 70.26/30.96 = [mark(YS)] 70.26/30.96 70.26/30.96 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [0] 70.26/30.96 >= [0] 70.26/30.96 = [cons(mark(X), app(XS, YS))] 70.26/30.96 70.26/30.96 [mark(nil())] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [mark(cons(X1, X2))] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [cons(mark(X1), X2)] 70.26/30.96 70.26/30.96 [mark(app(X1, X2))] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [a__app(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(from(X))] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [a__from(mark(X))] 70.26/30.96 70.26/30.96 [mark(s(X))] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [s(mark(X))] 70.26/30.96 70.26/30.96 [mark(zWadr(X1, X2))] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(prefix(X))] = [0] 70.26/30.96 ? [4] 70.26/30.96 = [a__prefix(mark(X))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [0] 70.26/30.96 >= [0] 70.26/30.96 = [cons(mark(X), from(s(X)))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [0] 70.26/30.96 ? [1] X + [7] 70.26/30.96 = [from(X)] 70.26/30.96 70.26/30.96 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.96 ? [1] X1 + [1] X2 + [7] 70.26/30.96 = [zWadr(X1, X2)] 70.26/30.96 70.26/30.96 [a__zWadr(XS, nil())] = [1] XS + [0] 70.26/30.96 >= [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(nil(), YS)] = [1] YS + [0] 70.26/30.96 >= [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [0] 70.26/30.96 >= [0] 70.26/30.96 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.96 70.26/30.96 [a__prefix(L)] = [1] L + [4] 70.26/30.96 > [0] 70.26/30.96 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.96 70.26/30.96 [a__prefix(X)] = [1] X + [4] 70.26/30.96 > [1] X + [3] 70.26/30.96 = [prefix(X)] 70.26/30.96 70.26/30.96 70.26/30.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.96 70.26/30.96 We are left with following problem, upon which TcT provides the 70.26/30.96 certificate YES(O(1),O(n^2)). 70.26/30.96 70.26/30.96 Strict Trs: 70.26/30.96 { mark(nil()) -> nil() 70.26/30.96 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.96 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.96 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.96 , a__from(X) -> from(X) 70.26/30.96 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.96 , a__zWadr(XS, nil()) -> nil() 70.26/30.96 , a__zWadr(nil(), YS) -> nil() 70.26/30.96 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.96 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) } 70.26/30.96 Weak Trs: 70.26/30.96 { a__app(X1, X2) -> app(X1, X2) 70.26/30.96 , a__app(nil(), YS) -> mark(YS) 70.26/30.96 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.96 , mark(from(X)) -> a__from(mark(X)) 70.26/30.96 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.96 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.96 , a__prefix(X) -> prefix(X) } 70.26/30.96 Obligation: 70.26/30.96 innermost runtime complexity 70.26/30.96 Answer: 70.26/30.96 YES(O(1),O(n^2)) 70.26/30.96 70.26/30.96 The weightgap principle applies (using the following nonconstant 70.26/30.96 growth matrix-interpretation) 70.26/30.96 70.26/30.96 The following argument positions are usable: 70.26/30.96 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.96 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.96 70.26/30.96 TcT has computed the following matrix interpretation satisfying 70.26/30.96 not(EDA) and not(IDA(1)). 70.26/30.96 70.26/30.96 [a__app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [nil] = [4] 70.26/30.96 70.26/30.96 [mark](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [cons](x1, x2) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [a__from](x1) = [1] x1 + [1] 70.26/30.96 70.26/30.96 [from](x1) = [1] x1 + [4] 70.26/30.96 70.26/30.96 [s](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [zWadr](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [a__prefix](x1) = [1] x1 + [4] 70.26/30.96 70.26/30.96 [prefix](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 The order satisfies the following ordering constraints: 70.26/30.96 70.26/30.96 [a__app(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [app(X1, X2)] 70.26/30.96 70.26/30.96 [a__app(nil(), YS)] = [1] YS + [4] 70.26/30.96 > [1] YS + [0] 70.26/30.96 = [mark(YS)] 70.26/30.96 70.26/30.96 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [cons(mark(X), app(XS, YS))] 70.26/30.96 70.26/30.96 [mark(nil())] = [4] 70.26/30.96 >= [4] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [mark(cons(X1, X2))] = [1] X1 + [0] 70.26/30.96 >= [1] X1 + [0] 70.26/30.96 = [cons(mark(X1), X2)] 70.26/30.96 70.26/30.96 [mark(app(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [a__app(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(from(X))] = [1] X + [4] 70.26/30.96 > [1] X + [1] 70.26/30.96 = [a__from(mark(X))] 70.26/30.96 70.26/30.96 [mark(s(X))] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [s(mark(X))] 70.26/30.96 70.26/30.96 [mark(zWadr(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(prefix(X))] = [1] X + [0] 70.26/30.96 ? [1] X + [4] 70.26/30.96 = [a__prefix(mark(X))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [1] 70.26/30.96 > [1] X + [0] 70.26/30.96 = [cons(mark(X), from(s(X)))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [1] 70.26/30.96 ? [1] X + [4] 70.26/30.96 = [from(X)] 70.26/30.96 70.26/30.96 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [zWadr(X1, X2)] 70.26/30.96 70.26/30.96 [a__zWadr(XS, nil())] = [1] XS + [4] 70.26/30.96 >= [4] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(nil(), YS)] = [1] YS + [4] 70.26/30.96 >= [4] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [0] 70.26/30.96 >= [1] X + [1] Y + [0] 70.26/30.96 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.96 70.26/30.96 [a__prefix(L)] = [1] L + [4] 70.26/30.96 >= [4] 70.26/30.96 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.96 70.26/30.96 [a__prefix(X)] = [1] X + [4] 70.26/30.96 > [1] X + [0] 70.26/30.96 = [prefix(X)] 70.26/30.96 70.26/30.96 70.26/30.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.96 70.26/30.96 We are left with following problem, upon which TcT provides the 70.26/30.96 certificate YES(O(1),O(n^2)). 70.26/30.96 70.26/30.96 Strict Trs: 70.26/30.96 { mark(nil()) -> nil() 70.26/30.96 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.96 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.96 , a__from(X) -> from(X) 70.26/30.96 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.96 , a__zWadr(XS, nil()) -> nil() 70.26/30.96 , a__zWadr(nil(), YS) -> nil() 70.26/30.96 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.96 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) } 70.26/30.96 Weak Trs: 70.26/30.96 { a__app(X1, X2) -> app(X1, X2) 70.26/30.96 , a__app(nil(), YS) -> mark(YS) 70.26/30.96 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.96 , mark(from(X)) -> a__from(mark(X)) 70.26/30.96 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.96 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.96 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.96 , a__prefix(X) -> prefix(X) } 70.26/30.96 Obligation: 70.26/30.96 innermost runtime complexity 70.26/30.96 Answer: 70.26/30.96 YES(O(1),O(n^2)) 70.26/30.96 70.26/30.96 The weightgap principle applies (using the following nonconstant 70.26/30.96 growth matrix-interpretation) 70.26/30.96 70.26/30.96 The following argument positions are usable: 70.26/30.96 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.96 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.96 70.26/30.96 TcT has computed the following matrix interpretation satisfying 70.26/30.96 not(EDA) and not(IDA(1)). 70.26/30.96 70.26/30.96 [a__app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [nil] = [0] 70.26/30.96 70.26/30.96 [mark](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [cons](x1, x2) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [a__from](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [from](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [s](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [1] 70.26/30.96 70.26/30.96 [zWadr](x1, x2) = [1] x1 + [1] x2 + [1] 70.26/30.96 70.26/30.96 [a__prefix](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [prefix](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 The order satisfies the following ordering constraints: 70.26/30.96 70.26/30.96 [a__app(X1, X2)] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [app(X1, X2)] 70.26/30.96 70.26/30.96 [a__app(nil(), YS)] = [1] YS + [0] 70.26/30.96 >= [1] YS + [0] 70.26/30.96 = [mark(YS)] 70.26/30.96 70.26/30.96 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [cons(mark(X), app(XS, YS))] 70.26/30.96 70.26/30.96 [mark(nil())] = [0] 70.26/30.96 >= [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [mark(cons(X1, X2))] = [1] X1 + [0] 70.26/30.96 >= [1] X1 + [0] 70.26/30.96 = [cons(mark(X1), X2)] 70.26/30.96 70.26/30.96 [mark(app(X1, X2))] = [1] X1 + [1] X2 + [0] 70.26/30.96 >= [1] X1 + [1] X2 + [0] 70.26/30.96 = [a__app(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(from(X))] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [a__from(mark(X))] 70.26/30.96 70.26/30.96 [mark(s(X))] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [s(mark(X))] 70.26/30.96 70.26/30.96 [mark(zWadr(X1, X2))] = [1] X1 + [1] X2 + [1] 70.26/30.96 >= [1] X1 + [1] X2 + [1] 70.26/30.96 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(prefix(X))] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [a__prefix(mark(X))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [cons(mark(X), from(s(X)))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [from(X)] 70.26/30.96 70.26/30.96 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [1] 70.26/30.96 >= [1] X1 + [1] X2 + [1] 70.26/30.96 = [zWadr(X1, X2)] 70.26/30.96 70.26/30.96 [a__zWadr(XS, nil())] = [1] XS + [1] 70.26/30.96 > [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(nil(), YS)] = [1] YS + [1] 70.26/30.96 > [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [1] 70.26/30.96 > [1] X + [1] Y + [0] 70.26/30.96 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.96 70.26/30.96 [a__prefix(L)] = [1] L + [0] 70.26/30.96 >= [0] 70.26/30.96 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.96 70.26/30.96 [a__prefix(X)] = [1] X + [0] 70.26/30.96 >= [1] X + [0] 70.26/30.96 = [prefix(X)] 70.26/30.96 70.26/30.96 70.26/30.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.96 70.26/30.96 We are left with following problem, upon which TcT provides the 70.26/30.96 certificate YES(O(1),O(n^2)). 70.26/30.96 70.26/30.96 Strict Trs: 70.26/30.96 { mark(nil()) -> nil() 70.26/30.96 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.96 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.96 , a__from(X) -> from(X) 70.26/30.96 , a__zWadr(X1, X2) -> zWadr(X1, X2) } 70.26/30.96 Weak Trs: 70.26/30.96 { a__app(X1, X2) -> app(X1, X2) 70.26/30.96 , a__app(nil(), YS) -> mark(YS) 70.26/30.96 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.96 , mark(from(X)) -> a__from(mark(X)) 70.26/30.96 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.96 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.96 , a__zWadr(XS, nil()) -> nil() 70.26/30.96 , a__zWadr(nil(), YS) -> nil() 70.26/30.96 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.96 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.96 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.96 , a__prefix(X) -> prefix(X) } 70.26/30.96 Obligation: 70.26/30.96 innermost runtime complexity 70.26/30.96 Answer: 70.26/30.96 YES(O(1),O(n^2)) 70.26/30.96 70.26/30.96 The weightgap principle applies (using the following nonconstant 70.26/30.96 growth matrix-interpretation) 70.26/30.96 70.26/30.96 The following argument positions are usable: 70.26/30.96 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.96 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.96 70.26/30.96 TcT has computed the following matrix interpretation satisfying 70.26/30.96 not(EDA) and not(IDA(1)). 70.26/30.96 70.26/30.96 [a__app](x1, x2) = [1] x1 + [1] x2 + [2] 70.26/30.96 70.26/30.96 [nil] = [0] 70.26/30.96 70.26/30.96 [mark](x1) = [1] x1 + [1] 70.26/30.96 70.26/30.96 [cons](x1, x2) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [app](x1, x2) = [1] x1 + [1] x2 + [0] 70.26/30.96 70.26/30.96 [a__from](x1) = [1] x1 + [1] 70.26/30.96 70.26/30.96 [from](x1) = [1] x1 + [1] 70.26/30.96 70.26/30.96 [s](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 [a__zWadr](x1, x2) = [1] x1 + [1] x2 + [4] 70.26/30.96 70.26/30.96 [zWadr](x1, x2) = [1] x1 + [1] x2 + [6] 70.26/30.96 70.26/30.96 [a__prefix](x1) = [1] x1 + [4] 70.26/30.96 70.26/30.96 [prefix](x1) = [1] x1 + [0] 70.26/30.96 70.26/30.96 The order satisfies the following ordering constraints: 70.26/30.96 70.26/30.96 [a__app(X1, X2)] = [1] X1 + [1] X2 + [2] 70.26/30.96 > [1] X1 + [1] X2 + [0] 70.26/30.96 = [app(X1, X2)] 70.26/30.96 70.26/30.96 [a__app(nil(), YS)] = [1] YS + [2] 70.26/30.96 > [1] YS + [1] 70.26/30.96 = [mark(YS)] 70.26/30.96 70.26/30.96 [a__app(cons(X, XS), YS)] = [1] YS + [1] X + [2] 70.26/30.96 > [1] X + [1] 70.26/30.96 = [cons(mark(X), app(XS, YS))] 70.26/30.96 70.26/30.96 [mark(nil())] = [1] 70.26/30.96 > [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [mark(cons(X1, X2))] = [1] X1 + [1] 70.26/30.96 >= [1] X1 + [1] 70.26/30.96 = [cons(mark(X1), X2)] 70.26/30.96 70.26/30.96 [mark(app(X1, X2))] = [1] X1 + [1] X2 + [1] 70.26/30.96 ? [1] X1 + [1] X2 + [4] 70.26/30.96 = [a__app(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(from(X))] = [1] X + [2] 70.26/30.96 >= [1] X + [2] 70.26/30.96 = [a__from(mark(X))] 70.26/30.96 70.26/30.96 [mark(s(X))] = [1] X + [1] 70.26/30.96 >= [1] X + [1] 70.26/30.96 = [s(mark(X))] 70.26/30.96 70.26/30.96 [mark(zWadr(X1, X2))] = [1] X1 + [1] X2 + [7] 70.26/30.96 > [1] X1 + [1] X2 + [6] 70.26/30.96 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(prefix(X))] = [1] X + [1] 70.26/30.96 ? [1] X + [5] 70.26/30.96 = [a__prefix(mark(X))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [1] 70.26/30.96 >= [1] X + [1] 70.26/30.96 = [cons(mark(X), from(s(X)))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1] X + [1] 70.26/30.96 >= [1] X + [1] 70.26/30.96 = [from(X)] 70.26/30.96 70.26/30.96 [a__zWadr(X1, X2)] = [1] X1 + [1] X2 + [4] 70.26/30.96 ? [1] X1 + [1] X2 + [6] 70.26/30.96 = [zWadr(X1, X2)] 70.26/30.96 70.26/30.96 [a__zWadr(XS, nil())] = [1] XS + [4] 70.26/30.96 > [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(nil(), YS)] = [1] YS + [4] 70.26/30.96 > [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1] X + [1] Y + [4] 70.26/30.96 >= [1] X + [1] Y + [4] 70.26/30.96 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.96 70.26/30.96 [a__prefix(L)] = [1] L + [4] 70.26/30.96 > [0] 70.26/30.96 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.96 70.26/30.96 [a__prefix(X)] = [1] X + [4] 70.26/30.96 > [1] X + [0] 70.26/30.96 = [prefix(X)] 70.26/30.96 70.26/30.96 70.26/30.96 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.26/30.96 70.26/30.96 We are left with following problem, upon which TcT provides the 70.26/30.96 certificate YES(O(1),O(n^2)). 70.26/30.96 70.26/30.96 Strict Trs: 70.26/30.96 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.96 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.96 , a__from(X) -> from(X) 70.26/30.96 , a__zWadr(X1, X2) -> zWadr(X1, X2) } 70.26/30.96 Weak Trs: 70.26/30.96 { a__app(X1, X2) -> app(X1, X2) 70.26/30.96 , a__app(nil(), YS) -> mark(YS) 70.26/30.96 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.96 , mark(nil()) -> nil() 70.26/30.96 , mark(from(X)) -> a__from(mark(X)) 70.26/30.96 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.96 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.96 , a__zWadr(XS, nil()) -> nil() 70.26/30.96 , a__zWadr(nil(), YS) -> nil() 70.26/30.96 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.96 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.96 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.96 , a__prefix(X) -> prefix(X) } 70.26/30.96 Obligation: 70.26/30.96 innermost runtime complexity 70.26/30.96 Answer: 70.26/30.96 YES(O(1),O(n^2)) 70.26/30.96 70.26/30.96 We use the processor 'matrix interpretation of dimension 2' to 70.26/30.96 orient following rules strictly. 70.26/30.96 70.26/30.96 Trs: 70.26/30.96 { mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) } 70.26/30.96 70.26/30.96 The induced complexity on above rules (modulo remaining rules) is 70.26/30.96 YES(?,O(n^2)) . These rules are moved into the corresponding weak 70.26/30.96 component(s). 70.26/30.96 70.26/30.96 Sub-proof: 70.26/30.96 ---------- 70.26/30.96 The following argument positions are usable: 70.26/30.96 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.96 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.96 70.26/30.96 TcT has computed the following constructor-based matrix 70.26/30.96 interpretation satisfying not(EDA). 70.26/30.96 70.26/30.96 [a__app](x1, x2) = [1 1] x1 + [1 4] x2 + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 70.26/30.96 [nil] = [0] 70.26/30.96 [0] 70.26/30.96 70.26/30.96 [mark](x1) = [1 1] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [cons](x1, x2) = [1 0] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [app](x1, x2) = [1 1] x1 + [1 4] x2 + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 70.26/30.96 [a__from](x1) = [1 2] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [from](x1) = [1 2] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [s](x1) = [1 0] x1 + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 70.26/30.96 [a__zWadr](x1, x2) = [1 5] x1 + [1 4] x2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 70.26/30.96 [zWadr](x1, x2) = [1 5] x1 + [1 4] x2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 70.26/30.96 [a__prefix](x1) = [1 0] x1 + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 70.26/30.96 [prefix](x1) = [1 0] x1 + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 70.26/30.96 The order satisfies the following ordering constraints: 70.26/30.96 70.26/30.96 [a__app(X1, X2)] = [1 1] X1 + [1 4] X2 + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 >= [1 1] X1 + [1 4] X2 + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 = [app(X1, X2)] 70.26/30.96 70.26/30.96 [a__app(nil(), YS)] = [1 4] YS + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 >= [1 1] YS + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [mark(YS)] 70.26/30.96 70.26/30.96 [a__app(cons(X, XS), YS)] = [1 4] YS + [1 1] X + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 >= [1 1] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [cons(mark(X), app(XS, YS))] 70.26/30.96 70.26/30.96 [mark(nil())] = [0] 70.26/30.96 [0] 70.26/30.96 >= [0] 70.26/30.96 [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [mark(cons(X1, X2))] = [1 1] X1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 >= [1 1] X1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [cons(mark(X1), X2)] 70.26/30.96 70.26/30.96 [mark(app(X1, X2))] = [1 2] X1 + [1 5] X2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 > [1 2] X1 + [1 5] X2 + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 = [a__app(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(from(X))] = [1 3] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 >= [1 3] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [a__from(mark(X))] 70.26/30.96 70.26/30.96 [mark(s(X))] = [1 1] X + [4] 70.26/30.96 [0 1] [4] 70.26/30.96 > [1 1] X + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 = [s(mark(X))] 70.26/30.96 70.26/30.96 [mark(zWadr(X1, X2))] = [1 6] X1 + [1 5] X2 + [8] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 > [1 6] X1 + [1 5] X2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.96 70.26/30.96 [mark(prefix(X))] = [1 1] X + [4] 70.26/30.96 [0 1] [4] 70.26/30.96 > [1 1] X + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 = [a__prefix(mark(X))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1 2] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 >= [1 1] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [cons(mark(X), from(s(X)))] 70.26/30.96 70.26/30.96 [a__from(X)] = [1 2] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 >= [1 2] X + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 = [from(X)] 70.26/30.96 70.26/30.96 [a__zWadr(X1, X2)] = [1 5] X1 + [1 4] X2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 >= [1 5] X1 + [1 4] X2 + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 = [zWadr(X1, X2)] 70.26/30.96 70.26/30.96 [a__zWadr(XS, nil())] = [1 5] XS + [4] 70.26/30.96 [0 1] [4] 70.26/30.96 > [0] 70.26/30.96 [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(nil(), YS)] = [1 4] YS + [4] 70.26/30.96 [0 1] [4] 70.26/30.96 > [0] 70.26/30.96 [0] 70.26/30.96 = [nil()] 70.26/30.96 70.26/30.96 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1 5] X + [1 4] Y + [4] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 > [1 5] X + [1 2] Y + [0] 70.26/30.96 [0 1] [0 1] [4] 70.26/30.96 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.96 70.26/30.96 [a__prefix(L)] = [1 0] L + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 >= [0] 70.26/30.96 [0] 70.26/30.96 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.96 70.26/30.96 [a__prefix(X)] = [1 0] X + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 >= [1 0] X + [0] 70.26/30.96 [0 1] [4] 70.26/30.96 = [prefix(X)] 70.26/30.96 70.26/30.96 70.26/30.96 We return to the main proof. 70.26/30.96 70.26/30.96 We are left with following problem, upon which TcT provides the 70.26/30.96 certificate YES(O(1),O(n^2)). 70.26/30.96 70.26/30.96 Strict Trs: 70.26/30.96 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.96 , a__from(X) -> from(X) 70.26/30.96 , a__zWadr(X1, X2) -> zWadr(X1, X2) } 70.26/30.96 Weak Trs: 70.26/30.96 { a__app(X1, X2) -> app(X1, X2) 70.26/30.96 , a__app(nil(), YS) -> mark(YS) 70.26/30.96 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.96 , mark(nil()) -> nil() 70.26/30.96 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.96 , mark(from(X)) -> a__from(mark(X)) 70.26/30.96 , mark(s(X)) -> s(mark(X)) 70.26/30.96 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.96 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.96 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.96 , a__zWadr(XS, nil()) -> nil() 70.26/30.96 , a__zWadr(nil(), YS) -> nil() 70.26/30.96 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.96 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.96 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.96 , a__prefix(X) -> prefix(X) } 70.26/30.96 Obligation: 70.26/30.96 innermost runtime complexity 70.26/30.96 Answer: 70.26/30.96 YES(O(1),O(n^2)) 70.26/30.96 70.26/30.96 We use the processor 'matrix interpretation of dimension 2' to 70.26/30.96 orient following rules strictly. 70.26/30.96 70.26/30.96 Trs: { a__zWadr(X1, X2) -> zWadr(X1, X2) } 70.26/30.96 70.26/30.96 The induced complexity on above rules (modulo remaining rules) is 70.26/30.96 YES(?,O(n^2)) . These rules are moved into the corresponding weak 70.26/30.96 component(s). 70.26/30.96 70.26/30.96 Sub-proof: 70.26/30.96 ---------- 70.26/30.96 The following argument positions are usable: 70.26/30.96 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.96 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.96 70.26/30.96 TcT has computed the following constructor-based matrix 70.26/30.96 interpretation satisfying not(EDA). 70.26/30.96 70.26/30.96 [a__app](x1, x2) = [1 2] x1 + [1 4] x2 + [0] 70.26/30.96 [0 1] [0 1] [0] 70.26/30.96 70.26/30.96 [nil] = [0] 70.26/30.96 [0] 70.26/30.96 70.26/30.96 [mark](x1) = [1 2] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [cons](x1, x2) = [1 0] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [app](x1, x2) = [1 2] x1 + [1 4] x2 + [0] 70.26/30.96 [0 1] [0 1] [0] 70.26/30.96 70.26/30.96 [a__from](x1) = [1 2] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [from](x1) = [1 2] x1 + [0] 70.26/30.96 [0 1] [0] 70.26/30.96 70.26/30.96 [s](x1) = [1 0] x1 + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 70.26/30.97 [a__zWadr](x1, x2) = [1 6] x1 + [1 4] x2 + [1] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 70.26/30.97 [zWadr](x1, x2) = [1 6] x1 + [1 4] x2 + [0] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 70.26/30.97 [a__prefix](x1) = [1 1] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 [prefix](x1) = [1 1] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 The order satisfies the following ordering constraints: 70.26/30.97 70.26/30.97 [a__app(X1, X2)] = [1 2] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 2] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [app(X1, X2)] 70.26/30.97 70.26/30.97 [a__app(nil(), YS)] = [1 4] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 2] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [mark(YS)] 70.26/30.97 70.26/30.97 [a__app(cons(X, XS), YS)] = [1 4] YS + [1 2] X + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 2] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X), app(XS, YS))] 70.26/30.97 70.26/30.97 [mark(nil())] = [0] 70.26/30.97 [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [mark(cons(X1, X2))] = [1 2] X1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 2] X1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X1), X2)] 70.26/30.97 70.26/30.97 [mark(app(X1, X2))] = [1 4] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 4] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [a__app(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(from(X))] = [1 4] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 4] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [a__from(mark(X))] 70.26/30.97 70.26/30.97 [mark(s(X))] = [1 2] X + [8] 70.26/30.97 [0 1] [4] 70.26/30.97 > [1 2] X + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 = [s(mark(X))] 70.26/30.97 70.26/30.97 [mark(zWadr(X1, X2))] = [1 8] X1 + [1 6] X2 + [8] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 > [1 8] X1 + [1 6] X2 + [1] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(prefix(X))] = [1 3] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 3] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [a__prefix(mark(X))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 2] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 2] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X), from(s(X)))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 2] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 2] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [from(X)] 70.26/30.97 70.26/30.97 [a__zWadr(X1, X2)] = [1 6] X1 + [1 4] X2 + [1] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 > [1 6] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 = [zWadr(X1, X2)] 70.26/30.97 70.26/30.97 [a__zWadr(XS, nil())] = [1 6] XS + [1] 70.26/30.97 [0 1] [4] 70.26/30.97 > [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(nil(), YS)] = [1 4] YS + [1] 70.26/30.97 [0 1] [4] 70.26/30.97 > [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1 6] X + [1 4] Y + [1] 70.26/30.97 [0 1] [0 1] [4] 70.26/30.97 > [1 6] X + [1 4] Y + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.97 70.26/30.97 [a__prefix(L)] = [1 1] L + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.97 70.26/30.97 [a__prefix(X)] = [1 1] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 1] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [prefix(X)] 70.26/30.97 70.26/30.97 70.26/30.97 We return to the main proof. 70.26/30.97 70.26/30.97 We are left with following problem, upon which TcT provides the 70.26/30.97 certificate YES(O(1),O(n^2)). 70.26/30.97 70.26/30.97 Strict Trs: 70.26/30.97 { mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.97 , a__from(X) -> from(X) } 70.26/30.97 Weak Trs: 70.26/30.97 { a__app(X1, X2) -> app(X1, X2) 70.26/30.97 , a__app(nil(), YS) -> mark(YS) 70.26/30.97 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.97 , mark(nil()) -> nil() 70.26/30.97 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.97 , mark(from(X)) -> a__from(mark(X)) 70.26/30.97 , mark(s(X)) -> s(mark(X)) 70.26/30.97 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.97 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.97 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.97 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.97 , a__zWadr(XS, nil()) -> nil() 70.26/30.97 , a__zWadr(nil(), YS) -> nil() 70.26/30.97 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.97 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.97 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.97 , a__prefix(X) -> prefix(X) } 70.26/30.97 Obligation: 70.26/30.97 innermost runtime complexity 70.26/30.97 Answer: 70.26/30.97 YES(O(1),O(n^2)) 70.26/30.97 70.26/30.97 We use the processor 'matrix interpretation of dimension 2' to 70.26/30.97 orient following rules strictly. 70.26/30.97 70.26/30.97 Trs: { a__from(X) -> from(X) } 70.26/30.97 70.26/30.97 The induced complexity on above rules (modulo remaining rules) is 70.26/30.97 YES(?,O(n^2)) . These rules are moved into the corresponding weak 70.26/30.97 component(s). 70.26/30.97 70.26/30.97 Sub-proof: 70.26/30.97 ---------- 70.26/30.97 The following argument positions are usable: 70.26/30.97 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.97 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.97 70.26/30.97 TcT has computed the following constructor-based matrix 70.26/30.97 interpretation satisfying not(EDA). 70.26/30.97 70.26/30.97 [a__app](x1, x2) = [1 4] x1 + [1 4] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [nil] = [0] 70.26/30.97 [0] 70.26/30.97 70.26/30.97 [mark](x1) = [1 1] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 [cons](x1, x2) = [1 2] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 [app](x1, x2) = [1 4] x1 + [1 4] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [a__from](x1) = [1 4] x1 + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 70.26/30.97 [from](x1) = [1 4] x1 + [2] 70.26/30.97 [0 1] [2] 70.26/30.97 70.26/30.97 [s](x1) = [1 0] x1 + [2] 70.26/30.97 [0 1] [6] 70.26/30.97 70.26/30.97 [a__zWadr](x1, x2) = [1 7] x1 + [1 7] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [zWadr](x1, x2) = [1 7] x1 + [1 7] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [a__prefix](x1) = [1 0] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 [prefix](x1) = [1 0] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 The order satisfies the following ordering constraints: 70.26/30.97 70.26/30.97 [a__app(X1, X2)] = [1 4] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 4] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [app(X1, X2)] 70.26/30.97 70.26/30.97 [a__app(nil(), YS)] = [1 4] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 1] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [mark(YS)] 70.26/30.97 70.26/30.97 [a__app(cons(X, XS), YS)] = [1 4] YS + [1 6] X + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 3] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X), app(XS, YS))] 70.26/30.97 70.26/30.97 [mark(nil())] = [0] 70.26/30.97 [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [mark(cons(X1, X2))] = [1 3] X1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 3] X1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X1), X2)] 70.26/30.97 70.26/30.97 [mark(app(X1, X2))] = [1 5] X1 + [1 5] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 5] X1 + [1 5] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [a__app(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(from(X))] = [1 5] X + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 >= [1 5] X + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 = [a__from(mark(X))] 70.26/30.97 70.26/30.97 [mark(s(X))] = [1 1] X + [8] 70.26/30.97 [0 1] [6] 70.26/30.97 > [1 1] X + [2] 70.26/30.97 [0 1] [6] 70.26/30.97 = [s(mark(X))] 70.26/30.97 70.26/30.97 [mark(zWadr(X1, X2))] = [1 8] X1 + [1 8] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 8] X1 + [1 8] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(prefix(X))] = [1 1] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 1] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [a__prefix(mark(X))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 4] X + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 > [1 3] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [cons(mark(X), from(s(X)))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 4] X + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 > [1 4] X + [2] 70.26/30.97 [0 1] [2] 70.26/30.97 = [from(X)] 70.26/30.97 70.26/30.97 [a__zWadr(X1, X2)] = [1 7] X1 + [1 7] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 7] X1 + [1 7] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [zWadr(X1, X2)] 70.26/30.97 70.26/30.97 [a__zWadr(XS, nil())] = [1 7] XS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(nil(), YS)] = [1 7] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1 9] X + [1 9] Y + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 9] X + [1 7] Y + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.97 70.26/30.97 [a__prefix(L)] = [1 0] L + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.97 70.26/30.97 [a__prefix(X)] = [1 0] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 0] X + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [prefix(X)] 70.26/30.97 70.26/30.97 70.26/30.97 We return to the main proof. 70.26/30.97 70.26/30.97 We are left with following problem, upon which TcT provides the 70.26/30.97 certificate YES(O(1),O(n^2)). 70.26/30.97 70.26/30.97 Strict Trs: { mark(cons(X1, X2)) -> cons(mark(X1), X2) } 70.26/30.97 Weak Trs: 70.26/30.97 { a__app(X1, X2) -> app(X1, X2) 70.26/30.97 , a__app(nil(), YS) -> mark(YS) 70.26/30.97 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.97 , mark(nil()) -> nil() 70.26/30.97 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.97 , mark(from(X)) -> a__from(mark(X)) 70.26/30.97 , mark(s(X)) -> s(mark(X)) 70.26/30.97 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.97 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.97 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.97 , a__from(X) -> from(X) 70.26/30.97 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.97 , a__zWadr(XS, nil()) -> nil() 70.26/30.97 , a__zWadr(nil(), YS) -> nil() 70.26/30.97 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.97 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.97 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.97 , a__prefix(X) -> prefix(X) } 70.26/30.97 Obligation: 70.26/30.97 innermost runtime complexity 70.26/30.97 Answer: 70.26/30.97 YES(O(1),O(n^2)) 70.26/30.97 70.26/30.97 We use the processor 'matrix interpretation of dimension 2' to 70.26/30.97 orient following rules strictly. 70.26/30.97 70.26/30.97 Trs: { mark(cons(X1, X2)) -> cons(mark(X1), X2) } 70.26/30.97 70.26/30.97 The induced complexity on above rules (modulo remaining rules) is 70.26/30.97 YES(?,O(n^2)) . These rules are moved into the corresponding weak 70.26/30.97 component(s). 70.26/30.97 70.26/30.97 Sub-proof: 70.26/30.97 ---------- 70.26/30.97 The following argument positions are usable: 70.26/30.97 Uargs(a__app) = {1, 2}, Uargs(cons) = {1}, Uargs(a__from) = {1}, 70.26/30.97 Uargs(s) = {1}, Uargs(a__zWadr) = {1, 2}, Uargs(a__prefix) = {1} 70.26/30.97 70.26/30.97 TcT has computed the following constructor-based matrix 70.26/30.97 interpretation satisfying not(EDA). 70.26/30.97 70.26/30.97 [a__app](x1, x2) = [1 2] x1 + [1 4] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [nil] = [0] 70.26/30.97 [0] 70.26/30.97 70.26/30.97 [mark](x1) = [1 2] x1 + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 70.26/30.97 [cons](x1, x2) = [1 0] x1 + [0] 70.26/30.97 [0 1] [1] 70.26/30.97 70.26/30.97 [app](x1, x2) = [1 2] x1 + [1 4] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [a__from](x1) = [1 2] x1 + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 70.26/30.97 [from](x1) = [1 2] x1 + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 70.26/30.97 [s](x1) = [1 0] x1 + [2] 70.26/30.97 [0 1] [1] 70.26/30.97 70.26/30.97 [a__zWadr](x1, x2) = [1 6] x1 + [1 6] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [zWadr](x1, x2) = [1 6] x1 + [1 6] x2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 70.26/30.97 [a__prefix](x1) = [1 0] x1 + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 70.26/30.97 [prefix](x1) = [1 0] x1 + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 70.26/30.97 The order satisfies the following ordering constraints: 70.26/30.97 70.26/30.97 [a__app(X1, X2)] = [1 2] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 2] X1 + [1 4] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [app(X1, X2)] 70.26/30.97 70.26/30.97 [a__app(nil(), YS)] = [1 4] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [1 2] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 = [mark(YS)] 70.26/30.97 70.26/30.97 [a__app(cons(X, XS), YS)] = [1 4] YS + [1 2] X + [2] 70.26/30.97 [0 1] [0 1] [1] 70.26/30.97 > [1 2] X + [0] 70.26/30.97 [0 1] [1] 70.26/30.97 = [cons(mark(X), app(XS, YS))] 70.26/30.97 70.26/30.97 [mark(nil())] = [0] 70.26/30.97 [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [mark(cons(X1, X2))] = [1 2] X1 + [2] 70.26/30.97 [0 1] [1] 70.26/30.97 > [1 2] X1 + [0] 70.26/30.97 [0 1] [1] 70.26/30.97 = [cons(mark(X1), X2)] 70.26/30.97 70.26/30.97 [mark(app(X1, X2))] = [1 4] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 4] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [a__app(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(from(X))] = [1 4] X + [4] 70.26/30.97 [0 1] [2] 70.26/30.97 > [1 4] X + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 = [a__from(mark(X))] 70.26/30.97 70.26/30.97 [mark(s(X))] = [1 2] X + [4] 70.26/30.97 [0 1] [1] 70.26/30.97 > [1 2] X + [2] 70.26/30.97 [0 1] [1] 70.26/30.97 = [s(mark(X))] 70.26/30.97 70.26/30.97 [mark(zWadr(X1, X2))] = [1 8] X1 + [1 8] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 8] X1 + [1 8] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [a__zWadr(mark(X1), mark(X2))] 70.26/30.97 70.26/30.97 [mark(prefix(X))] = [1 2] X + [8] 70.26/30.97 [0 1] [4] 70.26/30.97 > [1 2] X + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 = [a__prefix(mark(X))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 2] X + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 >= [1 2] X + [0] 70.26/30.97 [0 1] [1] 70.26/30.97 = [cons(mark(X), from(s(X)))] 70.26/30.97 70.26/30.97 [a__from(X)] = [1 2] X + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 >= [1 2] X + [0] 70.26/30.97 [0 1] [2] 70.26/30.97 = [from(X)] 70.26/30.97 70.26/30.97 [a__zWadr(X1, X2)] = [1 6] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 >= [1 6] X1 + [1 6] X2 + [0] 70.26/30.97 [0 1] [0 1] [0] 70.26/30.97 = [zWadr(X1, X2)] 70.26/30.97 70.26/30.97 [a__zWadr(XS, nil())] = [1 6] XS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(nil(), YS)] = [1 6] YS + [0] 70.26/30.97 [0 1] [0] 70.26/30.97 >= [0] 70.26/30.97 [0] 70.26/30.97 = [nil()] 70.26/30.97 70.26/30.97 [a__zWadr(cons(X, XS), cons(Y, YS))] = [1 6] X + [1 6] Y + [12] 70.26/30.97 [0 1] [0 1] [2] 70.26/30.97 > [1 6] X + [1 4] Y + [4] 70.26/30.97 [0 1] [0 1] [2] 70.26/30.97 = [cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS))] 70.26/30.97 70.26/30.97 [a__prefix(L)] = [1 0] L + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 >= [0] 70.26/30.97 [1] 70.26/30.97 = [cons(nil(), zWadr(L, prefix(L)))] 70.26/30.97 70.26/30.97 [a__prefix(X)] = [1 0] X + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 >= [1 0] X + [0] 70.26/30.97 [0 1] [4] 70.26/30.97 = [prefix(X)] 70.26/30.97 70.26/30.97 70.26/30.97 We return to the main proof. 70.26/30.97 70.26/30.97 We are left with following problem, upon which TcT provides the 70.26/30.97 certificate YES(O(1),O(1)). 70.26/30.97 70.26/30.97 Weak Trs: 70.26/30.97 { a__app(X1, X2) -> app(X1, X2) 70.26/30.97 , a__app(nil(), YS) -> mark(YS) 70.26/30.97 , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) 70.26/30.97 , mark(nil()) -> nil() 70.26/30.97 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 70.26/30.97 , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) 70.26/30.97 , mark(from(X)) -> a__from(mark(X)) 70.26/30.97 , mark(s(X)) -> s(mark(X)) 70.26/30.97 , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) 70.26/30.97 , mark(prefix(X)) -> a__prefix(mark(X)) 70.26/30.97 , a__from(X) -> cons(mark(X), from(s(X))) 70.26/30.97 , a__from(X) -> from(X) 70.26/30.97 , a__zWadr(X1, X2) -> zWadr(X1, X2) 70.26/30.97 , a__zWadr(XS, nil()) -> nil() 70.26/30.97 , a__zWadr(nil(), YS) -> nil() 70.26/30.97 , a__zWadr(cons(X, XS), cons(Y, YS)) -> 70.26/30.97 cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) 70.26/30.97 , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) 70.26/30.97 , a__prefix(X) -> prefix(X) } 70.26/30.97 Obligation: 70.26/30.97 innermost runtime complexity 70.26/30.97 Answer: 70.26/30.97 YES(O(1),O(1)) 70.26/30.97 70.26/30.97 Empty rules are trivially bounded 70.26/30.97 70.26/30.97 Hurray, we answered YES(O(1),O(n^2)) 70.26/30.99 EOF