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