YES(O(1),O(n^2)) 171.50/60.11 YES(O(1),O(n^2)) 171.50/60.11 171.50/60.11 We are left with following problem, upon which TcT provides the 171.50/60.11 certificate YES(O(1),O(n^2)). 171.50/60.11 171.50/60.11 Strict Trs: 171.50/60.11 { __(X1, X2) -> n____(X1, X2) 171.50/60.11 , __(X, nil()) -> X 171.50/60.11 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.11 , __(nil(), X) -> X 171.50/60.11 , nil() -> n__nil() 171.50/60.11 , and(tt(), X) -> activate(X) 171.50/60.11 , activate(X) -> X 171.50/60.11 , activate(n__nil()) -> nil() 171.50/60.11 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.11 , activate(n__isList(X)) -> isList(X) 171.50/60.11 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.11 , activate(n__isPal(X)) -> isPal(X) 171.50/60.11 , activate(n__a()) -> a() 171.50/60.11 , activate(n__e()) -> e() 171.50/60.11 , activate(n__i()) -> i() 171.50/60.11 , activate(n__o()) -> o() 171.50/60.11 , activate(n__u()) -> u() 171.50/60.11 , isList(V) -> isNeList(activate(V)) 171.50/60.11 , isList(X) -> n__isList(X) 171.50/60.11 , isList(n__nil()) -> tt() 171.50/60.11 , isList(n____(V1, V2)) -> 171.50/60.11 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.11 , isNeList(V) -> isQid(activate(V)) 171.50/60.11 , isNeList(X) -> n__isNeList(X) 171.50/60.11 , isNeList(n____(V1, V2)) -> 171.50/60.11 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.11 , isNeList(n____(V1, V2)) -> 171.50/60.11 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.11 , isQid(n__a()) -> tt() 171.50/60.11 , isQid(n__e()) -> tt() 171.50/60.11 , isQid(n__i()) -> tt() 171.50/60.11 , isQid(n__o()) -> tt() 171.50/60.11 , isQid(n__u()) -> tt() 171.50/60.11 , isNePal(V) -> isQid(activate(V)) 171.50/60.11 , isNePal(n____(I, __(P, I))) -> 171.50/60.11 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.11 , isPal(V) -> isNePal(activate(V)) 171.50/60.11 , isPal(X) -> n__isPal(X) 171.50/60.11 , isPal(n__nil()) -> tt() 171.50/60.11 , a() -> n__a() 171.50/60.11 , e() -> n__e() 171.50/60.11 , i() -> n__i() 171.50/60.11 , o() -> n__o() 171.50/60.11 , u() -> n__u() } 171.50/60.11 Obligation: 171.50/60.11 derivational complexity 171.50/60.11 Answer: 171.50/60.11 YES(O(1),O(n^2)) 171.50/60.11 171.50/60.11 We use the processor 'matrix interpretation of dimension 1' to 171.50/60.11 orient following rules strictly. 171.50/60.11 171.50/60.11 Trs: { isQid(n__u()) -> tt() } 171.50/60.11 171.50/60.11 The induced complexity on above rules (modulo remaining rules) is 171.50/60.11 YES(?,O(n^1)) . These rules are moved into the corresponding weak 171.50/60.11 component(s). 171.50/60.11 171.50/60.11 Sub-proof: 171.50/60.11 ---------- 171.50/60.11 TcT has computed the following triangular matrix interpretation. 171.50/60.11 171.50/60.11 [__](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.11 171.50/60.11 [nil] = [0] 171.50/60.12 171.50/60.12 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.12 171.50/60.12 [tt] = [0] 171.50/60.12 171.50/60.12 [activate](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [isList](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [isNeList](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [n__nil] = [0] 171.50/60.12 171.50/60.12 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.12 171.50/60.12 [n__isList](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [isQid](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [n__isNeList](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [isNePal](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [n__isPal](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [isPal](x1) = [1] x1 + [0] 171.50/60.12 171.50/60.12 [n__a] = [0] 171.50/60.12 171.50/60.12 [n__e] = [0] 171.50/60.12 171.50/60.12 [n__i] = [0] 171.50/60.12 171.50/60.12 [n__o] = [0] 171.50/60.12 171.50/60.12 [n__u] = [1] 171.50/60.12 171.50/60.12 [a] = [0] 171.50/60.12 171.50/60.12 [e] = [0] 171.50/60.12 171.50/60.12 [i] = [0] 171.50/60.12 171.50/60.12 [o] = [0] 171.50/60.12 171.50/60.12 [u] = [1] 171.50/60.12 171.50/60.12 The order satisfies the following ordering constraints: 171.50/60.12 171.50/60.12 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 171.50/60.12 >= [1] X1 + [1] X2 + [0] 171.50/60.12 = [n____(X1, X2)] 171.50/60.12 171.50/60.12 [__(X, nil())] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 171.50/60.12 >= [1] X + [1] Y + [1] Z + [0] 171.50/60.12 = [__(X, __(Y, Z))] 171.50/60.12 171.50/60.12 [__(nil(), X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [nil()] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [n__nil()] 171.50/60.12 171.50/60.12 [and(tt(), X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [activate(X)] 171.50/60.12 171.50/60.12 [activate(X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [activate(n__nil())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [nil()] 171.50/60.12 171.50/60.12 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 171.50/60.12 >= [1] X1 + [1] X2 + [0] 171.50/60.12 = [__(X1, X2)] 171.50/60.12 171.50/60.12 [activate(n__isList(X))] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [isList(X)] 171.50/60.12 171.50/60.12 [activate(n__isNeList(X))] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [isNeList(X)] 171.50/60.12 171.50/60.12 [activate(n__isPal(X))] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [isPal(X)] 171.50/60.12 171.50/60.12 [activate(n__a())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [a()] 171.50/60.12 171.50/60.12 [activate(n__e())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [e()] 171.50/60.12 171.50/60.12 [activate(n__i())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [i()] 171.50/60.12 171.50/60.12 [activate(n__o())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [o()] 171.50/60.12 171.50/60.12 [activate(n__u())] = [1] 171.50/60.12 >= [1] 171.50/60.12 = [u()] 171.50/60.12 171.50/60.12 [isList(V)] = [1] V + [0] 171.50/60.12 >= [1] V + [0] 171.50/60.12 = [isNeList(activate(V))] 171.50/60.12 171.50/60.12 [isList(X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [n__isList(X)] 171.50/60.12 171.50/60.12 [isList(n__nil())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.12 >= [1] V1 + [1] V2 + [0] 171.50/60.12 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(V)] = [1] V + [0] 171.50/60.12 >= [1] V + [0] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNeList(X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [n__isNeList(X)] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.12 >= [1] V1 + [1] V2 + [0] 171.50/60.12 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.12 >= [1] V1 + [1] V2 + [0] 171.50/60.12 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isQid(n__a())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__e())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__i())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__o())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__u())] = [1] 171.50/60.12 > [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isNePal(V)] = [1] V + [0] 171.50/60.12 >= [1] V + [0] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [0] 171.50/60.12 >= [1] I + [1] P + [0] 171.50/60.12 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.12 171.50/60.12 [isPal(V)] = [1] V + [0] 171.50/60.12 >= [1] V + [0] 171.50/60.12 = [isNePal(activate(V))] 171.50/60.12 171.50/60.12 [isPal(X)] = [1] X + [0] 171.50/60.12 >= [1] X + [0] 171.50/60.12 = [n__isPal(X)] 171.50/60.12 171.50/60.12 [isPal(n__nil())] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [a()] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [n__a()] 171.50/60.12 171.50/60.12 [e()] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [n__e()] 171.50/60.12 171.50/60.12 [i()] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [n__i()] 171.50/60.12 171.50/60.12 [o()] = [0] 171.50/60.12 >= [0] 171.50/60.12 = [n__o()] 171.50/60.12 171.50/60.12 [u()] = [1] 171.50/60.12 >= [1] 171.50/60.12 = [n__u()] 171.50/60.12 171.50/60.12 171.50/60.12 We return to the main proof. 171.50/60.12 171.50/60.12 We are left with following problem, upon which TcT provides the 171.50/60.12 certificate YES(O(1),O(n^2)). 171.50/60.12 171.50/60.12 Strict Trs: 171.50/60.12 { __(X1, X2) -> n____(X1, X2) 171.50/60.12 , __(X, nil()) -> X 171.50/60.12 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.12 , __(nil(), X) -> X 171.50/60.12 , nil() -> n__nil() 171.50/60.12 , and(tt(), X) -> activate(X) 171.50/60.12 , activate(X) -> X 171.50/60.12 , activate(n__nil()) -> nil() 171.50/60.12 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.12 , activate(n__isList(X)) -> isList(X) 171.50/60.12 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.12 , activate(n__isPal(X)) -> isPal(X) 171.50/60.12 , activate(n__a()) -> a() 171.50/60.12 , activate(n__e()) -> e() 171.50/60.12 , activate(n__i()) -> i() 171.50/60.12 , activate(n__o()) -> o() 171.50/60.12 , activate(n__u()) -> u() 171.50/60.12 , isList(V) -> isNeList(activate(V)) 171.50/60.12 , isList(X) -> n__isList(X) 171.50/60.12 , isList(n__nil()) -> tt() 171.50/60.12 , isList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.12 , isNeList(V) -> isQid(activate(V)) 171.50/60.12 , isNeList(X) -> n__isNeList(X) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.12 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.12 , isQid(n__a()) -> tt() 171.50/60.12 , isQid(n__e()) -> tt() 171.50/60.12 , isQid(n__i()) -> tt() 171.50/60.12 , isQid(n__o()) -> tt() 171.50/60.12 , isNePal(V) -> isQid(activate(V)) 171.50/60.12 , isNePal(n____(I, __(P, I))) -> 171.50/60.12 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.12 , isPal(V) -> isNePal(activate(V)) 171.50/60.12 , isPal(X) -> n__isPal(X) 171.50/60.12 , isPal(n__nil()) -> tt() 171.50/60.12 , a() -> n__a() 171.50/60.12 , e() -> n__e() 171.50/60.12 , i() -> n__i() 171.50/60.12 , o() -> n__o() 171.50/60.12 , u() -> n__u() } 171.50/60.12 Weak Trs: { isQid(n__u()) -> tt() } 171.50/60.12 Obligation: 171.50/60.12 derivational complexity 171.50/60.12 Answer: 171.50/60.12 YES(O(1),O(n^2)) 171.50/60.12 171.50/60.12 The weightgap principle applies (using the following nonconstant 171.50/60.12 growth matrix-interpretation) 171.50/60.12 171.50/60.12 TcT has computed the following triangular matrix interpretation. 171.50/60.12 Note that the diagonal of the component-wise maxima of 171.50/60.12 interpretation-entries contains no more than 1 non-zero entries. 171.50/60.12 171.50/60.12 [__](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [nil] = [2] 171.50/60.12 171.50/60.12 [and](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [tt] = [1] 171.50/60.12 171.50/60.12 [activate](x1) = [1] x1 + [2] 171.50/60.12 171.50/60.12 [isList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isNeList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__nil] = [1] 171.50/60.12 171.50/60.12 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [n__isList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isQid](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__isNeList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isNePal](x1) = [1] x1 + [2] 171.50/60.12 171.50/60.12 [n__isPal](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isPal](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__a] = [1] 171.50/60.12 171.50/60.12 [n__e] = [1] 171.50/60.12 171.50/60.12 [n__i] = [1] 171.50/60.12 171.50/60.12 [n__o] = [1] 171.50/60.12 171.50/60.12 [n__u] = [2] 171.50/60.12 171.50/60.12 [a] = [2] 171.50/60.12 171.50/60.12 [e] = [2] 171.50/60.12 171.50/60.12 [i] = [2] 171.50/60.12 171.50/60.12 [o] = [2] 171.50/60.12 171.50/60.12 [u] = [2] 171.50/60.12 171.50/60.12 The order satisfies the following ordering constraints: 171.50/60.12 171.50/60.12 [__(X1, X2)] = [1] X1 + [1] X2 + [1] 171.50/60.12 >= [1] X1 + [1] X2 + [1] 171.50/60.12 = [n____(X1, X2)] 171.50/60.12 171.50/60.12 [__(X, nil())] = [1] X + [3] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2] 171.50/60.12 >= [1] X + [1] Y + [1] Z + [2] 171.50/60.12 = [__(X, __(Y, Z))] 171.50/60.12 171.50/60.12 [__(nil(), X)] = [1] X + [3] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [nil()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__nil()] 171.50/60.12 171.50/60.12 [and(tt(), X)] = [1] X + [2] 171.50/60.12 >= [1] X + [2] 171.50/60.12 = [activate(X)] 171.50/60.12 171.50/60.12 [activate(X)] = [1] X + [2] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [activate(n__nil())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [nil()] 171.50/60.12 171.50/60.12 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [3] 171.50/60.12 > [1] X1 + [1] X2 + [1] 171.50/60.12 = [__(X1, X2)] 171.50/60.12 171.50/60.12 [activate(n__isList(X))] = [1] X + [3] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [isList(X)] 171.50/60.12 171.50/60.12 [activate(n__isNeList(X))] = [1] X + [3] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [isNeList(X)] 171.50/60.12 171.50/60.12 [activate(n__isPal(X))] = [1] X + [3] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [isPal(X)] 171.50/60.12 171.50/60.12 [activate(n__a())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [a()] 171.50/60.12 171.50/60.12 [activate(n__e())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [e()] 171.50/60.12 171.50/60.12 [activate(n__i())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [i()] 171.50/60.12 171.50/60.12 [activate(n__o())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [o()] 171.50/60.12 171.50/60.12 [activate(n__u())] = [4] 171.50/60.12 > [2] 171.50/60.12 = [u()] 171.50/60.12 171.50/60.12 [isList(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isNeList(activate(V))] 171.50/60.12 171.50/60.12 [isList(X)] = [1] X + [1] 171.50/60.12 >= [1] X + [1] 171.50/60.12 = [n__isList(X)] 171.50/60.12 171.50/60.12 [isList(n__nil())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNeList(X)] = [1] X + [1] 171.50/60.12 >= [1] X + [1] 171.50/60.12 = [n__isNeList(X)] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isQid(n__a())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__e())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__i())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__o())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__u())] = [3] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isNePal(V)] = [1] V + [2] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4] 171.50/60.12 ? [1] I + [1] P + [7] 171.50/60.12 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.12 171.50/60.12 [isPal(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [4] 171.50/60.12 = [isNePal(activate(V))] 171.50/60.12 171.50/60.12 [isPal(X)] = [1] X + [1] 171.50/60.12 >= [1] X + [1] 171.50/60.12 = [n__isPal(X)] 171.50/60.12 171.50/60.12 [isPal(n__nil())] = [2] 171.50/60.12 > [1] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [a()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__a()] 171.50/60.12 171.50/60.12 [e()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__e()] 171.50/60.12 171.50/60.12 [i()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__i()] 171.50/60.12 171.50/60.12 [o()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__o()] 171.50/60.12 171.50/60.12 [u()] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [n__u()] 171.50/60.12 171.50/60.12 171.50/60.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.50/60.12 171.50/60.12 We are left with following problem, upon which TcT provides the 171.50/60.12 certificate YES(O(1),O(n^2)). 171.50/60.12 171.50/60.12 Strict Trs: 171.50/60.12 { __(X1, X2) -> n____(X1, X2) 171.50/60.12 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.12 , and(tt(), X) -> activate(X) 171.50/60.12 , isList(V) -> isNeList(activate(V)) 171.50/60.12 , isList(X) -> n__isList(X) 171.50/60.12 , isList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.12 , isNeList(V) -> isQid(activate(V)) 171.50/60.12 , isNeList(X) -> n__isNeList(X) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.12 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.12 , isNePal(V) -> isQid(activate(V)) 171.50/60.12 , isNePal(n____(I, __(P, I))) -> 171.50/60.12 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.12 , isPal(V) -> isNePal(activate(V)) 171.50/60.12 , isPal(X) -> n__isPal(X) 171.50/60.12 , u() -> n__u() } 171.50/60.12 Weak Trs: 171.50/60.12 { __(X, nil()) -> X 171.50/60.12 , __(nil(), X) -> X 171.50/60.12 , nil() -> n__nil() 171.50/60.12 , activate(X) -> X 171.50/60.12 , activate(n__nil()) -> nil() 171.50/60.12 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.12 , activate(n__isList(X)) -> isList(X) 171.50/60.12 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.12 , activate(n__isPal(X)) -> isPal(X) 171.50/60.12 , activate(n__a()) -> a() 171.50/60.12 , activate(n__e()) -> e() 171.50/60.12 , activate(n__i()) -> i() 171.50/60.12 , activate(n__o()) -> o() 171.50/60.12 , activate(n__u()) -> u() 171.50/60.12 , isList(n__nil()) -> tt() 171.50/60.12 , isQid(n__a()) -> tt() 171.50/60.12 , isQid(n__e()) -> tt() 171.50/60.12 , isQid(n__i()) -> tt() 171.50/60.12 , isQid(n__o()) -> tt() 171.50/60.12 , isQid(n__u()) -> tt() 171.50/60.12 , isPal(n__nil()) -> tt() 171.50/60.12 , a() -> n__a() 171.50/60.12 , e() -> n__e() 171.50/60.12 , i() -> n__i() 171.50/60.12 , o() -> n__o() } 171.50/60.12 Obligation: 171.50/60.12 derivational complexity 171.50/60.12 Answer: 171.50/60.12 YES(O(1),O(n^2)) 171.50/60.12 171.50/60.12 The weightgap principle applies (using the following nonconstant 171.50/60.12 growth matrix-interpretation) 171.50/60.12 171.50/60.12 TcT has computed the following triangular matrix interpretation. 171.50/60.12 Note that the diagonal of the component-wise maxima of 171.50/60.12 interpretation-entries contains no more than 1 non-zero entries. 171.50/60.12 171.50/60.12 [__](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [nil] = [2] 171.50/60.12 171.50/60.12 [and](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [tt] = [2] 171.50/60.12 171.50/60.12 [activate](x1) = [1] x1 + [2] 171.50/60.12 171.50/60.12 [isList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isNeList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__nil] = [1] 171.50/60.12 171.50/60.12 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.12 171.50/60.12 [n__isList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isQid](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__isNeList](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isNePal](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [n__isPal](x1) = [1] x1 + [1] 171.50/60.12 171.50/60.12 [isPal](x1) = [1] x1 + [2] 171.50/60.12 171.50/60.12 [n__a] = [1] 171.50/60.12 171.50/60.12 [n__e] = [1] 171.50/60.12 171.50/60.12 [n__i] = [1] 171.50/60.12 171.50/60.12 [n__o] = [1] 171.50/60.12 171.50/60.12 [n__u] = [1] 171.50/60.12 171.50/60.12 [a] = [2] 171.50/60.12 171.50/60.12 [e] = [2] 171.50/60.12 171.50/60.12 [i] = [2] 171.50/60.12 171.50/60.12 [o] = [2] 171.50/60.12 171.50/60.12 [u] = [2] 171.50/60.12 171.50/60.12 The order satisfies the following ordering constraints: 171.50/60.12 171.50/60.12 [__(X1, X2)] = [1] X1 + [1] X2 + [1] 171.50/60.12 >= [1] X1 + [1] X2 + [1] 171.50/60.12 = [n____(X1, X2)] 171.50/60.12 171.50/60.12 [__(X, nil())] = [1] X + [3] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2] 171.50/60.12 >= [1] X + [1] Y + [1] Z + [2] 171.50/60.12 = [__(X, __(Y, Z))] 171.50/60.12 171.50/60.12 [__(nil(), X)] = [1] X + [3] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [nil()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__nil()] 171.50/60.12 171.50/60.12 [and(tt(), X)] = [1] X + [3] 171.50/60.12 > [1] X + [2] 171.50/60.12 = [activate(X)] 171.50/60.12 171.50/60.12 [activate(X)] = [1] X + [2] 171.50/60.12 > [1] X + [0] 171.50/60.12 = [X] 171.50/60.12 171.50/60.12 [activate(n__nil())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [nil()] 171.50/60.12 171.50/60.12 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [3] 171.50/60.12 > [1] X1 + [1] X2 + [1] 171.50/60.12 = [__(X1, X2)] 171.50/60.12 171.50/60.12 [activate(n__isList(X))] = [1] X + [3] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [isList(X)] 171.50/60.12 171.50/60.12 [activate(n__isNeList(X))] = [1] X + [3] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [isNeList(X)] 171.50/60.12 171.50/60.12 [activate(n__isPal(X))] = [1] X + [3] 171.50/60.12 > [1] X + [2] 171.50/60.12 = [isPal(X)] 171.50/60.12 171.50/60.12 [activate(n__a())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [a()] 171.50/60.12 171.50/60.12 [activate(n__e())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [e()] 171.50/60.12 171.50/60.12 [activate(n__i())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [i()] 171.50/60.12 171.50/60.12 [activate(n__o())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [o()] 171.50/60.12 171.50/60.12 [activate(n__u())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [u()] 171.50/60.12 171.50/60.12 [isList(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isNeList(activate(V))] 171.50/60.12 171.50/60.12 [isList(X)] = [1] X + [1] 171.50/60.12 >= [1] X + [1] 171.50/60.12 = [n__isList(X)] 171.50/60.12 171.50/60.12 [isList(n__nil())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNeList(X)] = [1] X + [1] 171.50/60.12 >= [1] X + [1] 171.50/60.12 = [n__isNeList(X)] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.12 171.50/60.12 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.12 ? [1] V1 + [1] V2 + [7] 171.50/60.12 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.12 171.50/60.12 [isQid(n__a())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__e())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__i())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__o())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isQid(n__u())] = [2] 171.50/60.12 >= [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [isNePal(V)] = [1] V + [1] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isQid(activate(V))] 171.50/60.12 171.50/60.12 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [3] 171.50/60.12 ? [1] I + [1] P + [7] 171.50/60.12 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.12 171.50/60.12 [isPal(V)] = [1] V + [2] 171.50/60.12 ? [1] V + [3] 171.50/60.12 = [isNePal(activate(V))] 171.50/60.12 171.50/60.12 [isPal(X)] = [1] X + [2] 171.50/60.12 > [1] X + [1] 171.50/60.12 = [n__isPal(X)] 171.50/60.12 171.50/60.12 [isPal(n__nil())] = [3] 171.50/60.12 > [2] 171.50/60.12 = [tt()] 171.50/60.12 171.50/60.12 [a()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__a()] 171.50/60.12 171.50/60.12 [e()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__e()] 171.50/60.12 171.50/60.12 [i()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__i()] 171.50/60.12 171.50/60.12 [o()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__o()] 171.50/60.12 171.50/60.12 [u()] = [2] 171.50/60.12 > [1] 171.50/60.12 = [n__u()] 171.50/60.12 171.50/60.12 171.50/60.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.50/60.12 171.50/60.12 We are left with following problem, upon which TcT provides the 171.50/60.12 certificate YES(O(1),O(n^2)). 171.50/60.12 171.50/60.12 Strict Trs: 171.50/60.12 { __(X1, X2) -> n____(X1, X2) 171.50/60.12 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.12 , isList(V) -> isNeList(activate(V)) 171.50/60.12 , isList(X) -> n__isList(X) 171.50/60.12 , isList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.12 , isNeList(V) -> isQid(activate(V)) 171.50/60.12 , isNeList(X) -> n__isNeList(X) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.12 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.12 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isNePal(V) -> isQid(activate(V)) 171.50/60.13 , isNePal(n____(I, __(P, I))) -> 171.50/60.13 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.13 , isPal(V) -> isNePal(activate(V)) } 171.50/60.13 Weak Trs: 171.50/60.13 { __(X, nil()) -> X 171.50/60.13 , __(nil(), X) -> X 171.50/60.13 , nil() -> n__nil() 171.50/60.13 , and(tt(), X) -> activate(X) 171.50/60.13 , activate(X) -> X 171.50/60.13 , activate(n__nil()) -> nil() 171.50/60.13 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.13 , activate(n__isList(X)) -> isList(X) 171.50/60.13 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.13 , activate(n__isPal(X)) -> isPal(X) 171.50/60.13 , activate(n__a()) -> a() 171.50/60.13 , activate(n__e()) -> e() 171.50/60.13 , activate(n__i()) -> i() 171.50/60.13 , activate(n__o()) -> o() 171.50/60.13 , activate(n__u()) -> u() 171.50/60.13 , isList(n__nil()) -> tt() 171.50/60.13 , isQid(n__a()) -> tt() 171.50/60.13 , isQid(n__e()) -> tt() 171.50/60.13 , isQid(n__i()) -> tt() 171.50/60.13 , isQid(n__o()) -> tt() 171.50/60.13 , isQid(n__u()) -> tt() 171.50/60.13 , isPal(X) -> n__isPal(X) 171.50/60.13 , isPal(n__nil()) -> tt() 171.50/60.13 , a() -> n__a() 171.50/60.13 , e() -> n__e() 171.50/60.13 , i() -> n__i() 171.50/60.13 , o() -> n__o() 171.50/60.13 , u() -> n__u() } 171.50/60.13 Obligation: 171.50/60.13 derivational complexity 171.50/60.13 Answer: 171.50/60.13 YES(O(1),O(n^2)) 171.50/60.13 171.50/60.13 The weightgap principle applies (using the following nonconstant 171.50/60.13 growth matrix-interpretation) 171.50/60.13 171.50/60.13 TcT has computed the following triangular matrix interpretation. 171.50/60.13 Note that the diagonal of the component-wise maxima of 171.50/60.13 interpretation-entries contains no more than 1 non-zero entries. 171.50/60.13 171.50/60.13 [__](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [nil] = [2] 171.50/60.13 171.50/60.13 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [tt] = [2] 171.50/60.13 171.50/60.13 [activate](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isNeList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__nil] = [2] 171.50/60.13 171.50/60.13 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [n__isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isQid](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isNeList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isNePal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isPal](x1) = [1] x1 + [1] 171.50/60.13 171.50/60.13 [isPal](x1) = [1] x1 + [1] 171.50/60.13 171.50/60.13 [n__a] = [2] 171.50/60.13 171.50/60.13 [n__e] = [2] 171.50/60.13 171.50/60.13 [n__i] = [2] 171.50/60.13 171.50/60.13 [n__o] = [2] 171.50/60.13 171.50/60.13 [n__u] = [2] 171.50/60.13 171.50/60.13 [a] = [2] 171.50/60.13 171.50/60.13 [e] = [2] 171.50/60.13 171.50/60.13 [i] = [2] 171.50/60.13 171.50/60.13 [o] = [2] 171.50/60.13 171.50/60.13 [u] = [2] 171.50/60.13 171.50/60.13 The order satisfies the following ordering constraints: 171.50/60.13 171.50/60.13 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 171.50/60.13 >= [1] X1 + [1] X2 + [0] 171.50/60.13 = [n____(X1, X2)] 171.50/60.13 171.50/60.13 [__(X, nil())] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 171.50/60.13 >= [1] X + [1] Y + [1] Z + [0] 171.50/60.13 = [__(X, __(Y, Z))] 171.50/60.13 171.50/60.13 [__(nil(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [nil()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__nil()] 171.50/60.13 171.50/60.13 [and(tt(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [activate(X)] 171.50/60.13 171.50/60.13 [activate(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [activate(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [nil()] 171.50/60.13 171.50/60.13 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 171.50/60.13 >= [1] X1 + [1] X2 + [0] 171.50/60.13 = [__(X1, X2)] 171.50/60.13 171.50/60.13 [activate(n__isList(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isList(X)] 171.50/60.13 171.50/60.13 [activate(n__isNeList(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isNeList(X)] 171.50/60.13 171.50/60.13 [activate(n__isPal(X))] = [1] X + [1] 171.50/60.13 >= [1] X + [1] 171.50/60.13 = [isPal(X)] 171.50/60.13 171.50/60.13 [activate(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [a()] 171.50/60.13 171.50/60.13 [activate(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [e()] 171.50/60.13 171.50/60.13 [activate(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [i()] 171.50/60.13 171.50/60.13 [activate(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [o()] 171.50/60.13 171.50/60.13 [activate(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [u()] 171.50/60.13 171.50/60.13 [isList(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isNeList(activate(V))] 171.50/60.13 171.50/60.13 [isList(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isList(X)] 171.50/60.13 171.50/60.13 [isList(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.13 >= [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNeList(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isNeList(X)] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.13 >= [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.13 >= [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isQid(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isNePal(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [0] 171.50/60.13 ? [1] I + [1] P + [1] 171.50/60.13 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.13 171.50/60.13 [isPal(V)] = [1] V + [1] 171.50/60.13 > [1] V + [0] 171.50/60.13 = [isNePal(activate(V))] 171.50/60.13 171.50/60.13 [isPal(X)] = [1] X + [1] 171.50/60.13 >= [1] X + [1] 171.50/60.13 = [n__isPal(X)] 171.50/60.13 171.50/60.13 [isPal(n__nil())] = [3] 171.50/60.13 > [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [a()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__a()] 171.50/60.13 171.50/60.13 [e()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__e()] 171.50/60.13 171.50/60.13 [i()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__i()] 171.50/60.13 171.50/60.13 [o()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__o()] 171.50/60.13 171.50/60.13 [u()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__u()] 171.50/60.13 171.50/60.13 171.50/60.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.50/60.13 171.50/60.13 We are left with following problem, upon which TcT provides the 171.50/60.13 certificate YES(O(1),O(n^2)). 171.50/60.13 171.50/60.13 Strict Trs: 171.50/60.13 { __(X1, X2) -> n____(X1, X2) 171.50/60.13 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.13 , isList(V) -> isNeList(activate(V)) 171.50/60.13 , isList(X) -> n__isList(X) 171.50/60.13 , isList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isNeList(V) -> isQid(activate(V)) 171.50/60.13 , isNeList(X) -> n__isNeList(X) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isNePal(V) -> isQid(activate(V)) 171.50/60.13 , isNePal(n____(I, __(P, I))) -> 171.50/60.13 and(isQid(activate(I)), n__isPal(activate(P))) } 171.50/60.13 Weak Trs: 171.50/60.13 { __(X, nil()) -> X 171.50/60.13 , __(nil(), X) -> X 171.50/60.13 , nil() -> n__nil() 171.50/60.13 , and(tt(), X) -> activate(X) 171.50/60.13 , activate(X) -> X 171.50/60.13 , activate(n__nil()) -> nil() 171.50/60.13 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.13 , activate(n__isList(X)) -> isList(X) 171.50/60.13 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.13 , activate(n__isPal(X)) -> isPal(X) 171.50/60.13 , activate(n__a()) -> a() 171.50/60.13 , activate(n__e()) -> e() 171.50/60.13 , activate(n__i()) -> i() 171.50/60.13 , activate(n__o()) -> o() 171.50/60.13 , activate(n__u()) -> u() 171.50/60.13 , isList(n__nil()) -> tt() 171.50/60.13 , isQid(n__a()) -> tt() 171.50/60.13 , isQid(n__e()) -> tt() 171.50/60.13 , isQid(n__i()) -> tt() 171.50/60.13 , isQid(n__o()) -> tt() 171.50/60.13 , isQid(n__u()) -> tt() 171.50/60.13 , isPal(V) -> isNePal(activate(V)) 171.50/60.13 , isPal(X) -> n__isPal(X) 171.50/60.13 , isPal(n__nil()) -> tt() 171.50/60.13 , a() -> n__a() 171.50/60.13 , e() -> n__e() 171.50/60.13 , i() -> n__i() 171.50/60.13 , o() -> n__o() 171.50/60.13 , u() -> n__u() } 171.50/60.13 Obligation: 171.50/60.13 derivational complexity 171.50/60.13 Answer: 171.50/60.13 YES(O(1),O(n^2)) 171.50/60.13 171.50/60.13 The weightgap principle applies (using the following nonconstant 171.50/60.13 growth matrix-interpretation) 171.50/60.13 171.50/60.13 TcT has computed the following triangular matrix interpretation. 171.50/60.13 Note that the diagonal of the component-wise maxima of 171.50/60.13 interpretation-entries contains no more than 1 non-zero entries. 171.50/60.13 171.50/60.13 [__](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [nil] = [2] 171.50/60.13 171.50/60.13 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [tt] = [2] 171.50/60.13 171.50/60.13 [activate](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isNeList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__nil] = [2] 171.50/60.13 171.50/60.13 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 171.50/60.13 171.50/60.13 [n__isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isQid](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isNeList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isNePal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isPal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isPal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__a] = [2] 171.50/60.13 171.50/60.13 [n__e] = [2] 171.50/60.13 171.50/60.13 [n__i] = [2] 171.50/60.13 171.50/60.13 [n__o] = [2] 171.50/60.13 171.50/60.13 [n__u] = [2] 171.50/60.13 171.50/60.13 [a] = [2] 171.50/60.13 171.50/60.13 [e] = [2] 171.50/60.13 171.50/60.13 [i] = [2] 171.50/60.13 171.50/60.13 [o] = [2] 171.50/60.13 171.50/60.13 [u] = [2] 171.50/60.13 171.50/60.13 The order satisfies the following ordering constraints: 171.50/60.13 171.50/60.13 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 171.50/60.13 ? [1] X1 + [1] X2 + [1] 171.50/60.13 = [n____(X1, X2)] 171.50/60.13 171.50/60.13 [__(X, nil())] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 171.50/60.13 >= [1] X + [1] Y + [1] Z + [0] 171.50/60.13 = [__(X, __(Y, Z))] 171.50/60.13 171.50/60.13 [__(nil(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [nil()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__nil()] 171.50/60.13 171.50/60.13 [and(tt(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [activate(X)] 171.50/60.13 171.50/60.13 [activate(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [activate(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [nil()] 171.50/60.13 171.50/60.13 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1] 171.50/60.13 > [1] X1 + [1] X2 + [0] 171.50/60.13 = [__(X1, X2)] 171.50/60.13 171.50/60.13 [activate(n__isList(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isList(X)] 171.50/60.13 171.50/60.13 [activate(n__isNeList(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isNeList(X)] 171.50/60.13 171.50/60.13 [activate(n__isPal(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isPal(X)] 171.50/60.13 171.50/60.13 [activate(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [a()] 171.50/60.13 171.50/60.13 [activate(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [e()] 171.50/60.13 171.50/60.13 [activate(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [i()] 171.50/60.13 171.50/60.13 [activate(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [o()] 171.50/60.13 171.50/60.13 [activate(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [u()] 171.50/60.13 171.50/60.13 [isList(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isNeList(activate(V))] 171.50/60.13 171.50/60.13 [isList(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isList(X)] 171.50/60.13 171.50/60.13 [isList(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 171.50/60.13 > [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNeList(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isNeList(X)] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 171.50/60.13 > [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 171.50/60.13 > [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isQid(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isNePal(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [1] 171.50/60.13 > [1] I + [1] P + [0] 171.50/60.13 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.13 171.50/60.13 [isPal(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isNePal(activate(V))] 171.50/60.13 171.50/60.13 [isPal(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isPal(X)] 171.50/60.13 171.50/60.13 [isPal(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [a()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__a()] 171.50/60.13 171.50/60.13 [e()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__e()] 171.50/60.13 171.50/60.13 [i()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__i()] 171.50/60.13 171.50/60.13 [o()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__o()] 171.50/60.13 171.50/60.13 [u()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__u()] 171.50/60.13 171.50/60.13 171.50/60.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.50/60.13 171.50/60.13 We are left with following problem, upon which TcT provides the 171.50/60.13 certificate YES(O(1),O(n^2)). 171.50/60.13 171.50/60.13 Strict Trs: 171.50/60.13 { __(X1, X2) -> n____(X1, X2) 171.50/60.13 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.13 , isList(V) -> isNeList(activate(V)) 171.50/60.13 , isList(X) -> n__isList(X) 171.50/60.13 , isNeList(V) -> isQid(activate(V)) 171.50/60.13 , isNeList(X) -> n__isNeList(X) 171.50/60.13 , isNePal(V) -> isQid(activate(V)) } 171.50/60.13 Weak Trs: 171.50/60.13 { __(X, nil()) -> X 171.50/60.13 , __(nil(), X) -> X 171.50/60.13 , nil() -> n__nil() 171.50/60.13 , and(tt(), X) -> activate(X) 171.50/60.13 , activate(X) -> X 171.50/60.13 , activate(n__nil()) -> nil() 171.50/60.13 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.13 , activate(n__isList(X)) -> isList(X) 171.50/60.13 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.13 , activate(n__isPal(X)) -> isPal(X) 171.50/60.13 , activate(n__a()) -> a() 171.50/60.13 , activate(n__e()) -> e() 171.50/60.13 , activate(n__i()) -> i() 171.50/60.13 , activate(n__o()) -> o() 171.50/60.13 , activate(n__u()) -> u() 171.50/60.13 , isList(n__nil()) -> tt() 171.50/60.13 , isList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isQid(n__a()) -> tt() 171.50/60.13 , isQid(n__e()) -> tt() 171.50/60.13 , isQid(n__i()) -> tt() 171.50/60.13 , isQid(n__o()) -> tt() 171.50/60.13 , isQid(n__u()) -> tt() 171.50/60.13 , isNePal(n____(I, __(P, I))) -> 171.50/60.13 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.13 , isPal(V) -> isNePal(activate(V)) 171.50/60.13 , isPal(X) -> n__isPal(X) 171.50/60.13 , isPal(n__nil()) -> tt() 171.50/60.13 , a() -> n__a() 171.50/60.13 , e() -> n__e() 171.50/60.13 , i() -> n__i() 171.50/60.13 , o() -> n__o() 171.50/60.13 , u() -> n__u() } 171.50/60.13 Obligation: 171.50/60.13 derivational complexity 171.50/60.13 Answer: 171.50/60.13 YES(O(1),O(n^2)) 171.50/60.13 171.50/60.13 The weightgap principle applies (using the following nonconstant 171.50/60.13 growth matrix-interpretation) 171.50/60.13 171.50/60.13 TcT has computed the following triangular matrix interpretation. 171.50/60.13 Note that the diagonal of the component-wise maxima of 171.50/60.13 interpretation-entries contains no more than 1 non-zero entries. 171.50/60.13 171.50/60.13 [__](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [nil] = [2] 171.50/60.13 171.50/60.13 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [tt] = [2] 171.50/60.13 171.50/60.13 [activate](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isNeList](x1) = [1] x1 + [1] 171.50/60.13 171.50/60.13 [n__nil] = [2] 171.50/60.13 171.50/60.13 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.13 171.50/60.13 [n__isList](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isQid](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isNeList](x1) = [1] x1 + [1] 171.50/60.13 171.50/60.13 [isNePal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__isPal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [isPal](x1) = [1] x1 + [0] 171.50/60.13 171.50/60.13 [n__a] = [2] 171.50/60.13 171.50/60.13 [n__e] = [2] 171.50/60.13 171.50/60.13 [n__i] = [2] 171.50/60.13 171.50/60.13 [n__o] = [2] 171.50/60.13 171.50/60.13 [n__u] = [2] 171.50/60.13 171.50/60.13 [a] = [2] 171.50/60.13 171.50/60.13 [e] = [2] 171.50/60.13 171.50/60.13 [i] = [2] 171.50/60.13 171.50/60.13 [o] = [2] 171.50/60.13 171.50/60.13 [u] = [2] 171.50/60.13 171.50/60.13 The order satisfies the following ordering constraints: 171.50/60.13 171.50/60.13 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 171.50/60.13 >= [1] X1 + [1] X2 + [0] 171.50/60.13 = [n____(X1, X2)] 171.50/60.13 171.50/60.13 [__(X, nil())] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 171.50/60.13 >= [1] X + [1] Y + [1] Z + [0] 171.50/60.13 = [__(X, __(Y, Z))] 171.50/60.13 171.50/60.13 [__(nil(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [nil()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__nil()] 171.50/60.13 171.50/60.13 [and(tt(), X)] = [1] X + [2] 171.50/60.13 > [1] X + [0] 171.50/60.13 = [activate(X)] 171.50/60.13 171.50/60.13 [activate(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [X] 171.50/60.13 171.50/60.13 [activate(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [nil()] 171.50/60.13 171.50/60.13 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 171.50/60.13 >= [1] X1 + [1] X2 + [0] 171.50/60.13 = [__(X1, X2)] 171.50/60.13 171.50/60.13 [activate(n__isList(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isList(X)] 171.50/60.13 171.50/60.13 [activate(n__isNeList(X))] = [1] X + [1] 171.50/60.13 >= [1] X + [1] 171.50/60.13 = [isNeList(X)] 171.50/60.13 171.50/60.13 [activate(n__isPal(X))] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [isPal(X)] 171.50/60.13 171.50/60.13 [activate(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [a()] 171.50/60.13 171.50/60.13 [activate(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [e()] 171.50/60.13 171.50/60.13 [activate(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [i()] 171.50/60.13 171.50/60.13 [activate(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [o()] 171.50/60.13 171.50/60.13 [activate(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [u()] 171.50/60.13 171.50/60.13 [isList(V)] = [1] V + [0] 171.50/60.13 ? [1] V + [1] 171.50/60.13 = [isNeList(activate(V))] 171.50/60.13 171.50/60.13 [isList(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isList(X)] 171.50/60.13 171.50/60.13 [isList(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.13 >= [1] V1 + [1] V2 + [0] 171.50/60.13 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(V)] = [1] V + [1] 171.50/60.13 > [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNeList(X)] = [1] X + [1] 171.50/60.13 >= [1] X + [1] 171.50/60.13 = [n__isNeList(X)] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 171.50/60.13 >= [1] V1 + [1] V2 + [1] 171.50/60.13 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.13 171.50/60.13 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 171.50/60.13 >= [1] V1 + [1] V2 + [1] 171.50/60.13 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.13 171.50/60.13 [isQid(n__a())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__e())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__i())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__o())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isQid(n__u())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [isNePal(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isQid(activate(V))] 171.50/60.13 171.50/60.13 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [0] 171.50/60.13 >= [1] I + [1] P + [0] 171.50/60.13 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.13 171.50/60.13 [isPal(V)] = [1] V + [0] 171.50/60.13 >= [1] V + [0] 171.50/60.13 = [isNePal(activate(V))] 171.50/60.13 171.50/60.13 [isPal(X)] = [1] X + [0] 171.50/60.13 >= [1] X + [0] 171.50/60.13 = [n__isPal(X)] 171.50/60.13 171.50/60.13 [isPal(n__nil())] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [tt()] 171.50/60.13 171.50/60.13 [a()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__a()] 171.50/60.13 171.50/60.13 [e()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__e()] 171.50/60.13 171.50/60.13 [i()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__i()] 171.50/60.13 171.50/60.13 [o()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__o()] 171.50/60.13 171.50/60.13 [u()] = [2] 171.50/60.13 >= [2] 171.50/60.13 = [n__u()] 171.50/60.13 171.50/60.13 171.50/60.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.50/60.13 171.50/60.13 We are left with following problem, upon which TcT provides the 171.50/60.13 certificate YES(O(1),O(n^2)). 171.50/60.13 171.50/60.13 Strict Trs: 171.50/60.13 { __(X1, X2) -> n____(X1, X2) 171.50/60.13 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.13 , isList(V) -> isNeList(activate(V)) 171.50/60.13 , isList(X) -> n__isList(X) 171.50/60.13 , isNeList(X) -> n__isNeList(X) 171.50/60.13 , isNePal(V) -> isQid(activate(V)) } 171.50/60.13 Weak Trs: 171.50/60.13 { __(X, nil()) -> X 171.50/60.13 , __(nil(), X) -> X 171.50/60.13 , nil() -> n__nil() 171.50/60.13 , and(tt(), X) -> activate(X) 171.50/60.13 , activate(X) -> X 171.50/60.13 , activate(n__nil()) -> nil() 171.50/60.13 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.13 , activate(n__isList(X)) -> isList(X) 171.50/60.13 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.13 , activate(n__isPal(X)) -> isPal(X) 171.50/60.13 , activate(n__a()) -> a() 171.50/60.13 , activate(n__e()) -> e() 171.50/60.13 , activate(n__i()) -> i() 171.50/60.13 , activate(n__o()) -> o() 171.50/60.13 , activate(n__u()) -> u() 171.50/60.13 , isList(n__nil()) -> tt() 171.50/60.13 , isList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isNeList(V) -> isQid(activate(V)) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.13 , isNeList(n____(V1, V2)) -> 171.50/60.13 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.13 , isQid(n__a()) -> tt() 171.50/60.13 , isQid(n__e()) -> tt() 171.50/60.13 , isQid(n__i()) -> tt() 171.50/60.13 , isQid(n__o()) -> tt() 171.50/60.13 , isQid(n__u()) -> tt() 171.50/60.13 , isNePal(n____(I, __(P, I))) -> 171.50/60.13 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.13 , isPal(V) -> isNePal(activate(V)) 171.50/60.13 , isPal(X) -> n__isPal(X) 171.50/60.13 , isPal(n__nil()) -> tt() 171.50/60.13 , a() -> n__a() 171.50/60.13 , e() -> n__e() 171.50/60.13 , i() -> n__i() 171.50/60.14 , o() -> n__o() 171.50/60.14 , u() -> n__u() } 171.50/60.14 Obligation: 171.50/60.14 derivational complexity 171.50/60.14 Answer: 171.50/60.14 YES(O(1),O(n^2)) 171.50/60.14 171.50/60.14 We use the processor 'matrix interpretation of dimension 1' to 171.50/60.14 orient following rules strictly. 171.50/60.14 171.50/60.14 Trs: { isNePal(V) -> isQid(activate(V)) } 171.50/60.14 171.50/60.14 The induced complexity on above rules (modulo remaining rules) is 171.50/60.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 171.50/60.14 component(s). 171.50/60.14 171.50/60.14 Sub-proof: 171.50/60.14 ---------- 171.50/60.14 TcT has computed the following triangular matrix interpretation. 171.50/60.14 171.50/60.14 [__](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.14 171.50/60.14 [nil] = [2] 171.50/60.14 171.50/60.14 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.14 171.50/60.14 [tt] = [2] 171.50/60.14 171.50/60.14 [activate](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isNeList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__nil] = [2] 171.50/60.14 171.50/60.14 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.14 171.50/60.14 [n__isList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isQid](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__isNeList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isNePal](x1) = [1] x1 + [1] 171.50/60.14 171.50/60.14 [n__isPal](x1) = [1] x1 + [1] 171.50/60.14 171.50/60.14 [isPal](x1) = [1] x1 + [1] 171.50/60.14 171.50/60.14 [n__a] = [2] 171.50/60.14 171.50/60.14 [n__e] = [2] 171.50/60.14 171.50/60.14 [n__i] = [2] 171.50/60.14 171.50/60.14 [n__o] = [2] 171.50/60.14 171.50/60.14 [n__u] = [2] 171.50/60.14 171.50/60.14 [a] = [2] 171.50/60.14 171.50/60.14 [e] = [2] 171.50/60.14 171.50/60.14 [i] = [2] 171.50/60.14 171.50/60.14 [o] = [2] 171.50/60.14 171.50/60.14 [u] = [2] 171.50/60.14 171.50/60.14 The order satisfies the following ordering constraints: 171.50/60.14 171.50/60.14 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 171.50/60.14 >= [1] X1 + [1] X2 + [0] 171.50/60.14 = [n____(X1, X2)] 171.50/60.14 171.50/60.14 [__(X, nil())] = [1] X + [2] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 171.50/60.14 >= [1] X + [1] Y + [1] Z + [0] 171.50/60.14 = [__(X, __(Y, Z))] 171.50/60.14 171.50/60.14 [__(nil(), X)] = [1] X + [2] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [nil()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__nil()] 171.50/60.14 171.50/60.14 [and(tt(), X)] = [1] X + [2] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [activate(X)] 171.50/60.14 171.50/60.14 [activate(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [activate(n__nil())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [nil()] 171.50/60.14 171.50/60.14 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 171.50/60.14 >= [1] X1 + [1] X2 + [0] 171.50/60.14 = [__(X1, X2)] 171.50/60.14 171.50/60.14 [activate(n__isList(X))] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [isList(X)] 171.50/60.14 171.50/60.14 [activate(n__isNeList(X))] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [isNeList(X)] 171.50/60.14 171.50/60.14 [activate(n__isPal(X))] = [1] X + [1] 171.50/60.14 >= [1] X + [1] 171.50/60.14 = [isPal(X)] 171.50/60.14 171.50/60.14 [activate(n__a())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [a()] 171.50/60.14 171.50/60.14 [activate(n__e())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [e()] 171.50/60.14 171.50/60.14 [activate(n__i())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [i()] 171.50/60.14 171.50/60.14 [activate(n__o())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [o()] 171.50/60.14 171.50/60.14 [activate(n__u())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [u()] 171.50/60.14 171.50/60.14 [isList(V)] = [1] V + [0] 171.50/60.14 >= [1] V + [0] 171.50/60.14 = [isNeList(activate(V))] 171.50/60.14 171.50/60.14 [isList(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [n__isList(X)] 171.50/60.14 171.50/60.14 [isList(n__nil())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.14 >= [1] V1 + [1] V2 + [0] 171.50/60.14 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(V)] = [1] V + [0] 171.50/60.14 >= [1] V + [0] 171.50/60.14 = [isQid(activate(V))] 171.50/60.14 171.50/60.14 [isNeList(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [n__isNeList(X)] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.14 >= [1] V1 + [1] V2 + [0] 171.50/60.14 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 171.50/60.14 >= [1] V1 + [1] V2 + [0] 171.50/60.14 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isQid(n__a())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__e())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__i())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__o())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__u())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isNePal(V)] = [1] V + [1] 171.50/60.14 > [1] V + [0] 171.50/60.14 = [isQid(activate(V))] 171.50/60.14 171.50/60.14 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [1] 171.50/60.14 >= [1] I + [1] P + [1] 171.50/60.14 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.14 171.50/60.14 [isPal(V)] = [1] V + [1] 171.50/60.14 >= [1] V + [1] 171.50/60.14 = [isNePal(activate(V))] 171.50/60.14 171.50/60.14 [isPal(X)] = [1] X + [1] 171.50/60.14 >= [1] X + [1] 171.50/60.14 = [n__isPal(X)] 171.50/60.14 171.50/60.14 [isPal(n__nil())] = [3] 171.50/60.14 > [2] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [a()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__a()] 171.50/60.14 171.50/60.14 [e()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__e()] 171.50/60.14 171.50/60.14 [i()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__i()] 171.50/60.14 171.50/60.14 [o()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__o()] 171.50/60.14 171.50/60.14 [u()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__u()] 171.50/60.14 171.50/60.14 171.50/60.14 We return to the main proof. 171.50/60.14 171.50/60.14 We are left with following problem, upon which TcT provides the 171.50/60.14 certificate YES(O(1),O(n^2)). 171.50/60.14 171.50/60.14 Strict Trs: 171.50/60.14 { __(X1, X2) -> n____(X1, X2) 171.50/60.14 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.14 , isList(V) -> isNeList(activate(V)) 171.50/60.14 , isList(X) -> n__isList(X) 171.50/60.14 , isNeList(X) -> n__isNeList(X) } 171.50/60.14 Weak Trs: 171.50/60.14 { __(X, nil()) -> X 171.50/60.14 , __(nil(), X) -> X 171.50/60.14 , nil() -> n__nil() 171.50/60.14 , and(tt(), X) -> activate(X) 171.50/60.14 , activate(X) -> X 171.50/60.14 , activate(n__nil()) -> nil() 171.50/60.14 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.14 , activate(n__isList(X)) -> isList(X) 171.50/60.14 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.14 , activate(n__isPal(X)) -> isPal(X) 171.50/60.14 , activate(n__a()) -> a() 171.50/60.14 , activate(n__e()) -> e() 171.50/60.14 , activate(n__i()) -> i() 171.50/60.14 , activate(n__o()) -> o() 171.50/60.14 , activate(n__u()) -> u() 171.50/60.14 , isList(n__nil()) -> tt() 171.50/60.14 , isList(n____(V1, V2)) -> 171.50/60.14 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.14 , isNeList(V) -> isQid(activate(V)) 171.50/60.14 , isNeList(n____(V1, V2)) -> 171.50/60.14 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.14 , isNeList(n____(V1, V2)) -> 171.50/60.14 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.14 , isQid(n__a()) -> tt() 171.50/60.14 , isQid(n__e()) -> tt() 171.50/60.14 , isQid(n__i()) -> tt() 171.50/60.14 , isQid(n__o()) -> tt() 171.50/60.14 , isQid(n__u()) -> tt() 171.50/60.14 , isNePal(V) -> isQid(activate(V)) 171.50/60.14 , isNePal(n____(I, __(P, I))) -> 171.50/60.14 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.14 , isPal(V) -> isNePal(activate(V)) 171.50/60.14 , isPal(X) -> n__isPal(X) 171.50/60.14 , isPal(n__nil()) -> tt() 171.50/60.14 , a() -> n__a() 171.50/60.14 , e() -> n__e() 171.50/60.14 , i() -> n__i() 171.50/60.14 , o() -> n__o() 171.50/60.14 , u() -> n__u() } 171.50/60.14 Obligation: 171.50/60.14 derivational complexity 171.50/60.14 Answer: 171.50/60.14 YES(O(1),O(n^2)) 171.50/60.14 171.50/60.14 We use the processor 'matrix interpretation of dimension 1' to 171.50/60.14 orient following rules strictly. 171.50/60.14 171.50/60.14 Trs: { isList(V) -> isNeList(activate(V)) } 171.50/60.14 171.50/60.14 The induced complexity on above rules (modulo remaining rules) is 171.50/60.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 171.50/60.14 component(s). 171.50/60.14 171.50/60.14 Sub-proof: 171.50/60.14 ---------- 171.50/60.14 TcT has computed the following triangular matrix interpretation. 171.50/60.14 171.50/60.14 [__](x1, x2) = [1] x1 + [1] x2 + [2] 171.50/60.14 171.50/60.14 [nil] = [1] 171.50/60.14 171.50/60.14 [and](x1, x2) = [1] x1 + [1] x2 + [0] 171.50/60.14 171.50/60.14 [tt] = [1] 171.50/60.14 171.50/60.14 [activate](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isList](x1) = [1] x1 + [2] 171.50/60.14 171.50/60.14 [isNeList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__nil] = [1] 171.50/60.14 171.50/60.14 [n____](x1, x2) = [1] x1 + [1] x2 + [2] 171.50/60.14 171.50/60.14 [n__isList](x1) = [1] x1 + [2] 171.50/60.14 171.50/60.14 [isQid](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__isNeList](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isNePal](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__isPal](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [isPal](x1) = [1] x1 + [0] 171.50/60.14 171.50/60.14 [n__a] = [2] 171.50/60.14 171.50/60.14 [n__e] = [2] 171.50/60.14 171.50/60.14 [n__i] = [2] 171.50/60.14 171.50/60.14 [n__o] = [2] 171.50/60.14 171.50/60.14 [n__u] = [2] 171.50/60.14 171.50/60.14 [a] = [2] 171.50/60.14 171.50/60.14 [e] = [2] 171.50/60.14 171.50/60.14 [i] = [2] 171.50/60.14 171.50/60.14 [o] = [2] 171.50/60.14 171.50/60.14 [u] = [2] 171.50/60.14 171.50/60.14 The order satisfies the following ordering constraints: 171.50/60.14 171.50/60.14 [__(X1, X2)] = [1] X1 + [1] X2 + [2] 171.50/60.14 >= [1] X1 + [1] X2 + [2] 171.50/60.14 = [n____(X1, X2)] 171.50/60.14 171.50/60.14 [__(X, nil())] = [1] X + [3] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [4] 171.50/60.14 >= [1] X + [1] Y + [1] Z + [4] 171.50/60.14 = [__(X, __(Y, Z))] 171.50/60.14 171.50/60.14 [__(nil(), X)] = [1] X + [3] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [nil()] = [1] 171.50/60.14 >= [1] 171.50/60.14 = [n__nil()] 171.50/60.14 171.50/60.14 [and(tt(), X)] = [1] X + [1] 171.50/60.14 > [1] X + [0] 171.50/60.14 = [activate(X)] 171.50/60.14 171.50/60.14 [activate(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [activate(n__nil())] = [1] 171.50/60.14 >= [1] 171.50/60.14 = [nil()] 171.50/60.14 171.50/60.14 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [2] 171.50/60.14 >= [1] X1 + [1] X2 + [2] 171.50/60.14 = [__(X1, X2)] 171.50/60.14 171.50/60.14 [activate(n__isList(X))] = [1] X + [2] 171.50/60.14 >= [1] X + [2] 171.50/60.14 = [isList(X)] 171.50/60.14 171.50/60.14 [activate(n__isNeList(X))] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [isNeList(X)] 171.50/60.14 171.50/60.14 [activate(n__isPal(X))] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [isPal(X)] 171.50/60.14 171.50/60.14 [activate(n__a())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [a()] 171.50/60.14 171.50/60.14 [activate(n__e())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [e()] 171.50/60.14 171.50/60.14 [activate(n__i())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [i()] 171.50/60.14 171.50/60.14 [activate(n__o())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [o()] 171.50/60.14 171.50/60.14 [activate(n__u())] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [u()] 171.50/60.14 171.50/60.14 [isList(V)] = [1] V + [2] 171.50/60.14 > [1] V + [0] 171.50/60.14 = [isNeList(activate(V))] 171.50/60.14 171.50/60.14 [isList(X)] = [1] X + [2] 171.50/60.14 >= [1] X + [2] 171.50/60.14 = [n__isList(X)] 171.50/60.14 171.50/60.14 [isList(n__nil())] = [3] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [4] 171.50/60.14 >= [1] V1 + [1] V2 + [4] 171.50/60.14 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(V)] = [1] V + [0] 171.50/60.14 >= [1] V + [0] 171.50/60.14 = [isQid(activate(V))] 171.50/60.14 171.50/60.14 [isNeList(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [n__isNeList(X)] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.14 >= [1] V1 + [1] V2 + [2] 171.50/60.14 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 171.50/60.14 >= [1] V1 + [1] V2 + [2] 171.50/60.14 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isQid(n__a())] = [2] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__e())] = [2] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__i())] = [2] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__o())] = [2] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isQid(n__u())] = [2] 171.50/60.14 > [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isNePal(V)] = [1] V + [0] 171.50/60.14 >= [1] V + [0] 171.50/60.14 = [isQid(activate(V))] 171.50/60.14 171.50/60.14 [isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4] 171.50/60.14 > [1] I + [1] P + [0] 171.50/60.14 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.14 171.50/60.14 [isPal(V)] = [1] V + [0] 171.50/60.14 >= [1] V + [0] 171.50/60.14 = [isNePal(activate(V))] 171.50/60.14 171.50/60.14 [isPal(X)] = [1] X + [0] 171.50/60.14 >= [1] X + [0] 171.50/60.14 = [n__isPal(X)] 171.50/60.14 171.50/60.14 [isPal(n__nil())] = [1] 171.50/60.14 >= [1] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [a()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__a()] 171.50/60.14 171.50/60.14 [e()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__e()] 171.50/60.14 171.50/60.14 [i()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__i()] 171.50/60.14 171.50/60.14 [o()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__o()] 171.50/60.14 171.50/60.14 [u()] = [2] 171.50/60.14 >= [2] 171.50/60.14 = [n__u()] 171.50/60.14 171.50/60.14 171.50/60.14 We return to the main proof. 171.50/60.14 171.50/60.14 We are left with following problem, upon which TcT provides the 171.50/60.14 certificate YES(O(1),O(n^2)). 171.50/60.14 171.50/60.14 Strict Trs: 171.50/60.14 { __(X1, X2) -> n____(X1, X2) 171.50/60.14 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.14 , isList(X) -> n__isList(X) 171.50/60.14 , isNeList(X) -> n__isNeList(X) } 171.50/60.14 Weak Trs: 171.50/60.14 { __(X, nil()) -> X 171.50/60.14 , __(nil(), X) -> X 171.50/60.14 , nil() -> n__nil() 171.50/60.14 , and(tt(), X) -> activate(X) 171.50/60.14 , activate(X) -> X 171.50/60.14 , activate(n__nil()) -> nil() 171.50/60.14 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.14 , activate(n__isList(X)) -> isList(X) 171.50/60.14 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.14 , activate(n__isPal(X)) -> isPal(X) 171.50/60.14 , activate(n__a()) -> a() 171.50/60.14 , activate(n__e()) -> e() 171.50/60.14 , activate(n__i()) -> i() 171.50/60.14 , activate(n__o()) -> o() 171.50/60.14 , activate(n__u()) -> u() 171.50/60.14 , isList(V) -> isNeList(activate(V)) 171.50/60.14 , isList(n__nil()) -> tt() 171.50/60.14 , isList(n____(V1, V2)) -> 171.50/60.14 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.14 , isNeList(V) -> isQid(activate(V)) 171.50/60.14 , isNeList(n____(V1, V2)) -> 171.50/60.14 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.14 , isNeList(n____(V1, V2)) -> 171.50/60.14 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.14 , isQid(n__a()) -> tt() 171.50/60.14 , isQid(n__e()) -> tt() 171.50/60.14 , isQid(n__i()) -> tt() 171.50/60.14 , isQid(n__o()) -> tt() 171.50/60.14 , isQid(n__u()) -> tt() 171.50/60.14 , isNePal(V) -> isQid(activate(V)) 171.50/60.14 , isNePal(n____(I, __(P, I))) -> 171.50/60.14 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.14 , isPal(V) -> isNePal(activate(V)) 171.50/60.14 , isPal(X) -> n__isPal(X) 171.50/60.14 , isPal(n__nil()) -> tt() 171.50/60.14 , a() -> n__a() 171.50/60.14 , e() -> n__e() 171.50/60.14 , i() -> n__i() 171.50/60.14 , o() -> n__o() 171.50/60.14 , u() -> n__u() } 171.50/60.14 Obligation: 171.50/60.14 derivational complexity 171.50/60.14 Answer: 171.50/60.14 YES(O(1),O(n^2)) 171.50/60.14 171.50/60.14 We use the processor 'matrix interpretation of dimension 2' to 171.50/60.14 orient following rules strictly. 171.50/60.14 171.50/60.14 Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) } 171.50/60.14 171.50/60.14 The induced complexity on above rules (modulo remaining rules) is 171.50/60.14 YES(?,O(n^2)) . These rules are moved into the corresponding weak 171.50/60.14 component(s). 171.50/60.14 171.50/60.14 Sub-proof: 171.50/60.14 ---------- 171.50/60.14 TcT has computed the following triangular matrix interpretation. 171.50/60.14 171.50/60.14 [__](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 171.50/60.14 [nil] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 171.50/60.14 [0 0] [0 1] [0] 171.50/60.14 171.50/60.14 [tt] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [activate](x1) = [1 0] x1 + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 171.50/60.14 [isList](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [isNeList](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [n__nil] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [n____](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 171.50/60.14 [n__isList](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [isQid](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [n__isNeList](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [isNePal](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [n__isPal](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [isPal](x1) = [1 0] x1 + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 171.50/60.14 [n__a] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [n__e] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [n__i] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [n__o] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [n__u] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [a] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [e] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [i] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [o] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 [u] = [0] 171.50/60.14 [0] 171.50/60.14 171.50/60.14 The order satisfies the following ordering constraints: 171.50/60.14 171.50/60.14 [__(X1, X2)] = [1 1] X1 + [1 0] X2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 >= [1 1] X1 + [1 0] X2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 = [n____(X1, X2)] 171.50/60.14 171.50/60.14 [__(X, nil())] = [1 1] X + [0] 171.50/60.14 [0 1] [1] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [__(__(X, Y), Z)] = [1 2] X + [1 1] Y + [1 0] Z + [1] 171.50/60.14 [0 1] [0 1] [0 1] [2] 171.50/60.14 > [1 1] X + [1 1] Y + [1 0] Z + [0] 171.50/60.14 [0 1] [0 1] [0 1] [2] 171.50/60.14 = [__(X, __(Y, Z))] 171.50/60.14 171.50/60.14 [__(nil(), X)] = [1 0] X + [0] 171.50/60.14 [0 1] [1] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [nil()] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [n__nil()] 171.50/60.14 171.50/60.14 [and(tt(), X)] = [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 = [activate(X)] 171.50/60.14 171.50/60.14 [activate(X)] = [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 1] [0] 171.50/60.14 = [X] 171.50/60.14 171.50/60.14 [activate(n__nil())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [nil()] 171.50/60.14 171.50/60.14 [activate(n____(X1, X2))] = [1 1] X1 + [1 0] X2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 >= [1 1] X1 + [1 0] X2 + [0] 171.50/60.14 [0 1] [0 1] [1] 171.50/60.14 = [__(X1, X2)] 171.50/60.14 171.50/60.14 [activate(n__isList(X))] = [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [isList(X)] 171.50/60.14 171.50/60.14 [activate(n__isNeList(X))] = [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [isNeList(X)] 171.50/60.14 171.50/60.14 [activate(n__isPal(X))] = [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [isPal(X)] 171.50/60.14 171.50/60.14 [activate(n__a())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [a()] 171.50/60.14 171.50/60.14 [activate(n__e())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [e()] 171.50/60.14 171.50/60.14 [activate(n__i())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [i()] 171.50/60.14 171.50/60.14 [activate(n__o())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [o()] 171.50/60.14 171.50/60.14 [activate(n__u())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [u()] 171.50/60.14 171.50/60.14 [isList(V)] = [1 0] V + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] V + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [isNeList(activate(V))] 171.50/60.14 171.50/60.14 [isList(X)] = [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [n__isList(X)] 171.50/60.14 171.50/60.14 [isList(n__nil())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.14 [isList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 >= [1 0] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(V)] = [1 0] V + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] V + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [isQid(activate(V))] 171.50/60.14 171.50/60.14 [isNeList(X)] = [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 >= [1 0] X + [0] 171.50/60.14 [0 0] [0] 171.50/60.14 = [n__isNeList(X)] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 >= [1 0] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.14 171.50/60.14 [isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 >= [1 0] V1 + [1 0] V2 + [0] 171.50/60.14 [0 0] [0 0] [0] 171.50/60.14 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.14 171.50/60.14 [isQid(n__a())] = [0] 171.50/60.14 [0] 171.50/60.14 >= [0] 171.50/60.14 [0] 171.50/60.14 = [tt()] 171.50/60.14 171.50/60.15 [isQid(n__e())] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__i())] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__o())] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__u())] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isNePal(V)] = [1 0] V + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 0] V + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isQid(activate(V))] 171.50/60.15 171.50/60.15 [isNePal(n____(I, __(P, I)))] = [2 1] I + [1 1] P + [0] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 0] I + [1 0] P + [0] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.15 171.50/60.15 [isPal(V)] = [1 0] V + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 0] V + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isNePal(activate(V))] 171.50/60.15 171.50/60.15 [isPal(X)] = [1 0] X + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 0] X + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 = [n__isPal(X)] 171.50/60.15 171.50/60.15 [isPal(n__nil())] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [a()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__a()] 171.50/60.15 171.50/60.15 [e()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__e()] 171.50/60.15 171.50/60.15 [i()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__i()] 171.50/60.15 171.50/60.15 [o()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__o()] 171.50/60.15 171.50/60.15 [u()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__u()] 171.50/60.15 171.50/60.15 171.50/60.15 We return to the main proof. 171.50/60.15 171.50/60.15 We are left with following problem, upon which TcT provides the 171.50/60.15 certificate YES(O(1),O(n^2)). 171.50/60.15 171.50/60.15 Strict Trs: 171.50/60.15 { __(X1, X2) -> n____(X1, X2) 171.50/60.15 , isList(X) -> n__isList(X) 171.50/60.15 , isNeList(X) -> n__isNeList(X) } 171.50/60.15 Weak Trs: 171.50/60.15 { __(X, nil()) -> X 171.50/60.15 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.15 , __(nil(), X) -> X 171.50/60.15 , nil() -> n__nil() 171.50/60.15 , and(tt(), X) -> activate(X) 171.50/60.15 , activate(X) -> X 171.50/60.15 , activate(n__nil()) -> nil() 171.50/60.15 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.15 , activate(n__isList(X)) -> isList(X) 171.50/60.15 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.15 , activate(n__isPal(X)) -> isPal(X) 171.50/60.15 , activate(n__a()) -> a() 171.50/60.15 , activate(n__e()) -> e() 171.50/60.15 , activate(n__i()) -> i() 171.50/60.15 , activate(n__o()) -> o() 171.50/60.15 , activate(n__u()) -> u() 171.50/60.15 , isList(V) -> isNeList(activate(V)) 171.50/60.15 , isList(n__nil()) -> tt() 171.50/60.15 , isList(n____(V1, V2)) -> 171.50/60.15 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.15 , isNeList(V) -> isQid(activate(V)) 171.50/60.15 , isNeList(n____(V1, V2)) -> 171.50/60.15 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.15 , isNeList(n____(V1, V2)) -> 171.50/60.15 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.15 , isQid(n__a()) -> tt() 171.50/60.15 , isQid(n__e()) -> tt() 171.50/60.15 , isQid(n__i()) -> tt() 171.50/60.15 , isQid(n__o()) -> tt() 171.50/60.15 , isQid(n__u()) -> tt() 171.50/60.15 , isNePal(V) -> isQid(activate(V)) 171.50/60.15 , isNePal(n____(I, __(P, I))) -> 171.50/60.15 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.15 , isPal(V) -> isNePal(activate(V)) 171.50/60.15 , isPal(X) -> n__isPal(X) 171.50/60.15 , isPal(n__nil()) -> tt() 171.50/60.15 , a() -> n__a() 171.50/60.15 , e() -> n__e() 171.50/60.15 , i() -> n__i() 171.50/60.15 , o() -> n__o() 171.50/60.15 , u() -> n__u() } 171.50/60.15 Obligation: 171.50/60.15 derivational complexity 171.50/60.15 Answer: 171.50/60.15 YES(O(1),O(n^2)) 171.50/60.15 171.50/60.15 We use the processor 'matrix interpretation of dimension 2' to 171.50/60.15 orient following rules strictly. 171.50/60.15 171.50/60.15 Trs: 171.50/60.15 { __(X1, X2) -> n____(X1, X2) 171.50/60.15 , isNeList(X) -> n__isNeList(X) } 171.50/60.15 171.50/60.15 The induced complexity on above rules (modulo remaining rules) is 171.50/60.15 YES(?,O(n^2)) . These rules are moved into the corresponding weak 171.50/60.15 component(s). 171.50/60.15 171.50/60.15 Sub-proof: 171.50/60.15 ---------- 171.50/60.15 TcT has computed the following triangular matrix interpretation. 171.50/60.15 171.50/60.15 [__](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 171.50/60.15 [nil] = [0] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [and](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 171.50/60.15 [0 0] [0 1] [0] 171.50/60.15 171.50/60.15 [tt] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [activate](x1) = [1 0] x1 + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 171.50/60.15 [isList](x1) = [1 2] x1 + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isNeList](x1) = [1 2] x1 + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__nil] = [0] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [n____](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 171.50/60.15 [n__isList](x1) = [1 2] x1 + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isQid](x1) = [1 1] x1 + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__isNeList](x1) = [1 2] x1 + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isNePal](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [1] 171.50/60.15 171.50/60.15 [n__isPal](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [1] 171.50/60.15 171.50/60.15 [isPal](x1) = [1 1] x1 + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 171.50/60.15 [n__a] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n__e] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n__i] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n__o] = [0] 171.50/60.15 [1] 171.50/60.15 171.50/60.15 [n__u] = [0] 171.50/60.15 [1] 171.50/60.15 171.50/60.15 [a] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [e] = [2] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [i] = [2] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [o] = [1] 171.50/60.15 [1] 171.50/60.15 171.50/60.15 [u] = [1] 171.50/60.15 [1] 171.50/60.15 171.50/60.15 The order satisfies the following ordering constraints: 171.50/60.15 171.50/60.15 [__(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 > [1 0] X1 + [1 0] X2 + [0] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 = [n____(X1, X2)] 171.50/60.15 171.50/60.15 [__(X, nil())] = [1 0] X + [1] 171.50/60.15 [0 1] [4] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [__(__(X, Y), Z)] = [1 0] X + [1 0] Y + [1 0] Z + [2] 171.50/60.15 [0 1] [0 1] [0 1] [4] 171.50/60.15 >= [1 0] X + [1 0] Y + [1 0] Z + [2] 171.50/60.15 [0 1] [0 1] [0 1] [4] 171.50/60.15 = [__(X, __(Y, Z))] 171.50/60.15 171.50/60.15 [__(nil(), X)] = [1 0] X + [1] 171.50/60.15 [0 1] [4] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [nil()] = [0] 171.50/60.15 [2] 171.50/60.15 >= [0] 171.50/60.15 [2] 171.50/60.15 = [n__nil()] 171.50/60.15 171.50/60.15 [and(tt(), X)] = [1 2] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 >= [1 0] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 = [activate(X)] 171.50/60.15 171.50/60.15 [activate(X)] = [1 0] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [activate(n__nil())] = [1] 171.50/60.15 [2] 171.50/60.15 > [0] 171.50/60.15 [2] 171.50/60.15 = [nil()] 171.50/60.15 171.50/60.15 [activate(n____(X1, X2))] = [1 0] X1 + [1 0] X2 + [1] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 >= [1 0] X1 + [1 0] X2 + [1] 171.50/60.15 [0 1] [0 1] [2] 171.50/60.15 = [__(X1, X2)] 171.50/60.15 171.50/60.15 [activate(n__isList(X))] = [1 2] X + [3] 171.50/60.15 [0 0] [0] 171.50/60.15 > [1 2] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isList(X)] 171.50/60.15 171.50/60.15 [activate(n__isNeList(X))] = [1 2] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 2] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isNeList(X)] 171.50/60.15 171.50/60.15 [activate(n__isPal(X))] = [1 1] X + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 >= [1 1] X + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 = [isPal(X)] 171.50/60.15 171.50/60.15 [activate(n__a())] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [a()] 171.50/60.15 171.50/60.15 [activate(n__e())] = [2] 171.50/60.15 [0] 171.50/60.15 >= [2] 171.50/60.15 [0] 171.50/60.15 = [e()] 171.50/60.15 171.50/60.15 [activate(n__i())] = [2] 171.50/60.15 [0] 171.50/60.15 >= [2] 171.50/60.15 [0] 171.50/60.15 = [i()] 171.50/60.15 171.50/60.15 [activate(n__o())] = [1] 171.50/60.15 [1] 171.50/60.15 >= [1] 171.50/60.15 [1] 171.50/60.15 = [o()] 171.50/60.15 171.50/60.15 [activate(n__u())] = [1] 171.50/60.15 [1] 171.50/60.15 >= [1] 171.50/60.15 [1] 171.50/60.15 = [u()] 171.50/60.15 171.50/60.15 [isList(V)] = [1 2] V + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 2] V + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isNeList(activate(V))] 171.50/60.15 171.50/60.15 [isList(X)] = [1 2] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 2] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [n__isList(X)] 171.50/60.15 171.50/60.15 [isList(n__nil())] = [6] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isList(n____(V1, V2))] = [1 2] V1 + [1 2] V2 + [6] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 2] V1 + [1 2] V2 + [6] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.15 171.50/60.15 [isNeList(V)] = [1 2] V + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] V + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isQid(activate(V))] 171.50/60.15 171.50/60.15 [isNeList(X)] = [1 2] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 > [1 2] X + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 = [n__isNeList(X)] 171.50/60.15 171.50/60.15 [isNeList(n____(V1, V2))] = [1 2] V1 + [1 2] V2 + [5] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 > [1 2] V1 + [1 2] V2 + [4] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.15 171.50/60.15 [isNeList(n____(V1, V2))] = [1 2] V1 + [1 2] V2 + [5] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 2] V1 + [1 2] V2 + [5] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.15 171.50/60.15 [isQid(n__a())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__e())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__i())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__o())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__u())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isNePal(V)] = [1 1] V + [1] 171.50/60.15 [0 0] [1] 171.50/60.15 >= [1 1] V + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isQid(activate(V))] 171.50/60.15 171.50/60.15 [isNePal(n____(I, __(P, I)))] = [2 2] I + [1 1] P + [6] 171.50/60.15 [0 0] [0 0] [1] 171.50/60.15 > [1 1] I + [1 1] P + [5] 171.50/60.15 [0 0] [0 0] [1] 171.50/60.15 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.15 171.50/60.15 [isPal(V)] = [1 1] V + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 >= [1 1] V + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 = [isNePal(activate(V))] 171.50/60.15 171.50/60.15 [isPal(X)] = [1 1] X + [2] 171.50/60.15 [0 0] [1] 171.50/60.15 > [1 1] X + [1] 171.50/60.15 [0 0] [1] 171.50/60.15 = [n__isPal(X)] 171.50/60.15 171.50/60.15 [isPal(n__nil())] = [4] 171.50/60.15 [1] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [a()] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [n__a()] 171.50/60.15 171.50/60.15 [e()] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [n__e()] 171.50/60.15 171.50/60.15 [i()] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [n__i()] 171.50/60.15 171.50/60.15 [o()] = [1] 171.50/60.15 [1] 171.50/60.15 > [0] 171.50/60.15 [1] 171.50/60.15 = [n__o()] 171.50/60.15 171.50/60.15 [u()] = [1] 171.50/60.15 [1] 171.50/60.15 > [0] 171.50/60.15 [1] 171.50/60.15 = [n__u()] 171.50/60.15 171.50/60.15 171.50/60.15 We return to the main proof. 171.50/60.15 171.50/60.15 We are left with following problem, upon which TcT provides the 171.50/60.15 certificate YES(O(1),O(n^2)). 171.50/60.15 171.50/60.15 Strict Trs: { isList(X) -> n__isList(X) } 171.50/60.15 Weak Trs: 171.50/60.15 { __(X1, X2) -> n____(X1, X2) 171.50/60.15 , __(X, nil()) -> X 171.50/60.15 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.15 , __(nil(), X) -> X 171.50/60.15 , nil() -> n__nil() 171.50/60.15 , and(tt(), X) -> activate(X) 171.50/60.15 , activate(X) -> X 171.50/60.15 , activate(n__nil()) -> nil() 171.50/60.15 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.15 , activate(n__isList(X)) -> isList(X) 171.50/60.15 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.15 , activate(n__isPal(X)) -> isPal(X) 171.50/60.15 , activate(n__a()) -> a() 171.50/60.15 , activate(n__e()) -> e() 171.50/60.15 , activate(n__i()) -> i() 171.50/60.15 , activate(n__o()) -> o() 171.50/60.15 , activate(n__u()) -> u() 171.50/60.15 , isList(V) -> isNeList(activate(V)) 171.50/60.15 , isList(n__nil()) -> tt() 171.50/60.15 , isList(n____(V1, V2)) -> 171.50/60.15 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.15 , isNeList(V) -> isQid(activate(V)) 171.50/60.15 , isNeList(X) -> n__isNeList(X) 171.50/60.15 , isNeList(n____(V1, V2)) -> 171.50/60.15 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.15 , isNeList(n____(V1, V2)) -> 171.50/60.15 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.15 , isQid(n__a()) -> tt() 171.50/60.15 , isQid(n__e()) -> tt() 171.50/60.15 , isQid(n__i()) -> tt() 171.50/60.15 , isQid(n__o()) -> tt() 171.50/60.15 , isQid(n__u()) -> tt() 171.50/60.15 , isNePal(V) -> isQid(activate(V)) 171.50/60.15 , isNePal(n____(I, __(P, I))) -> 171.50/60.15 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.15 , isPal(V) -> isNePal(activate(V)) 171.50/60.15 , isPal(X) -> n__isPal(X) 171.50/60.15 , isPal(n__nil()) -> tt() 171.50/60.15 , a() -> n__a() 171.50/60.15 , e() -> n__e() 171.50/60.15 , i() -> n__i() 171.50/60.15 , o() -> n__o() 171.50/60.15 , u() -> n__u() } 171.50/60.15 Obligation: 171.50/60.15 derivational complexity 171.50/60.15 Answer: 171.50/60.15 YES(O(1),O(n^2)) 171.50/60.15 171.50/60.15 We use the processor 'matrix interpretation of dimension 2' to 171.50/60.15 orient following rules strictly. 171.50/60.15 171.50/60.15 Trs: { isList(X) -> n__isList(X) } 171.50/60.15 171.50/60.15 The induced complexity on above rules (modulo remaining rules) is 171.50/60.15 YES(?,O(n^2)) . These rules are moved into the corresponding weak 171.50/60.15 component(s). 171.50/60.15 171.50/60.15 Sub-proof: 171.50/60.15 ---------- 171.50/60.15 TcT has computed the following triangular matrix interpretation. 171.50/60.15 171.50/60.15 [__](x1, x2) = [1 2] x1 + [1 0] x2 + [2] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 171.50/60.15 [nil] = [0] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 171.50/60.15 [0 0] [0 1] [0] 171.50/60.15 171.50/60.15 [tt] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [activate](x1) = [1 0] x1 + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 171.50/60.15 [isList](x1) = [1 1] x1 + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isNeList](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__nil] = [0] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n____](x1, x2) = [1 2] x1 + [1 0] x2 + [2] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 171.50/60.15 [n__isList](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isQid](x1) = [1 1] x1 + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__isNeList](x1) = [1 1] x1 + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isNePal](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__isPal](x1) = [1 1] x1 + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [isPal](x1) = [1 1] x1 + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 171.50/60.15 [n__a] = [2] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [n__e] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n__i] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [n__o] = [0] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [n__u] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [a] = [2] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [e] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [i] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 [o] = [1] 171.50/60.15 [2] 171.50/60.15 171.50/60.15 [u] = [1] 171.50/60.15 [0] 171.50/60.15 171.50/60.15 The order satisfies the following ordering constraints: 171.50/60.15 171.50/60.15 [__(X1, X2)] = [1 2] X1 + [1 0] X2 + [2] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 >= [1 2] X1 + [1 0] X2 + [2] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 = [n____(X1, X2)] 171.50/60.15 171.50/60.15 [__(X, nil())] = [1 2] X + [2] 171.50/60.15 [0 1] [1] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [__(__(X, Y), Z)] = [1 4] X + [1 2] Y + [1 0] Z + [6] 171.50/60.15 [0 1] [0 1] [0 1] [2] 171.50/60.15 > [1 2] X + [1 2] Y + [1 0] Z + [4] 171.50/60.15 [0 1] [0 1] [0 1] [2] 171.50/60.15 = [__(X, __(Y, Z))] 171.50/60.15 171.50/60.15 [__(nil(), X)] = [1 0] X + [2] 171.50/60.15 [0 1] [1] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [nil()] = [0] 171.50/60.15 [0] 171.50/60.15 >= [0] 171.50/60.15 [0] 171.50/60.15 = [n__nil()] 171.50/60.15 171.50/60.15 [and(tt(), X)] = [1 0] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 >= [1 0] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 = [activate(X)] 171.50/60.15 171.50/60.15 [activate(X)] = [1 0] X + [1] 171.50/60.15 [0 1] [0] 171.50/60.15 > [1 0] X + [0] 171.50/60.15 [0 1] [0] 171.50/60.15 = [X] 171.50/60.15 171.50/60.15 [activate(n__nil())] = [1] 171.50/60.15 [0] 171.50/60.15 > [0] 171.50/60.15 [0] 171.50/60.15 = [nil()] 171.50/60.15 171.50/60.15 [activate(n____(X1, X2))] = [1 2] X1 + [1 0] X2 + [3] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 > [1 2] X1 + [1 0] X2 + [2] 171.50/60.15 [0 1] [0 1] [1] 171.50/60.15 = [__(X1, X2)] 171.50/60.15 171.50/60.15 [activate(n__isList(X))] = [1 1] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isList(X)] 171.50/60.15 171.50/60.15 [activate(n__isNeList(X))] = [1 1] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isNeList(X)] 171.50/60.15 171.50/60.15 [activate(n__isPal(X))] = [1 1] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isPal(X)] 171.50/60.15 171.50/60.15 [activate(n__a())] = [3] 171.50/60.15 [2] 171.50/60.15 > [2] 171.50/60.15 [2] 171.50/60.15 = [a()] 171.50/60.15 171.50/60.15 [activate(n__e())] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [e()] 171.50/60.15 171.50/60.15 [activate(n__i())] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [i()] 171.50/60.15 171.50/60.15 [activate(n__o())] = [1] 171.50/60.15 [2] 171.50/60.15 >= [1] 171.50/60.15 [2] 171.50/60.15 = [o()] 171.50/60.15 171.50/60.15 [activate(n__u())] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [u()] 171.50/60.15 171.50/60.15 [isList(V)] = [1 1] V + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] V + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isNeList(activate(V))] 171.50/60.15 171.50/60.15 [isList(X)] = [1 1] X + [2] 171.50/60.15 [0 0] [0] 171.50/60.15 > [1 1] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [n__isList(X)] 171.50/60.15 171.50/60.15 [isList(n__nil())] = [2] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isList(n____(V1, V2))] = [1 3] V1 + [1 1] V2 + [5] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 1] V1 + [1 1] V2 + [5] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isList(activate(V1)), n__isList(activate(V2)))] 171.50/60.15 171.50/60.15 [isNeList(V)] = [1 1] V + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 >= [1 1] V + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 = [isQid(activate(V))] 171.50/60.15 171.50/60.15 [isNeList(X)] = [1 1] X + [1] 171.50/60.15 [0 0] [0] 171.50/60.15 > [1 1] X + [0] 171.50/60.15 [0 0] [0] 171.50/60.15 = [n__isNeList(X)] 171.50/60.15 171.50/60.15 [isNeList(n____(V1, V2))] = [1 3] V1 + [1 1] V2 + [4] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 1] V1 + [1 1] V2 + [4] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 171.50/60.15 171.50/60.15 [isNeList(n____(V1, V2))] = [1 3] V1 + [1 1] V2 + [4] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 >= [1 1] V1 + [1 1] V2 + [4] 171.50/60.15 [0 0] [0 0] [0] 171.50/60.15 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 171.50/60.15 171.50/60.15 [isQid(n__a())] = [4] 171.50/60.15 [0] 171.50/60.15 > [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__e())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.15 171.50/60.15 [isQid(n__i())] = [1] 171.50/60.15 [0] 171.50/60.15 >= [1] 171.50/60.15 [0] 171.50/60.15 = [tt()] 171.50/60.16 171.50/60.16 [isQid(n__o())] = [2] 171.50/60.16 [0] 171.50/60.16 > [1] 171.50/60.16 [0] 171.50/60.16 = [tt()] 171.50/60.16 171.50/60.16 [isQid(n__u())] = [1] 171.50/60.16 [0] 171.50/60.16 >= [1] 171.50/60.16 [0] 171.50/60.16 = [tt()] 171.50/60.16 171.50/60.16 [isNePal(V)] = [1 1] V + [1] 171.50/60.16 [0 0] [0] 171.50/60.16 >= [1 1] V + [1] 171.50/60.16 [0 0] [0] 171.50/60.16 = [isQid(activate(V))] 171.50/60.16 171.50/60.16 [isNePal(n____(I, __(P, I)))] = [2 4] I + [1 3] P + [7] 171.50/60.16 [0 0] [0 0] [0] 171.50/60.16 > [1 1] I + [1 1] P + [3] 171.50/60.16 [0 0] [0 0] [0] 171.50/60.16 = [and(isQid(activate(I)), n__isPal(activate(P)))] 171.50/60.16 171.50/60.16 [isPal(V)] = [1 1] V + [2] 171.50/60.16 [0 0] [0] 171.50/60.16 >= [1 1] V + [2] 171.50/60.16 [0 0] [0] 171.50/60.16 = [isNePal(activate(V))] 171.50/60.16 171.50/60.16 [isPal(X)] = [1 1] X + [2] 171.50/60.16 [0 0] [0] 171.50/60.16 > [1 1] X + [1] 171.50/60.16 [0 0] [0] 171.50/60.16 = [n__isPal(X)] 171.50/60.16 171.50/60.16 [isPal(n__nil())] = [2] 171.50/60.16 [0] 171.50/60.16 > [1] 171.50/60.16 [0] 171.50/60.16 = [tt()] 171.50/60.16 171.50/60.16 [a()] = [2] 171.50/60.16 [2] 171.50/60.16 >= [2] 171.50/60.16 [2] 171.50/60.16 = [n__a()] 171.50/60.16 171.50/60.16 [e()] = [1] 171.50/60.16 [0] 171.50/60.16 >= [1] 171.50/60.16 [0] 171.50/60.16 = [n__e()] 171.50/60.16 171.50/60.16 [i()] = [1] 171.50/60.16 [0] 171.50/60.16 >= [1] 171.50/60.16 [0] 171.50/60.16 = [n__i()] 171.50/60.16 171.50/60.16 [o()] = [1] 171.50/60.16 [2] 171.50/60.16 > [0] 171.50/60.16 [2] 171.50/60.16 = [n__o()] 171.50/60.16 171.50/60.16 [u()] = [1] 171.50/60.16 [0] 171.50/60.16 >= [1] 171.50/60.16 [0] 171.50/60.16 = [n__u()] 171.50/60.16 171.50/60.16 171.50/60.16 We return to the main proof. 171.50/60.16 171.50/60.16 We are left with following problem, upon which TcT provides the 171.50/60.16 certificate YES(O(1),O(1)). 171.50/60.16 171.50/60.16 Weak Trs: 171.50/60.16 { __(X1, X2) -> n____(X1, X2) 171.50/60.16 , __(X, nil()) -> X 171.50/60.16 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 171.50/60.16 , __(nil(), X) -> X 171.50/60.16 , nil() -> n__nil() 171.50/60.16 , and(tt(), X) -> activate(X) 171.50/60.16 , activate(X) -> X 171.50/60.16 , activate(n__nil()) -> nil() 171.50/60.16 , activate(n____(X1, X2)) -> __(X1, X2) 171.50/60.16 , activate(n__isList(X)) -> isList(X) 171.50/60.16 , activate(n__isNeList(X)) -> isNeList(X) 171.50/60.16 , activate(n__isPal(X)) -> isPal(X) 171.50/60.16 , activate(n__a()) -> a() 171.50/60.16 , activate(n__e()) -> e() 171.50/60.16 , activate(n__i()) -> i() 171.50/60.16 , activate(n__o()) -> o() 171.50/60.16 , activate(n__u()) -> u() 171.50/60.16 , isList(V) -> isNeList(activate(V)) 171.50/60.16 , isList(X) -> n__isList(X) 171.50/60.16 , isList(n__nil()) -> tt() 171.50/60.16 , isList(n____(V1, V2)) -> 171.50/60.16 and(isList(activate(V1)), n__isList(activate(V2))) 171.50/60.16 , isNeList(V) -> isQid(activate(V)) 171.50/60.16 , isNeList(X) -> n__isNeList(X) 171.50/60.16 , isNeList(n____(V1, V2)) -> 171.50/60.16 and(isList(activate(V1)), n__isNeList(activate(V2))) 171.50/60.16 , isNeList(n____(V1, V2)) -> 171.50/60.16 and(isNeList(activate(V1)), n__isList(activate(V2))) 171.50/60.16 , isQid(n__a()) -> tt() 171.50/60.16 , isQid(n__e()) -> tt() 171.50/60.16 , isQid(n__i()) -> tt() 171.50/60.16 , isQid(n__o()) -> tt() 171.50/60.16 , isQid(n__u()) -> tt() 171.50/60.16 , isNePal(V) -> isQid(activate(V)) 171.50/60.16 , isNePal(n____(I, __(P, I))) -> 171.50/60.16 and(isQid(activate(I)), n__isPal(activate(P))) 171.50/60.16 , isPal(V) -> isNePal(activate(V)) 171.50/60.16 , isPal(X) -> n__isPal(X) 171.50/60.16 , isPal(n__nil()) -> tt() 171.50/60.16 , a() -> n__a() 171.50/60.16 , e() -> n__e() 171.50/60.16 , i() -> n__i() 171.50/60.16 , o() -> n__o() 171.50/60.16 , u() -> n__u() } 171.50/60.16 Obligation: 171.50/60.16 derivational complexity 171.50/60.16 Answer: 171.50/60.16 YES(O(1),O(1)) 171.50/60.16 171.50/60.16 Empty rules are trivially bounded 171.50/60.16 171.50/60.16 Hurray, we answered YES(O(1),O(n^2)) 171.67/60.24 EOF