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