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