YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Arguments of following rules are not normal-forms: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [6] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [7] [activate](x1) = [1] x1 + [0] [isList](x1) = [1] x1 + [0] [isNeList](x1) = [1] x1 + [7] [n__nil] = [7] [n____](x1, x2) = [1] x1 + [1] x2 + [3] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [3] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [7] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [7] [n__a] = [7] [n__e] = [7] [n__i] = [7] [n__o] = [7] [n__u] = [7] [a] = [6] [e] = [6] [i] = [6] [o] = [6] [u] = [6] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [7] > [1] X1 + [1] X2 + [3] = [n____(X1, X2)] [nil()] = [6] ? [7] = [n__nil()] [and(tt(), X)] = [1] X + [7] > [1] X + [0] = [activate(X)] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [7] > [6] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [3] ? [1] X1 + [1] X2 + [7] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [0] >= [1] X + [0] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [0] ? [1] X + [7] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [0] ? [1] X + [7] = [isPal(X)] [activate(n__a())] = [7] > [6] = [a()] [activate(n__e())] = [7] > [6] = [e()] [activate(n__i())] = [7] > [6] = [i()] [activate(n__o())] = [7] > [6] = [o()] [activate(n__u())] = [7] > [6] = [u()] [isList(V)] = [1] V + [0] ? [1] V + [7] = [isNeList(activate(V))] [isList(X)] = [1] X + [0] >= [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [7] >= [7] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [3] > [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [7] > [1] V + [3] = [isQid(activate(V))] [isNeList(X)] = [1] X + [7] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] > [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] > [1] V1 + [1] V2 + [7] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [10] > [7] = [tt()] [isQid(n__e())] = [10] > [7] = [tt()] [isQid(n__i())] = [10] > [7] = [tt()] [isQid(n__o())] = [10] > [7] = [tt()] [isQid(n__u())] = [10] > [7] = [tt()] [isNePal(V)] = [1] V + [7] > [1] V + [3] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [13] > [1] I + [1] P + [3] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [7] >= [1] V + [7] = [isNePal(activate(V))] [isPal(X)] = [1] X + [7] > [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [14] > [7] = [tt()] [a()] = [6] ? [7] = [n__a()] [e()] = [6] ? [7] = [n__e()] [i()] = [6] ? [7] = [n__i()] [o()] = [6] ? [7] = [n__o()] [u()] = [6] ? [7] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { nil() -> n__nil() , activate(X) -> X , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isPal(V) -> isNePal(activate(V)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , and(tt(), X) -> activate(X) , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [1] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [0] [activate](x1) = [1] x1 + [0] [isList](x1) = [1] x1 + [0] [isNeList](x1) = [1] x1 + [0] [n__nil] = [1] [n____](x1, x2) = [1] x1 + [1] x2 + [0] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [4] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [4] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [0] [e] = [0] [i] = [0] [o] = [0] [u] = [0] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [n____(X1, X2)] [nil()] = [1] >= [1] = [n__nil()] [and(tt(), X)] = [1] X + [0] >= [1] X + [0] = [activate(X)] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [1] >= [1] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [0] >= [1] X + [0] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [0] >= [1] X + [0] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [0] ? [1] X + [4] = [isPal(X)] [activate(n__a())] = [0] >= [0] = [a()] [activate(n__e())] = [0] >= [0] = [e()] [activate(n__i())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [isList(V)] = [1] V + [0] >= [1] V + [0] = [isNeList(activate(V))] [isList(X)] = [1] X + [0] >= [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [1] > [0] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNeList(X)] = [1] X + [0] >= [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [tt()] [isNePal(V)] = [1] V + [4] > [1] V + [0] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [4] > [1] I + [1] P + [0] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] >= [1] V + [4] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [5] > [0] = [tt()] [a()] = [0] >= [0] = [n__a()] [e()] = [0] >= [0] = [n__e()] [i()] = [0] >= [0] = [n__i()] [o()] = [0] >= [0] = [n__o()] [u()] = [0] >= [0] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { nil() -> n__nil() , activate(X) -> X , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isPal(V) -> isNePal(activate(V)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , and(tt(), X) -> activate(X) , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [0] [activate](x1) = [1] x1 + [0] [isList](x1) = [1] x1 + [0] [isNeList](x1) = [1] x1 + [0] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [0] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [0] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [4] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [0] [e] = [0] [i] = [0] [o] = [0] [u] = [0] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [and(tt(), X)] = [1] X + [0] >= [1] X + [0] = [activate(X)] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [0] >= [0] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [0] >= [1] X + [0] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [0] >= [1] X + [0] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [0] ? [1] X + [4] = [isPal(X)] [activate(n__a())] = [0] >= [0] = [a()] [activate(n__e())] = [0] >= [0] = [e()] [activate(n__i())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [isList(V)] = [1] V + [0] >= [1] V + [0] = [isNeList(activate(V))] [isList(X)] = [1] X + [0] >= [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [0] >= [0] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNeList(X)] = [1] X + [0] >= [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] >= [1] V1 + [1] V2 + [0] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [tt()] [isNePal(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [0] >= [1] I + [1] P + [0] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] > [1] V + [0] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [4] > [0] = [tt()] [a()] = [0] >= [0] = [n__a()] [e()] = [0] >= [0] = [n__e()] [i()] = [0] >= [0] = [n__i()] [o()] = [0] >= [0] = [n__o()] [u()] = [0] >= [0] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { nil() -> n__nil() , activate(X) -> X , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , and(tt(), X) -> activate(X) , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [0] [activate](x1) = [1] x1 + [0] [isList](x1) = [1] x1 + [1] [isNeList](x1) = [1] x1 + [1] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [0] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [0] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [4] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [0] [e] = [0] [i] = [0] [o] = [0] [u] = [0] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [and(tt(), X)] = [1] X + [0] >= [1] X + [0] = [activate(X)] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [0] >= [0] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [0] ? [1] X + [1] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [0] ? [1] X + [1] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [0] ? [1] X + [4] = [isPal(X)] [activate(n__a())] = [0] >= [0] = [a()] [activate(n__e())] = [0] >= [0] = [e()] [activate(n__i())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [isList(V)] = [1] V + [1] >= [1] V + [1] = [isNeList(activate(V))] [isList(X)] = [1] X + [1] > [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [1] > [0] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [1] > [1] V + [0] = [isQid(activate(V))] [isNeList(X)] = [1] X + [1] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [tt()] [isNePal(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [0] >= [1] I + [1] P + [0] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] > [1] V + [0] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [4] > [0] = [tt()] [a()] = [0] >= [0] = [n__a()] [e()] = [0] >= [0] = [n__e()] [i()] = [0] >= [0] = [n__i()] [o()] = [0] >= [0] = [n__o()] [u()] = [0] >= [0] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { nil() -> n__nil() , activate(X) -> X , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , isList(V) -> isNeList(activate(V)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , and(tt(), X) -> activate(X) , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [0] [activate](x1) = [1] x1 + [0] [isList](x1) = [1] x1 + [1] [isNeList](x1) = [1] x1 + [0] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [1] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [0] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [0] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [0] [e] = [0] [i] = [0] [o] = [0] [u] = [0] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [and(tt(), X)] = [1] X + [0] >= [1] X + [0] = [activate(X)] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [0] >= [0] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [0] ? [1] X + [1] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [0] >= [1] X + [0] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [0] >= [1] X + [0] = [isPal(X)] [activate(n__a())] = [0] >= [0] = [a()] [activate(n__e())] = [0] >= [0] = [e()] [activate(n__i())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [isList(V)] = [1] V + [1] > [1] V + [0] = [isNeList(activate(V))] [isList(X)] = [1] X + [1] > [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [1] > [0] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] > [1] V1 + [1] V2 + [1] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNeList(X)] = [1] X + [0] >= [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] > [1] V1 + [1] V2 + [0] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [tt()] [isNePal(V)] = [1] V + [0] >= [1] V + [0] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [2] > [1] I + [1] P + [0] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [0] >= [1] V + [0] = [isNePal(activate(V))] [isPal(X)] = [1] X + [0] >= [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [0] >= [0] = [tt()] [a()] = [0] >= [0] = [n__a()] [e()] = [0] >= [0] = [n__e()] [i()] = [0] >= [0] = [n__i()] [o()] = [0] >= [0] = [n__o()] [u()] = [0] >= [0] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { nil() -> n__nil() , activate(X) -> X , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , and(tt(), X) -> activate(X) , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [6] [nil] = [5] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [4] [activate](x1) = [1] x1 + [2] [isList](x1) = [1] x1 + [6] [isNeList](x1) = [1] x1 + [4] [n__nil] = [4] [n____](x1, x2) = [1] x1 + [1] x2 + [6] [n__isList](x1) = [1] x1 + [2] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [2] [n__isPal](x1) = [1] x1 + [2] [isPal](x1) = [1] x1 + [4] [n__a] = [7] [n__e] = [7] [n__i] = [7] [n__o] = [7] [n__u] = [7] [a] = [5] [e] = [5] [i] = [5] [o] = [5] [u] = [5] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [6] >= [1] X1 + [1] X2 + [6] = [n____(X1, X2)] [nil()] = [5] > [4] = [n__nil()] [and(tt(), X)] = [1] X + [4] > [1] X + [2] = [activate(X)] [activate(X)] = [1] X + [2] > [1] X + [0] = [X] [activate(n__nil())] = [6] > [5] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8] ? [1] X1 + [1] X2 + [10] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [4] ? [1] X + [6] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [2] ? [1] X + [4] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [4] >= [1] X + [4] = [isPal(X)] [activate(n__a())] = [9] > [5] = [a()] [activate(n__e())] = [9] > [5] = [e()] [activate(n__i())] = [9] > [5] = [i()] [activate(n__o())] = [9] > [5] = [o()] [activate(n__u())] = [9] > [5] = [u()] [isList(V)] = [1] V + [6] >= [1] V + [6] = [isNeList(activate(V))] [isList(X)] = [1] X + [6] > [1] X + [2] = [n__isList(X)] [isList(n__nil())] = [10] > [4] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [12] >= [1] V1 + [1] V2 + [12] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [4] > [1] V + [2] = [isQid(activate(V))] [isNeList(X)] = [1] X + [4] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] >= [1] V1 + [1] V2 + [10] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] >= [1] V1 + [1] V2 + [10] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [7] > [4] = [tt()] [isQid(n__e())] = [7] > [4] = [tt()] [isQid(n__i())] = [7] > [4] = [tt()] [isQid(n__o())] = [7] > [4] = [tt()] [isQid(n__u())] = [7] > [4] = [tt()] [isNePal(V)] = [1] V + [2] >= [1] V + [2] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [14] > [1] I + [1] P + [6] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] >= [1] V + [4] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [2] = [n__isPal(X)] [isPal(n__nil())] = [8] > [4] = [tt()] [a()] = [5] ? [7] = [n__a()] [e()] = [5] ? [7] = [n__e()] [i()] = [5] ? [7] = [n__i()] [o()] = [5] ? [7] = [n__o()] [u()] = [5] ? [7] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [6] [nil] = [2] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [2] [activate](x1) = [1] x1 + [2] [isList](x1) = [1] x1 + [6] [isNeList](x1) = [1] x1 + [4] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [6] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [2] [n__isPal](x1) = [1] x1 + [0] [isPal](x1) = [1] x1 + [4] [n__a] = [6] [n__e] = [2] [n__i] = [6] [n__o] = [6] [n__u] = [6] [a] = [7] [e] = [3] [i] = [7] [o] = [7] [u] = [7] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [6] >= [1] X1 + [1] X2 + [6] = [n____(X1, X2)] [nil()] = [2] > [0] = [n__nil()] [and(tt(), X)] = [1] X + [2] >= [1] X + [2] = [activate(X)] [activate(X)] = [1] X + [2] > [1] X + [0] = [X] [activate(n__nil())] = [2] >= [2] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8] ? [1] X1 + [1] X2 + [10] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [2] ? [1] X + [6] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [2] ? [1] X + [4] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [2] ? [1] X + [4] = [isPal(X)] [activate(n__a())] = [8] > [7] = [a()] [activate(n__e())] = [4] > [3] = [e()] [activate(n__i())] = [8] > [7] = [i()] [activate(n__o())] = [8] > [7] = [o()] [activate(n__u())] = [8] > [7] = [u()] [isList(V)] = [1] V + [6] >= [1] V + [6] = [isNeList(activate(V))] [isList(X)] = [1] X + [6] > [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [6] > [2] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [12] > [1] V1 + [1] V2 + [10] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [4] > [1] V + [2] = [isQid(activate(V))] [isNeList(X)] = [1] X + [4] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] >= [1] V1 + [1] V2 + [10] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] > [1] V1 + [1] V2 + [8] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [6] > [2] = [tt()] [isQid(n__e())] = [2] >= [2] = [tt()] [isQid(n__i())] = [6] > [2] = [tt()] [isQid(n__o())] = [6] > [2] = [tt()] [isQid(n__u())] = [6] > [2] = [tt()] [isNePal(V)] = [1] V + [2] >= [1] V + [2] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [14] > [1] I + [1] P + [4] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] >= [1] V + [4] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [0] = [n__isPal(X)] [isPal(n__nil())] = [4] > [2] = [tt()] [a()] = [7] > [6] = [n__a()] [e()] = [3] > [2] = [n__e()] [i()] = [7] > [6] = [n__i()] [o()] = [7] > [6] = [n__o()] [u()] = [7] > [6] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [6] [nil] = [1] [and](x1, x2) = [1] x1 + [1] x2 + [1] [tt] = [0] [activate](x1) = [1] x1 + [1] [isList](x1) = [1] x1 + [5] [isNeList](x1) = [1] x1 + [4] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [4] [n__isList](x1) = [1] x1 + [0] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [1] [n__isPal](x1) = [1] x1 + [4] [isPal](x1) = [1] x1 + [4] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [1] [e] = [1] [i] = [1] [o] = [1] [u] = [1] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [6] > [1] X1 + [1] X2 + [4] = [n____(X1, X2)] [nil()] = [1] > [0] = [n__nil()] [and(tt(), X)] = [1] X + [1] >= [1] X + [1] = [activate(X)] [activate(X)] = [1] X + [1] > [1] X + [0] = [X] [activate(n__nil())] = [1] >= [1] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5] ? [1] X1 + [1] X2 + [8] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [1] ? [1] X + [5] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [1] ? [1] X + [4] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [5] > [1] X + [4] = [isPal(X)] [activate(n__a())] = [1] >= [1] = [a()] [activate(n__e())] = [1] >= [1] = [e()] [activate(n__i())] = [1] >= [1] = [i()] [activate(n__o())] = [1] >= [1] = [o()] [activate(n__u())] = [1] >= [1] = [u()] [isList(V)] = [1] V + [5] >= [1] V + [5] = [isNeList(activate(V))] [isList(X)] = [1] X + [5] > [1] X + [0] = [n__isList(X)] [isList(n__nil())] = [5] > [0] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [9] > [1] V1 + [1] V2 + [8] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [4] > [1] V + [1] = [isQid(activate(V))] [isNeList(X)] = [1] X + [4] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [8] >= [1] V1 + [1] V2 + [8] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [8] > [1] V1 + [1] V2 + [7] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [tt()] [isNePal(V)] = [1] V + [1] >= [1] V + [1] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [9] > [1] I + [1] P + [7] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] > [1] V + [2] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] >= [1] X + [4] = [n__isPal(X)] [isPal(n__nil())] = [4] > [0] = [tt()] [a()] = [1] > [0] = [n__a()] [e()] = [1] > [0] = [n__e()] [i()] = [1] > [0] = [n__i()] [o()] = [1] > [0] = [n__o()] [u()] = [1] > [0] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [4] [nil] = [1] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [1] [activate](x1) = [1] x1 + [1] [isList](x1) = [1] x1 + [2] [isNeList](x1) = [1] x1 + [1] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [4] [n__isList](x1) = [1] x1 + [2] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [0] [isNePal](x1) = [1] x1 + [1] [n__isPal](x1) = [1] x1 + [3] [isPal](x1) = [1] x1 + [4] [n__a] = [1] [n__e] = [4] [n__i] = [4] [n__o] = [3] [n__u] = [4] [a] = [1] [e] = [5] [i] = [5] [o] = [4] [u] = [5] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = [n____(X1, X2)] [nil()] = [1] > [0] = [n__nil()] [and(tt(), X)] = [1] X + [1] >= [1] X + [1] = [activate(X)] [activate(X)] = [1] X + [1] > [1] X + [0] = [X] [activate(n__nil())] = [1] >= [1] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5] ? [1] X1 + [1] X2 + [6] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [3] > [1] X + [2] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [1] >= [1] X + [1] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [4] >= [1] X + [4] = [isPal(X)] [activate(n__a())] = [2] > [1] = [a()] [activate(n__e())] = [5] >= [5] = [e()] [activate(n__i())] = [5] >= [5] = [i()] [activate(n__o())] = [4] >= [4] = [o()] [activate(n__u())] = [5] >= [5] = [u()] [isList(V)] = [1] V + [2] >= [1] V + [2] = [isNeList(activate(V))] [isList(X)] = [1] X + [2] >= [1] X + [2] = [n__isList(X)] [isList(n__nil())] = [2] > [1] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [6] >= [1] V1 + [1] V2 + [6] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [1] >= [1] V + [1] = [isQid(activate(V))] [isNeList(X)] = [1] X + [1] > [1] X + [0] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5] > [1] V1 + [1] V2 + [4] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5] >= [1] V1 + [1] V2 + [5] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [1] >= [1] = [tt()] [isQid(n__e())] = [4] > [1] = [tt()] [isQid(n__i())] = [4] > [1] = [tt()] [isQid(n__o())] = [3] > [1] = [tt()] [isQid(n__u())] = [4] > [1] = [tt()] [isNePal(V)] = [1] V + [1] >= [1] V + [1] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [9] > [1] I + [1] P + [5] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] > [1] V + [2] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [3] = [n__isPal(X)] [isPal(n__nil())] = [4] > [1] = [tt()] [a()] = [1] >= [1] = [n__a()] [e()] = [5] > [4] = [n__e()] [i()] = [5] > [4] = [n__i()] [o()] = [4] > [3] = [n__o()] [u()] = [5] > [4] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isNeList(X)) -> isNeList(X) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n__isList(X)) -> isList(X) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [1] [and](x1, x2) = [1] x1 + [1] x2 + [0] [tt] = [1] [activate](x1) = [1] x1 + [1] [isList](x1) = [1] x1 + [4] [isNeList](x1) = [1] x1 + [3] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [7] [n__isList](x1) = [1] x1 + [4] [isQid](x1) = [1] x1 + [0] [n__isNeList](x1) = [1] x1 + [3] [isNePal](x1) = [1] x1 + [1] [n__isPal](x1) = [1] x1 + [3] [isPal](x1) = [1] x1 + [4] [n__a] = [4] [n__e] = [4] [n__i] = [1] [n__o] = [2] [n__u] = [1] [a] = [5] [e] = [5] [i] = [1] [o] = [3] [u] = [1] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = [n____(X1, X2)] [nil()] = [1] > [0] = [n__nil()] [and(tt(), X)] = [1] X + [1] >= [1] X + [1] = [activate(X)] [activate(X)] = [1] X + [1] > [1] X + [0] = [X] [activate(n__nil())] = [1] >= [1] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8] ? [1] X1 + [1] X2 + [9] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1] X + [5] > [1] X + [4] = [isList(X)] [activate(n__isNeList(X))] = [1] X + [4] > [1] X + [3] = [isNeList(X)] [activate(n__isPal(X))] = [1] X + [4] >= [1] X + [4] = [isPal(X)] [activate(n__a())] = [5] >= [5] = [a()] [activate(n__e())] = [5] >= [5] = [e()] [activate(n__i())] = [2] > [1] = [i()] [activate(n__o())] = [3] >= [3] = [o()] [activate(n__u())] = [2] > [1] = [u()] [isList(V)] = [1] V + [4] >= [1] V + [4] = [isNeList(activate(V))] [isList(X)] = [1] X + [4] >= [1] X + [4] = [n__isList(X)] [isList(n__nil())] = [4] > [1] = [tt()] [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [11] > [1] V1 + [1] V2 + [10] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1] V + [3] > [1] V + [1] = [isQid(activate(V))] [isNeList(X)] = [1] X + [3] >= [1] X + [3] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] > [1] V1 + [1] V2 + [9] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10] > [1] V1 + [1] V2 + [9] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [4] > [1] = [tt()] [isQid(n__e())] = [4] > [1] = [tt()] [isQid(n__i())] = [1] >= [1] = [tt()] [isQid(n__o())] = [2] > [1] = [tt()] [isQid(n__u())] = [1] >= [1] = [tt()] [isNePal(V)] = [1] V + [1] >= [1] V + [1] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [15] > [1] I + [1] P + [5] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1] V + [4] > [1] V + [2] = [isNePal(activate(V))] [isPal(X)] = [1] X + [4] > [1] X + [3] = [n__isPal(X)] [isPal(n__nil())] = [4] > [1] = [tt()] [a()] = [5] > [4] = [n__a()] [e()] = [5] > [4] = [n__e()] [i()] = [1] >= [1] = [n__i()] [o()] = [3] > [2] = [n__o()] [u()] = [1] >= [1] = [n__u()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(__) = {1, 2}, Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n__isList) = {1}, Uargs(isQid) = {1}, Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}, Uargs(n__isPal) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [1 2] x1 + [1 2] x2 + [2] [0 1] [0 1] [2] [nil] = [0] [0] [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 1] [0] [tt] = [0] [0] [activate](x1) = [1 1] x1 + [0] [0 1] [0] [isList](x1) = [1 2] x1 + [0] [0 1] [4] [isNeList](x1) = [1 1] x1 + [0] [0 1] [4] [n__nil] = [0] [0] [n____](x1, x2) = [1 2] x1 + [1 2] x2 + [2] [0 1] [0 1] [2] [n__isList](x1) = [1 1] x1 + [0] [0 1] [4] [isQid](x1) = [1 0] x1 + [0] [0 0] [4] [n__isNeList](x1) = [1 0] x1 + [0] [0 1] [4] [isNePal](x1) = [1 1] x1 + [0] [0 0] [4] [n__isPal](x1) = [1 2] x1 + [0] [0 0] [4] [isPal](x1) = [1 2] x1 + [4] [0 0] [4] [n__a] = [0] [0] [n__e] = [0] [0] [n__i] = [4] [0] [n__o] = [0] [0] [n__u] = [0] [0] [a] = [0] [0] [e] = [0] [0] [i] = [4] [0] [o] = [0] [0] [u] = [0] [0] The following symbols are considered usable {__, nil, and, activate, isList, isNeList, isQid, isNePal, isPal, a, e, i, o, u} The order satisfies the following ordering constraints: [__(X1, X2)] = [1 2] X1 + [1 2] X2 + [2] [0 1] [0 1] [2] >= [1 2] X1 + [1 2] X2 + [2] [0 1] [0 1] [2] = [n____(X1, X2)] [nil()] = [0] [0] >= [0] [0] = [n__nil()] [and(tt(), X)] = [1 1] X + [0] [0 1] [0] >= [1 1] X + [0] [0 1] [0] = [activate(X)] [activate(X)] = [1 1] X + [0] [0 1] [0] >= [1 0] X + [0] [0 1] [0] = [X] [activate(n__nil())] = [0] [0] >= [0] [0] = [nil()] [activate(n____(X1, X2))] = [1 3] X1 + [1 3] X2 + [4] [0 1] [0 1] [2] > [1 3] X1 + [1 3] X2 + [2] [0 1] [0 1] [2] = [__(activate(X1), activate(X2))] [activate(n__isList(X))] = [1 2] X + [4] [0 1] [4] > [1 2] X + [0] [0 1] [4] = [isList(X)] [activate(n__isNeList(X))] = [1 1] X + [4] [0 1] [4] > [1 1] X + [0] [0 1] [4] = [isNeList(X)] [activate(n__isPal(X))] = [1 2] X + [4] [0 0] [4] >= [1 2] X + [4] [0 0] [4] = [isPal(X)] [activate(n__a())] = [0] [0] >= [0] [0] = [a()] [activate(n__e())] = [0] [0] >= [0] [0] = [e()] [activate(n__i())] = [4] [0] >= [4] [0] = [i()] [activate(n__o())] = [0] [0] >= [0] [0] = [o()] [activate(n__u())] = [0] [0] >= [0] [0] = [u()] [isList(V)] = [1 2] V + [0] [0 1] [4] >= [1 2] V + [0] [0 1] [4] = [isNeList(activate(V))] [isList(X)] = [1 2] X + [0] [0 1] [4] >= [1 1] X + [0] [0 1] [4] = [n__isList(X)] [isList(n__nil())] = [0] [4] >= [0] [0] = [tt()] [isList(n____(V1, V2))] = [1 4] V1 + [1 4] V2 + [6] [0 1] [0 1] [6] > [1 3] V1 + [1 3] V2 + [4] [0 0] [0 1] [4] = [and(isList(activate(V1)), n__isList(activate(V2)))] [isNeList(V)] = [1 1] V + [0] [0 1] [4] >= [1 1] V + [0] [0 0] [4] = [isQid(activate(V))] [isNeList(X)] = [1 1] X + [0] [0 1] [4] >= [1 0] X + [0] [0 1] [4] = [n__isNeList(X)] [isNeList(n____(V1, V2))] = [1 3] V1 + [1 3] V2 + [4] [0 1] [0 1] [6] >= [1 3] V1 + [1 2] V2 + [4] [0 0] [0 1] [4] = [and(isList(activate(V1)), n__isNeList(activate(V2)))] [isNeList(n____(V1, V2))] = [1 3] V1 + [1 3] V2 + [4] [0 1] [0 1] [6] >= [1 2] V1 + [1 3] V2 + [4] [0 0] [0 1] [4] = [and(isNeList(activate(V1)), n__isList(activate(V2)))] [isQid(n__a())] = [0] [4] >= [0] [0] = [tt()] [isQid(n__e())] = [0] [4] >= [0] [0] = [tt()] [isQid(n__i())] = [4] [4] > [0] [0] = [tt()] [isQid(n__o())] = [0] [4] >= [0] [0] = [tt()] [isQid(n__u())] = [0] [4] >= [0] [0] = [tt()] [isNePal(V)] = [1 1] V + [0] [0 0] [4] >= [1 1] V + [0] [0 0] [4] = [isQid(activate(V))] [isNePal(n____(I, n____(P, I)))] = [2 8] I + [1 5] P + [12] [0 0] [0 0] [4] > [1 1] I + [1 3] P + [4] [0 0] [0 0] [4] = [and(isQid(activate(I)), n__isPal(activate(P)))] [isPal(V)] = [1 2] V + [4] [0 0] [4] > [1 2] V + [0] [0 0] [4] = [isNePal(activate(V))] [isPal(X)] = [1 2] X + [4] [0 0] [4] > [1 2] X + [0] [0 0] [4] = [n__isPal(X)] [isPal(n__nil())] = [4] [4] > [0] [0] = [tt()] [a()] = [0] [0] >= [0] [0] = [n__a()] [e()] = [0] [0] >= [0] [0] = [n__e()] [i()] = [4] [0] >= [4] [0] = [n__i()] [o()] = [0] [0] >= [0] [0] = [n__o()] [u()] = [0] [0] >= [0] [0] = [n__u()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))