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