MAYBE 217.08/60.05 MAYBE 217.08/60.05 217.08/60.05 We are left with following problem, upon which TcT provides the 217.08/60.05 certificate MAYBE. 217.08/60.05 217.08/60.05 Strict Trs: 217.08/60.05 { __(X1, X2) -> n____(X1, X2) 217.08/60.05 , __(X, nil()) -> X 217.08/60.05 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.05 , __(nil(), X) -> X 217.08/60.05 , nil() -> n__nil() 217.08/60.05 , and(tt(), X) -> activate(X) 217.08/60.05 , activate(X) -> X 217.08/60.05 , activate(n__nil()) -> nil() 217.08/60.05 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.05 , activate(n__isList(X)) -> isList(X) 217.08/60.05 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.05 , activate(n__isPal(X)) -> isPal(X) 217.08/60.05 , activate(n__a()) -> a() 217.08/60.05 , activate(n__e()) -> e() 217.08/60.05 , activate(n__i()) -> i() 217.08/60.05 , activate(n__o()) -> o() 217.08/60.05 , activate(n__u()) -> u() 217.08/60.05 , isList(V) -> isNeList(activate(V)) 217.08/60.05 , isList(X) -> n__isList(X) 217.08/60.05 , isList(n__nil()) -> tt() 217.08/60.05 , isList(n____(V1, V2)) -> 217.08/60.05 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.05 , isNeList(V) -> isQid(activate(V)) 217.08/60.05 , isNeList(X) -> n__isNeList(X) 217.08/60.05 , isNeList(n____(V1, V2)) -> 217.08/60.05 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.05 , isNeList(n____(V1, V2)) -> 217.08/60.05 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.05 , isQid(n__a()) -> tt() 217.08/60.05 , isQid(n__e()) -> tt() 217.08/60.05 , isQid(n__i()) -> tt() 217.08/60.05 , isQid(n__o()) -> tt() 217.08/60.05 , isQid(n__u()) -> tt() 217.08/60.05 , isNePal(V) -> isQid(activate(V)) 217.08/60.05 , isNePal(n____(I, n____(P, I))) -> 217.08/60.05 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.05 , isPal(V) -> isNePal(activate(V)) 217.08/60.05 , isPal(X) -> n__isPal(X) 217.08/60.05 , isPal(n__nil()) -> tt() 217.08/60.05 , a() -> n__a() 217.08/60.05 , e() -> n__e() 217.08/60.05 , i() -> n__i() 217.08/60.05 , o() -> n__o() 217.08/60.05 , u() -> n__u() } 217.08/60.05 Obligation: 217.08/60.05 derivational complexity 217.08/60.05 Answer: 217.08/60.05 MAYBE 217.08/60.05 217.08/60.05 None of the processors succeeded. 217.08/60.05 217.08/60.05 Details of failed attempt(s): 217.08/60.05 ----------------------------- 217.08/60.05 1) 'Fastest (timeout of 60 seconds)' failed due to the following 217.08/60.05 reason: 217.08/60.05 217.08/60.05 Computation stopped due to timeout after 60.0 seconds. 217.08/60.05 217.08/60.05 2) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 217.08/60.05 the following reason: 217.08/60.05 217.08/60.05 The weightgap principle applies (using the following nonconstant 217.08/60.05 growth matrix-interpretation) 217.08/60.05 217.08/60.05 TcT has computed the following triangular matrix interpretation. 217.08/60.05 Note that the diagonal of the component-wise maxima of 217.08/60.05 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.05 217.08/60.05 [__](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.05 217.08/60.05 [nil] = [0] 217.08/60.05 217.08/60.05 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.05 217.08/60.05 [tt] = [0] 217.08/60.05 217.08/60.05 [activate](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [isList](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [isNeList](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [n__nil] = [0] 217.08/60.05 217.08/60.05 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.05 217.08/60.05 [n__isList](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [isQid](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [n__isNeList](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [isNePal](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [n__isPal](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [isPal](x1) = [1] x1 + [0] 217.08/60.05 217.08/60.05 [n__a] = [0] 217.08/60.05 217.08/60.05 [n__e] = [0] 217.08/60.05 217.08/60.05 [n__i] = [0] 217.08/60.05 217.08/60.05 [n__o] = [0] 217.08/60.05 217.08/60.05 [n__u] = [0] 217.08/60.05 217.08/60.05 [a] = [2] 217.08/60.05 217.08/60.05 [e] = [2] 217.08/60.05 217.08/60.05 [i] = [2] 217.08/60.05 217.08/60.05 [o] = [1] 217.08/60.05 217.08/60.05 [u] = [1] 217.08/60.05 217.08/60.05 The order satisfies the following ordering constraints: 217.08/60.05 217.08/60.05 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 217.08/60.05 >= [1] X1 + [1] X2 + [0] 217.08/60.05 = [n____(X1, X2)] 217.08/60.05 217.08/60.05 [__(X, nil())] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [X] 217.08/60.05 217.08/60.05 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 217.08/60.05 >= [1] X + [1] Y + [1] Z + [0] 217.08/60.05 = [__(X, __(Y, Z))] 217.08/60.05 217.08/60.05 [__(nil(), X)] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [X] 217.08/60.05 217.08/60.05 [nil()] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [n__nil()] 217.08/60.05 217.08/60.05 [and(tt(), X)] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [activate(X)] 217.08/60.05 217.08/60.05 [activate(X)] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [X] 217.08/60.05 217.08/60.05 [activate(n__nil())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [nil()] 217.08/60.05 217.08/60.05 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 217.08/60.05 >= [1] X1 + [1] X2 + [0] 217.08/60.05 = [__(activate(X1), activate(X2))] 217.08/60.05 217.08/60.05 [activate(n__isList(X))] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [isList(X)] 217.08/60.05 217.08/60.05 [activate(n__isNeList(X))] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [isNeList(X)] 217.08/60.05 217.08/60.05 [activate(n__isPal(X))] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [isPal(X)] 217.08/60.05 217.08/60.05 [activate(n__a())] = [0] 217.08/60.05 ? [2] 217.08/60.05 = [a()] 217.08/60.05 217.08/60.05 [activate(n__e())] = [0] 217.08/60.05 ? [2] 217.08/60.05 = [e()] 217.08/60.05 217.08/60.05 [activate(n__i())] = [0] 217.08/60.05 ? [2] 217.08/60.05 = [i()] 217.08/60.05 217.08/60.05 [activate(n__o())] = [0] 217.08/60.05 ? [1] 217.08/60.05 = [o()] 217.08/60.05 217.08/60.05 [activate(n__u())] = [0] 217.08/60.05 ? [1] 217.08/60.05 = [u()] 217.08/60.05 217.08/60.05 [isList(V)] = [1] V + [0] 217.08/60.05 >= [1] V + [0] 217.08/60.05 = [isNeList(activate(V))] 217.08/60.05 217.08/60.05 [isList(X)] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [n__isList(X)] 217.08/60.05 217.08/60.05 [isList(n__nil())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 217.08/60.05 >= [1] V1 + [1] V2 + [0] 217.08/60.05 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.05 217.08/60.05 [isNeList(V)] = [1] V + [0] 217.08/60.05 >= [1] V + [0] 217.08/60.05 = [isQid(activate(V))] 217.08/60.05 217.08/60.05 [isNeList(X)] = [1] X + [0] 217.08/60.05 >= [1] X + [0] 217.08/60.05 = [n__isNeList(X)] 217.08/60.05 217.08/60.05 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 217.08/60.05 >= [1] V1 + [1] V2 + [0] 217.08/60.05 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.05 217.08/60.05 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 217.08/60.05 >= [1] V1 + [1] V2 + [0] 217.08/60.05 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.05 217.08/60.05 [isQid(n__a())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isQid(n__e())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isQid(n__i())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isQid(n__o())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isQid(n__u())] = [0] 217.08/60.05 >= [0] 217.08/60.05 = [tt()] 217.08/60.05 217.08/60.05 [isNePal(V)] = [1] V + [0] 217.08/60.06 >= [1] V + [0] 217.08/60.06 = [isQid(activate(V))] 217.08/60.06 217.08/60.06 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [0] 217.08/60.06 >= [1] I + [1] P + [0] 217.08/60.06 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.06 217.08/60.06 [isPal(V)] = [1] V + [0] 217.08/60.06 >= [1] V + [0] 217.08/60.06 = [isNePal(activate(V))] 217.08/60.06 217.08/60.06 [isPal(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [n__isPal(X)] 217.08/60.06 217.08/60.06 [isPal(n__nil())] = [0] 217.08/60.06 >= [0] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [a()] = [2] 217.08/60.06 > [0] 217.08/60.06 = [n__a()] 217.08/60.06 217.08/60.06 [e()] = [2] 217.08/60.06 > [0] 217.08/60.06 = [n__e()] 217.08/60.06 217.08/60.06 [i()] = [2] 217.08/60.06 > [0] 217.08/60.06 = [n__i()] 217.08/60.06 217.08/60.06 [o()] = [1] 217.08/60.06 > [0] 217.08/60.06 = [n__o()] 217.08/60.06 217.08/60.06 [u()] = [1] 217.08/60.06 > [0] 217.08/60.06 = [n__u()] 217.08/60.06 217.08/60.06 217.08/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.06 217.08/60.06 We are left with following problem, upon which TcT provides the 217.08/60.06 certificate MAYBE. 217.08/60.06 217.08/60.06 Strict Trs: 217.08/60.06 { __(X1, X2) -> n____(X1, X2) 217.08/60.06 , __(X, nil()) -> X 217.08/60.06 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.06 , __(nil(), X) -> X 217.08/60.06 , nil() -> n__nil() 217.08/60.06 , and(tt(), X) -> activate(X) 217.08/60.06 , activate(X) -> X 217.08/60.06 , activate(n__nil()) -> nil() 217.08/60.06 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.06 , activate(n__isList(X)) -> isList(X) 217.08/60.06 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.06 , activate(n__isPal(X)) -> isPal(X) 217.08/60.06 , activate(n__a()) -> a() 217.08/60.06 , activate(n__e()) -> e() 217.08/60.06 , activate(n__i()) -> i() 217.08/60.06 , activate(n__o()) -> o() 217.08/60.06 , activate(n__u()) -> u() 217.08/60.06 , isList(V) -> isNeList(activate(V)) 217.08/60.06 , isList(X) -> n__isList(X) 217.08/60.06 , isList(n__nil()) -> tt() 217.08/60.06 , isList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isNeList(V) -> isQid(activate(V)) 217.08/60.06 , isNeList(X) -> n__isNeList(X) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isQid(n__a()) -> tt() 217.08/60.06 , isQid(n__e()) -> tt() 217.08/60.06 , isQid(n__i()) -> tt() 217.08/60.06 , isQid(n__o()) -> tt() 217.08/60.06 , isQid(n__u()) -> tt() 217.08/60.06 , isNePal(V) -> isQid(activate(V)) 217.08/60.06 , isNePal(n____(I, n____(P, I))) -> 217.08/60.06 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.06 , isPal(V) -> isNePal(activate(V)) 217.08/60.06 , isPal(X) -> n__isPal(X) 217.08/60.06 , isPal(n__nil()) -> tt() } 217.08/60.06 Weak Trs: 217.08/60.06 { a() -> n__a() 217.08/60.06 , e() -> n__e() 217.08/60.06 , i() -> n__i() 217.08/60.06 , o() -> n__o() 217.08/60.06 , u() -> n__u() } 217.08/60.06 Obligation: 217.08/60.06 derivational complexity 217.08/60.06 Answer: 217.08/60.06 MAYBE 217.08/60.06 217.08/60.06 The weightgap principle applies (using the following nonconstant 217.08/60.06 growth matrix-interpretation) 217.08/60.06 217.08/60.06 TcT has computed the following triangular matrix interpretation. 217.08/60.06 Note that the diagonal of the component-wise maxima of 217.08/60.06 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.06 217.08/60.06 [__](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.06 217.08/60.06 [nil] = [2] 217.08/60.06 217.08/60.06 [and](x1, x2) = [1] x1 + [1] x2 + [1] 217.08/60.06 217.08/60.06 [tt] = [1] 217.08/60.06 217.08/60.06 [activate](x1) = [1] x1 + [2] 217.08/60.06 217.08/60.06 [isList](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [isNeList](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [n__nil] = [2] 217.08/60.06 217.08/60.06 [n____](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.06 217.08/60.06 [n__isList](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [isQid](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [n__isNeList](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [isNePal](x1) = [1] x1 + [2] 217.08/60.06 217.08/60.06 [n__isPal](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [isPal](x1) = [1] x1 + [1] 217.08/60.06 217.08/60.06 [n__a] = [1] 217.08/60.06 217.08/60.06 [n__e] = [1] 217.08/60.06 217.08/60.06 [n__i] = [2] 217.08/60.06 217.08/60.06 [n__o] = [1] 217.08/60.06 217.08/60.06 [n__u] = [1] 217.08/60.06 217.08/60.06 [a] = [2] 217.08/60.06 217.08/60.06 [e] = [2] 217.08/60.06 217.08/60.06 [i] = [2] 217.08/60.06 217.08/60.06 [o] = [2] 217.08/60.06 217.08/60.06 [u] = [2] 217.08/60.06 217.08/60.06 The order satisfies the following ordering constraints: 217.08/60.06 217.08/60.06 [__(X1, X2)] = [1] X1 + [1] X2 + [2] 217.08/60.06 >= [1] X1 + [1] X2 + [2] 217.08/60.06 = [n____(X1, X2)] 217.08/60.06 217.08/60.06 [__(X, nil())] = [1] X + [4] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [4] 217.08/60.06 >= [1] X + [1] Y + [1] Z + [4] 217.08/60.06 = [__(X, __(Y, Z))] 217.08/60.06 217.08/60.06 [__(nil(), X)] = [1] X + [4] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [nil()] = [2] 217.08/60.06 >= [2] 217.08/60.06 = [n__nil()] 217.08/60.06 217.08/60.06 [and(tt(), X)] = [1] X + [2] 217.08/60.06 >= [1] X + [2] 217.08/60.06 = [activate(X)] 217.08/60.06 217.08/60.06 [activate(X)] = [1] X + [2] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [activate(n__nil())] = [4] 217.08/60.06 > [2] 217.08/60.06 = [nil()] 217.08/60.06 217.08/60.06 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [4] 217.08/60.06 ? [1] X1 + [1] X2 + [6] 217.08/60.06 = [__(activate(X1), activate(X2))] 217.08/60.06 217.08/60.06 [activate(n__isList(X))] = [1] X + [3] 217.08/60.06 > [1] X + [1] 217.08/60.06 = [isList(X)] 217.08/60.06 217.08/60.06 [activate(n__isNeList(X))] = [1] X + [3] 217.08/60.06 > [1] X + [1] 217.08/60.06 = [isNeList(X)] 217.08/60.06 217.08/60.06 [activate(n__isPal(X))] = [1] X + [3] 217.08/60.06 > [1] X + [1] 217.08/60.06 = [isPal(X)] 217.08/60.06 217.08/60.06 [activate(n__a())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [a()] 217.08/60.06 217.08/60.06 [activate(n__e())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [e()] 217.08/60.06 217.08/60.06 [activate(n__i())] = [4] 217.08/60.06 > [2] 217.08/60.06 = [i()] 217.08/60.06 217.08/60.06 [activate(n__o())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [o()] 217.08/60.06 217.08/60.06 [activate(n__u())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [u()] 217.08/60.06 217.08/60.06 [isList(V)] = [1] V + [1] 217.08/60.06 ? [1] V + [3] 217.08/60.06 = [isNeList(activate(V))] 217.08/60.06 217.08/60.06 [isList(X)] = [1] X + [1] 217.08/60.06 >= [1] X + [1] 217.08/60.06 = [n__isList(X)] 217.08/60.06 217.08/60.06 [isList(n__nil())] = [3] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [3] 217.08/60.06 ? [1] V1 + [1] V2 + [7] 217.08/60.06 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.06 217.08/60.06 [isNeList(V)] = [1] V + [1] 217.08/60.06 ? [1] V + [3] 217.08/60.06 = [isQid(activate(V))] 217.08/60.06 217.08/60.06 [isNeList(X)] = [1] X + [1] 217.08/60.06 >= [1] X + [1] 217.08/60.06 = [n__isNeList(X)] 217.08/60.06 217.08/60.06 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [3] 217.08/60.06 ? [1] V1 + [1] V2 + [7] 217.08/60.06 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.06 217.08/60.06 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [3] 217.08/60.06 ? [1] V1 + [1] V2 + [7] 217.08/60.06 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.06 217.08/60.06 [isQid(n__a())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__e())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__i())] = [3] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__o())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__u())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isNePal(V)] = [1] V + [2] 217.08/60.06 ? [1] V + [3] 217.08/60.06 = [isQid(activate(V))] 217.08/60.06 217.08/60.06 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [6] 217.08/60.06 ? [1] I + [1] P + [7] 217.08/60.06 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.06 217.08/60.06 [isPal(V)] = [1] V + [1] 217.08/60.06 ? [1] V + [4] 217.08/60.06 = [isNePal(activate(V))] 217.08/60.06 217.08/60.06 [isPal(X)] = [1] X + [1] 217.08/60.06 >= [1] X + [1] 217.08/60.06 = [n__isPal(X)] 217.08/60.06 217.08/60.06 [isPal(n__nil())] = [3] 217.08/60.06 > [1] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [a()] = [2] 217.08/60.06 > [1] 217.08/60.06 = [n__a()] 217.08/60.06 217.08/60.06 [e()] = [2] 217.08/60.06 > [1] 217.08/60.06 = [n__e()] 217.08/60.06 217.08/60.06 [i()] = [2] 217.08/60.06 >= [2] 217.08/60.06 = [n__i()] 217.08/60.06 217.08/60.06 [o()] = [2] 217.08/60.06 > [1] 217.08/60.06 = [n__o()] 217.08/60.06 217.08/60.06 [u()] = [2] 217.08/60.06 > [1] 217.08/60.06 = [n__u()] 217.08/60.06 217.08/60.06 217.08/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.06 217.08/60.06 We are left with following problem, upon which TcT provides the 217.08/60.06 certificate MAYBE. 217.08/60.06 217.08/60.06 Strict Trs: 217.08/60.06 { __(X1, X2) -> n____(X1, X2) 217.08/60.06 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.06 , nil() -> n__nil() 217.08/60.06 , and(tt(), X) -> activate(X) 217.08/60.06 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.06 , isList(V) -> isNeList(activate(V)) 217.08/60.06 , isList(X) -> n__isList(X) 217.08/60.06 , isList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isNeList(V) -> isQid(activate(V)) 217.08/60.06 , isNeList(X) -> n__isNeList(X) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isNePal(V) -> isQid(activate(V)) 217.08/60.06 , isNePal(n____(I, n____(P, I))) -> 217.08/60.06 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.06 , isPal(V) -> isNePal(activate(V)) 217.08/60.06 , isPal(X) -> n__isPal(X) } 217.08/60.06 Weak Trs: 217.08/60.06 { __(X, nil()) -> X 217.08/60.06 , __(nil(), X) -> X 217.08/60.06 , activate(X) -> X 217.08/60.06 , activate(n__nil()) -> nil() 217.08/60.06 , activate(n__isList(X)) -> isList(X) 217.08/60.06 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.06 , activate(n__isPal(X)) -> isPal(X) 217.08/60.06 , activate(n__a()) -> a() 217.08/60.06 , activate(n__e()) -> e() 217.08/60.06 , activate(n__i()) -> i() 217.08/60.06 , activate(n__o()) -> o() 217.08/60.06 , activate(n__u()) -> u() 217.08/60.06 , isList(n__nil()) -> tt() 217.08/60.06 , isQid(n__a()) -> tt() 217.08/60.06 , isQid(n__e()) -> tt() 217.08/60.06 , isQid(n__i()) -> tt() 217.08/60.06 , isQid(n__o()) -> tt() 217.08/60.06 , isQid(n__u()) -> tt() 217.08/60.06 , isPal(n__nil()) -> tt() 217.08/60.06 , a() -> n__a() 217.08/60.06 , e() -> n__e() 217.08/60.06 , i() -> n__i() 217.08/60.06 , o() -> n__o() 217.08/60.06 , u() -> n__u() } 217.08/60.06 Obligation: 217.08/60.06 derivational complexity 217.08/60.06 Answer: 217.08/60.06 MAYBE 217.08/60.06 217.08/60.06 The weightgap principle applies (using the following nonconstant 217.08/60.06 growth matrix-interpretation) 217.08/60.06 217.08/60.06 TcT has computed the following triangular matrix interpretation. 217.08/60.06 Note that the diagonal of the component-wise maxima of 217.08/60.06 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.06 217.08/60.06 [__](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.06 217.08/60.06 [nil] = [1] 217.08/60.06 217.08/60.06 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.06 217.08/60.06 [tt] = [2] 217.08/60.06 217.08/60.06 [activate](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isNeList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [n__nil] = [2] 217.08/60.06 217.08/60.06 [n____](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.06 217.08/60.06 [n__isList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isQid](x1) = [1] x1 + [2] 217.08/60.06 217.08/60.06 [n__isNeList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isNePal](x1) = [1] x1 + [2] 217.08/60.06 217.08/60.06 [n__isPal](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isPal](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [n__a] = [1] 217.08/60.06 217.08/60.06 [n__e] = [1] 217.08/60.06 217.08/60.06 [n__i] = [1] 217.08/60.06 217.08/60.06 [n__o] = [1] 217.08/60.06 217.08/60.06 [n__u] = [1] 217.08/60.06 217.08/60.06 [a] = [1] 217.08/60.06 217.08/60.06 [e] = [1] 217.08/60.06 217.08/60.06 [i] = [1] 217.08/60.06 217.08/60.06 [o] = [1] 217.08/60.06 217.08/60.06 [u] = [1] 217.08/60.06 217.08/60.06 The order satisfies the following ordering constraints: 217.08/60.06 217.08/60.06 [__(X1, X2)] = [1] X1 + [1] X2 + [2] 217.08/60.06 >= [1] X1 + [1] X2 + [2] 217.08/60.06 = [n____(X1, X2)] 217.08/60.06 217.08/60.06 [__(X, nil())] = [1] X + [3] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [4] 217.08/60.06 >= [1] X + [1] Y + [1] Z + [4] 217.08/60.06 = [__(X, __(Y, Z))] 217.08/60.06 217.08/60.06 [__(nil(), X)] = [1] X + [3] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [nil()] = [1] 217.08/60.06 ? [2] 217.08/60.06 = [n__nil()] 217.08/60.06 217.08/60.06 [and(tt(), X)] = [1] X + [2] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [activate(X)] 217.08/60.06 217.08/60.06 [activate(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [activate(n__nil())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [nil()] 217.08/60.06 217.08/60.06 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [2] 217.08/60.06 >= [1] X1 + [1] X2 + [2] 217.08/60.06 = [__(activate(X1), activate(X2))] 217.08/60.06 217.08/60.06 [activate(n__isList(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isList(X)] 217.08/60.06 217.08/60.06 [activate(n__isNeList(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isNeList(X)] 217.08/60.06 217.08/60.06 [activate(n__isPal(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isPal(X)] 217.08/60.06 217.08/60.06 [activate(n__a())] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [a()] 217.08/60.06 217.08/60.06 [activate(n__e())] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [e()] 217.08/60.06 217.08/60.06 [activate(n__i())] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [i()] 217.08/60.06 217.08/60.06 [activate(n__o())] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [o()] 217.08/60.06 217.08/60.06 [activate(n__u())] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [u()] 217.08/60.06 217.08/60.06 [isList(V)] = [1] V + [0] 217.08/60.06 >= [1] V + [0] 217.08/60.06 = [isNeList(activate(V))] 217.08/60.06 217.08/60.06 [isList(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [n__isList(X)] 217.08/60.06 217.08/60.06 [isList(n__nil())] = [2] 217.08/60.06 >= [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 217.08/60.06 > [1] V1 + [1] V2 + [0] 217.08/60.06 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.06 217.08/60.06 [isNeList(V)] = [1] V + [0] 217.08/60.06 ? [1] V + [2] 217.08/60.06 = [isQid(activate(V))] 217.08/60.06 217.08/60.06 [isNeList(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [n__isNeList(X)] 217.08/60.06 217.08/60.06 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 217.08/60.06 > [1] V1 + [1] V2 + [0] 217.08/60.06 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.06 217.08/60.06 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 217.08/60.06 > [1] V1 + [1] V2 + [0] 217.08/60.06 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.06 217.08/60.06 [isQid(n__a())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__e())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__i())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__o())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isQid(n__u())] = [3] 217.08/60.06 > [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [isNePal(V)] = [1] V + [2] 217.08/60.06 >= [1] V + [2] 217.08/60.06 = [isQid(activate(V))] 217.08/60.06 217.08/60.06 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [6] 217.08/60.06 > [1] I + [1] P + [2] 217.08/60.06 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.06 217.08/60.06 [isPal(V)] = [1] V + [0] 217.08/60.06 ? [1] V + [2] 217.08/60.06 = [isNePal(activate(V))] 217.08/60.06 217.08/60.06 [isPal(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [n__isPal(X)] 217.08/60.06 217.08/60.06 [isPal(n__nil())] = [2] 217.08/60.06 >= [2] 217.08/60.06 = [tt()] 217.08/60.06 217.08/60.06 [a()] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [n__a()] 217.08/60.06 217.08/60.06 [e()] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [n__e()] 217.08/60.06 217.08/60.06 [i()] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [n__i()] 217.08/60.06 217.08/60.06 [o()] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [n__o()] 217.08/60.06 217.08/60.06 [u()] = [1] 217.08/60.06 >= [1] 217.08/60.06 = [n__u()] 217.08/60.06 217.08/60.06 217.08/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.06 217.08/60.06 We are left with following problem, upon which TcT provides the 217.08/60.06 certificate MAYBE. 217.08/60.06 217.08/60.06 Strict Trs: 217.08/60.06 { __(X1, X2) -> n____(X1, X2) 217.08/60.06 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.06 , nil() -> n__nil() 217.08/60.06 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.06 , isList(V) -> isNeList(activate(V)) 217.08/60.06 , isList(X) -> n__isList(X) 217.08/60.06 , isNeList(V) -> isQid(activate(V)) 217.08/60.06 , isNeList(X) -> n__isNeList(X) 217.08/60.06 , isNePal(V) -> isQid(activate(V)) 217.08/60.06 , isPal(V) -> isNePal(activate(V)) 217.08/60.06 , isPal(X) -> n__isPal(X) } 217.08/60.06 Weak Trs: 217.08/60.06 { __(X, nil()) -> X 217.08/60.06 , __(nil(), X) -> X 217.08/60.06 , and(tt(), X) -> activate(X) 217.08/60.06 , activate(X) -> X 217.08/60.06 , activate(n__nil()) -> nil() 217.08/60.06 , activate(n__isList(X)) -> isList(X) 217.08/60.06 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.06 , activate(n__isPal(X)) -> isPal(X) 217.08/60.06 , activate(n__a()) -> a() 217.08/60.06 , activate(n__e()) -> e() 217.08/60.06 , activate(n__i()) -> i() 217.08/60.06 , activate(n__o()) -> o() 217.08/60.06 , activate(n__u()) -> u() 217.08/60.06 , isList(n__nil()) -> tt() 217.08/60.06 , isList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.06 , isNeList(n____(V1, V2)) -> 217.08/60.06 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.06 , isQid(n__a()) -> tt() 217.08/60.06 , isQid(n__e()) -> tt() 217.08/60.06 , isQid(n__i()) -> tt() 217.08/60.06 , isQid(n__o()) -> tt() 217.08/60.06 , isQid(n__u()) -> tt() 217.08/60.06 , isNePal(n____(I, n____(P, I))) -> 217.08/60.06 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.06 , isPal(n__nil()) -> tt() 217.08/60.06 , a() -> n__a() 217.08/60.06 , e() -> n__e() 217.08/60.06 , i() -> n__i() 217.08/60.06 , o() -> n__o() 217.08/60.06 , u() -> n__u() } 217.08/60.06 Obligation: 217.08/60.06 derivational complexity 217.08/60.06 Answer: 217.08/60.06 MAYBE 217.08/60.06 217.08/60.06 The weightgap principle applies (using the following nonconstant 217.08/60.06 growth matrix-interpretation) 217.08/60.06 217.08/60.06 TcT has computed the following triangular matrix interpretation. 217.08/60.06 Note that the diagonal of the component-wise maxima of 217.08/60.06 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.06 217.08/60.06 [__](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.06 217.08/60.06 [nil] = [1] 217.08/60.06 217.08/60.06 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.06 217.08/60.06 [tt] = [2] 217.08/60.06 217.08/60.06 [activate](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isNeList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [n__nil] = [2] 217.08/60.06 217.08/60.06 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 217.08/60.06 217.08/60.06 [n__isList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isQid](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [n__isNeList](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isNePal](x1) = [1] x1 + [2] 217.08/60.06 217.08/60.06 [n__isPal](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [isPal](x1) = [1] x1 + [0] 217.08/60.06 217.08/60.06 [n__a] = [2] 217.08/60.06 217.08/60.06 [n__e] = [2] 217.08/60.06 217.08/60.06 [n__i] = [2] 217.08/60.06 217.08/60.06 [n__o] = [2] 217.08/60.06 217.08/60.06 [n__u] = [2] 217.08/60.06 217.08/60.06 [a] = [2] 217.08/60.06 217.08/60.06 [e] = [2] 217.08/60.06 217.08/60.06 [i] = [2] 217.08/60.06 217.08/60.06 [o] = [2] 217.08/60.06 217.08/60.06 [u] = [2] 217.08/60.06 217.08/60.06 The order satisfies the following ordering constraints: 217.08/60.06 217.08/60.06 [__(X1, X2)] = [1] X1 + [1] X2 + [2] 217.08/60.06 > [1] X1 + [1] X2 + [1] 217.08/60.06 = [n____(X1, X2)] 217.08/60.06 217.08/60.06 [__(X, nil())] = [1] X + [3] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [4] 217.08/60.06 >= [1] X + [1] Y + [1] Z + [4] 217.08/60.06 = [__(X, __(Y, Z))] 217.08/60.06 217.08/60.06 [__(nil(), X)] = [1] X + [3] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [nil()] = [1] 217.08/60.06 ? [2] 217.08/60.06 = [n__nil()] 217.08/60.06 217.08/60.06 [and(tt(), X)] = [1] X + [2] 217.08/60.06 > [1] X + [0] 217.08/60.06 = [activate(X)] 217.08/60.06 217.08/60.06 [activate(X)] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [X] 217.08/60.06 217.08/60.06 [activate(n__nil())] = [2] 217.08/60.06 > [1] 217.08/60.06 = [nil()] 217.08/60.06 217.08/60.06 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1] 217.08/60.06 ? [1] X1 + [1] X2 + [2] 217.08/60.06 = [__(activate(X1), activate(X2))] 217.08/60.06 217.08/60.06 [activate(n__isList(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isList(X)] 217.08/60.06 217.08/60.06 [activate(n__isNeList(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isNeList(X)] 217.08/60.06 217.08/60.06 [activate(n__isPal(X))] = [1] X + [0] 217.08/60.06 >= [1] X + [0] 217.08/60.06 = [isPal(X)] 217.08/60.06 217.08/60.06 [activate(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [a()] 217.08/60.07 217.08/60.07 [activate(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [e()] 217.08/60.07 217.08/60.07 [activate(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [i()] 217.08/60.07 217.08/60.07 [activate(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [o()] 217.08/60.07 217.08/60.07 [activate(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [u()] 217.08/60.07 217.08/60.07 [isList(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isNeList(activate(V))] 217.08/60.07 217.08/60.07 [isList(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isList(X)] 217.08/60.07 217.08/60.07 [isList(n__nil())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNeList(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isNeList(X)] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isQid(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isNePal(V)] = [1] V + [2] 217.08/60.07 > [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [4] 217.08/60.07 > [1] I + [1] P + [0] 217.08/60.07 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.07 217.08/60.07 [isPal(V)] = [1] V + [0] 217.08/60.07 ? [1] V + [2] 217.08/60.07 = [isNePal(activate(V))] 217.08/60.07 217.08/60.07 [isPal(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isPal(X)] 217.08/60.07 217.08/60.07 [isPal(n__nil())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [a()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__a()] 217.08/60.07 217.08/60.07 [e()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__e()] 217.08/60.07 217.08/60.07 [i()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__i()] 217.08/60.07 217.08/60.07 [o()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__o()] 217.08/60.07 217.08/60.07 [u()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__u()] 217.08/60.07 217.08/60.07 217.08/60.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.07 217.08/60.07 We are left with following problem, upon which TcT provides the 217.08/60.07 certificate MAYBE. 217.08/60.07 217.08/60.07 Strict Trs: 217.08/60.07 { __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.07 , nil() -> n__nil() 217.08/60.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.07 , isList(V) -> isNeList(activate(V)) 217.08/60.07 , isList(X) -> n__isList(X) 217.08/60.07 , isNeList(V) -> isQid(activate(V)) 217.08/60.07 , isNeList(X) -> n__isNeList(X) 217.08/60.07 , isPal(V) -> isNePal(activate(V)) 217.08/60.07 , isPal(X) -> n__isPal(X) } 217.08/60.07 Weak Trs: 217.08/60.07 { __(X1, X2) -> n____(X1, X2) 217.08/60.07 , __(X, nil()) -> X 217.08/60.07 , __(nil(), X) -> X 217.08/60.07 , and(tt(), X) -> activate(X) 217.08/60.07 , activate(X) -> X 217.08/60.07 , activate(n__nil()) -> nil() 217.08/60.07 , activate(n__isList(X)) -> isList(X) 217.08/60.07 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.07 , activate(n__isPal(X)) -> isPal(X) 217.08/60.07 , activate(n__a()) -> a() 217.08/60.07 , activate(n__e()) -> e() 217.08/60.07 , activate(n__i()) -> i() 217.08/60.07 , activate(n__o()) -> o() 217.08/60.07 , activate(n__u()) -> u() 217.08/60.07 , isList(n__nil()) -> tt() 217.08/60.07 , isList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isQid(n__a()) -> tt() 217.08/60.07 , isQid(n__e()) -> tt() 217.08/60.07 , isQid(n__i()) -> tt() 217.08/60.07 , isQid(n__o()) -> tt() 217.08/60.07 , isQid(n__u()) -> tt() 217.08/60.07 , isNePal(V) -> isQid(activate(V)) 217.08/60.07 , isNePal(n____(I, n____(P, I))) -> 217.08/60.07 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.07 , isPal(n__nil()) -> tt() 217.08/60.07 , a() -> n__a() 217.08/60.07 , e() -> n__e() 217.08/60.07 , i() -> n__i() 217.08/60.07 , o() -> n__o() 217.08/60.07 , u() -> n__u() } 217.08/60.07 Obligation: 217.08/60.07 derivational complexity 217.08/60.07 Answer: 217.08/60.07 MAYBE 217.08/60.07 217.08/60.07 The weightgap principle applies (using the following nonconstant 217.08/60.07 growth matrix-interpretation) 217.08/60.07 217.08/60.07 TcT has computed the following triangular matrix interpretation. 217.08/60.07 Note that the diagonal of the component-wise maxima of 217.08/60.07 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.07 217.08/60.07 [__](x1, x2) = [1] x1 + [1] x2 + [1] 217.08/60.07 217.08/60.07 [nil] = [1] 217.08/60.07 217.08/60.07 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.07 217.08/60.07 [tt] = [2] 217.08/60.07 217.08/60.07 [activate](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isNeList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__nil] = [2] 217.08/60.07 217.08/60.07 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 217.08/60.07 217.08/60.07 [n__isList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isQid](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__isNeList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isNePal](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__isPal](x1) = [1] x1 + [1] 217.08/60.07 217.08/60.07 [isPal](x1) = [1] x1 + [1] 217.08/60.07 217.08/60.07 [n__a] = [2] 217.08/60.07 217.08/60.07 [n__e] = [2] 217.08/60.07 217.08/60.07 [n__i] = [2] 217.08/60.07 217.08/60.07 [n__o] = [2] 217.08/60.07 217.08/60.07 [n__u] = [2] 217.08/60.07 217.08/60.07 [a] = [2] 217.08/60.07 217.08/60.07 [e] = [2] 217.08/60.07 217.08/60.07 [i] = [2] 217.08/60.07 217.08/60.07 [o] = [2] 217.08/60.07 217.08/60.07 [u] = [2] 217.08/60.07 217.08/60.07 The order satisfies the following ordering constraints: 217.08/60.07 217.08/60.07 [__(X1, X2)] = [1] X1 + [1] X2 + [1] 217.08/60.07 >= [1] X1 + [1] X2 + [1] 217.08/60.07 = [n____(X1, X2)] 217.08/60.07 217.08/60.07 [__(X, nil())] = [1] X + [2] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2] 217.08/60.07 >= [1] X + [1] Y + [1] Z + [2] 217.08/60.07 = [__(X, __(Y, Z))] 217.08/60.07 217.08/60.07 [__(nil(), X)] = [1] X + [2] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [nil()] = [1] 217.08/60.07 ? [2] 217.08/60.07 = [n__nil()] 217.08/60.07 217.08/60.07 [and(tt(), X)] = [1] X + [2] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [activate(X)] 217.08/60.07 217.08/60.07 [activate(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [activate(n__nil())] = [2] 217.08/60.07 > [1] 217.08/60.07 = [nil()] 217.08/60.07 217.08/60.07 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1] 217.08/60.07 >= [1] X1 + [1] X2 + [1] 217.08/60.07 = [__(activate(X1), activate(X2))] 217.08/60.07 217.08/60.07 [activate(n__isList(X))] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [isList(X)] 217.08/60.07 217.08/60.07 [activate(n__isNeList(X))] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [isNeList(X)] 217.08/60.07 217.08/60.07 [activate(n__isPal(X))] = [1] X + [1] 217.08/60.07 >= [1] X + [1] 217.08/60.07 = [isPal(X)] 217.08/60.07 217.08/60.07 [activate(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [a()] 217.08/60.07 217.08/60.07 [activate(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [e()] 217.08/60.07 217.08/60.07 [activate(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [i()] 217.08/60.07 217.08/60.07 [activate(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [o()] 217.08/60.07 217.08/60.07 [activate(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [u()] 217.08/60.07 217.08/60.07 [isList(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isNeList(activate(V))] 217.08/60.07 217.08/60.07 [isList(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isList(X)] 217.08/60.07 217.08/60.07 [isList(n__nil())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNeList(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isNeList(X)] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 > [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isQid(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isNePal(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [2] 217.08/60.07 > [1] I + [1] P + [1] 217.08/60.07 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.07 217.08/60.07 [isPal(V)] = [1] V + [1] 217.08/60.07 > [1] V + [0] 217.08/60.07 = [isNePal(activate(V))] 217.08/60.07 217.08/60.07 [isPal(X)] = [1] X + [1] 217.08/60.07 >= [1] X + [1] 217.08/60.07 = [n__isPal(X)] 217.08/60.07 217.08/60.07 [isPal(n__nil())] = [3] 217.08/60.07 > [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [a()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__a()] 217.08/60.07 217.08/60.07 [e()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__e()] 217.08/60.07 217.08/60.07 [i()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__i()] 217.08/60.07 217.08/60.07 [o()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__o()] 217.08/60.07 217.08/60.07 [u()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__u()] 217.08/60.07 217.08/60.07 217.08/60.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.07 217.08/60.07 We are left with following problem, upon which TcT provides the 217.08/60.07 certificate MAYBE. 217.08/60.07 217.08/60.07 Strict Trs: 217.08/60.07 { __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.07 , nil() -> n__nil() 217.08/60.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.07 , isList(V) -> isNeList(activate(V)) 217.08/60.07 , isList(X) -> n__isList(X) 217.08/60.07 , isNeList(V) -> isQid(activate(V)) 217.08/60.07 , isNeList(X) -> n__isNeList(X) 217.08/60.07 , isPal(X) -> n__isPal(X) } 217.08/60.07 Weak Trs: 217.08/60.07 { __(X1, X2) -> n____(X1, X2) 217.08/60.07 , __(X, nil()) -> X 217.08/60.07 , __(nil(), X) -> X 217.08/60.07 , and(tt(), X) -> activate(X) 217.08/60.07 , activate(X) -> X 217.08/60.07 , activate(n__nil()) -> nil() 217.08/60.07 , activate(n__isList(X)) -> isList(X) 217.08/60.07 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.07 , activate(n__isPal(X)) -> isPal(X) 217.08/60.07 , activate(n__a()) -> a() 217.08/60.07 , activate(n__e()) -> e() 217.08/60.07 , activate(n__i()) -> i() 217.08/60.07 , activate(n__o()) -> o() 217.08/60.07 , activate(n__u()) -> u() 217.08/60.07 , isList(n__nil()) -> tt() 217.08/60.07 , isList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isQid(n__a()) -> tt() 217.08/60.07 , isQid(n__e()) -> tt() 217.08/60.07 , isQid(n__i()) -> tt() 217.08/60.07 , isQid(n__o()) -> tt() 217.08/60.07 , isQid(n__u()) -> tt() 217.08/60.07 , isNePal(V) -> isQid(activate(V)) 217.08/60.07 , isNePal(n____(I, n____(P, I))) -> 217.08/60.07 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.07 , isPal(V) -> isNePal(activate(V)) 217.08/60.07 , isPal(n__nil()) -> tt() 217.08/60.07 , a() -> n__a() 217.08/60.07 , e() -> n__e() 217.08/60.07 , i() -> n__i() 217.08/60.07 , o() -> n__o() 217.08/60.07 , u() -> n__u() } 217.08/60.07 Obligation: 217.08/60.07 derivational complexity 217.08/60.07 Answer: 217.08/60.07 MAYBE 217.08/60.07 217.08/60.07 The weightgap principle applies (using the following nonconstant 217.08/60.07 growth matrix-interpretation) 217.08/60.07 217.08/60.07 TcT has computed the following triangular matrix interpretation. 217.08/60.07 Note that the diagonal of the component-wise maxima of 217.08/60.07 interpretation-entries contains no more than 1 non-zero entries. 217.08/60.07 217.08/60.07 [__](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.07 217.08/60.07 [nil] = [1] 217.08/60.07 217.08/60.07 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.07 217.08/60.07 [tt] = [2] 217.08/60.07 217.08/60.07 [activate](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isNeList](x1) = [1] x1 + [1] 217.08/60.07 217.08/60.07 [n__nil] = [2] 217.08/60.07 217.08/60.07 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.07 217.08/60.07 [n__isList](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isQid](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__isNeList](x1) = [1] x1 + [1] 217.08/60.07 217.08/60.07 [isNePal](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__isPal](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [isPal](x1) = [1] x1 + [0] 217.08/60.07 217.08/60.07 [n__a] = [2] 217.08/60.07 217.08/60.07 [n__e] = [2] 217.08/60.07 217.08/60.07 [n__i] = [2] 217.08/60.07 217.08/60.07 [n__o] = [2] 217.08/60.07 217.08/60.07 [n__u] = [2] 217.08/60.07 217.08/60.07 [a] = [2] 217.08/60.07 217.08/60.07 [e] = [2] 217.08/60.07 217.08/60.07 [i] = [2] 217.08/60.07 217.08/60.07 [o] = [2] 217.08/60.07 217.08/60.07 [u] = [2] 217.08/60.07 217.08/60.07 The order satisfies the following ordering constraints: 217.08/60.07 217.08/60.07 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 217.08/60.07 >= [1] X1 + [1] X2 + [0] 217.08/60.07 = [n____(X1, X2)] 217.08/60.07 217.08/60.07 [__(X, nil())] = [1] X + [1] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] 217.08/60.07 >= [1] X + [1] Y + [1] Z + [0] 217.08/60.07 = [__(X, __(Y, Z))] 217.08/60.07 217.08/60.07 [__(nil(), X)] = [1] X + [1] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [nil()] = [1] 217.08/60.07 ? [2] 217.08/60.07 = [n__nil()] 217.08/60.07 217.08/60.07 [and(tt(), X)] = [1] X + [2] 217.08/60.07 > [1] X + [0] 217.08/60.07 = [activate(X)] 217.08/60.07 217.08/60.07 [activate(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [X] 217.08/60.07 217.08/60.07 [activate(n__nil())] = [2] 217.08/60.07 > [1] 217.08/60.07 = [nil()] 217.08/60.07 217.08/60.07 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 217.08/60.07 >= [1] X1 + [1] X2 + [0] 217.08/60.07 = [__(activate(X1), activate(X2))] 217.08/60.07 217.08/60.07 [activate(n__isList(X))] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [isList(X)] 217.08/60.07 217.08/60.07 [activate(n__isNeList(X))] = [1] X + [1] 217.08/60.07 >= [1] X + [1] 217.08/60.07 = [isNeList(X)] 217.08/60.07 217.08/60.07 [activate(n__isPal(X))] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [isPal(X)] 217.08/60.07 217.08/60.07 [activate(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [a()] 217.08/60.07 217.08/60.07 [activate(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [e()] 217.08/60.07 217.08/60.07 [activate(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [i()] 217.08/60.07 217.08/60.07 [activate(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [o()] 217.08/60.07 217.08/60.07 [activate(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [u()] 217.08/60.07 217.08/60.07 [isList(V)] = [1] V + [0] 217.08/60.07 ? [1] V + [1] 217.08/60.07 = [isNeList(activate(V))] 217.08/60.07 217.08/60.07 [isList(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isList(X)] 217.08/60.07 217.08/60.07 [isList(n__nil())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0] 217.08/60.07 >= [1] V1 + [1] V2 + [0] 217.08/60.07 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(V)] = [1] V + [1] 217.08/60.07 > [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNeList(X)] = [1] X + [1] 217.08/60.07 >= [1] X + [1] 217.08/60.07 = [n__isNeList(X)] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 >= [1] V1 + [1] V2 + [1] 217.08/60.07 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.07 217.08/60.07 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1] 217.08/60.07 >= [1] V1 + [1] V2 + [1] 217.08/60.07 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.07 217.08/60.07 [isQid(n__a())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__e())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__i())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__o())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isQid(n__u())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [isNePal(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isQid(activate(V))] 217.08/60.07 217.08/60.07 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [0] 217.08/60.07 >= [1] I + [1] P + [0] 217.08/60.07 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.07 217.08/60.07 [isPal(V)] = [1] V + [0] 217.08/60.07 >= [1] V + [0] 217.08/60.07 = [isNePal(activate(V))] 217.08/60.07 217.08/60.07 [isPal(X)] = [1] X + [0] 217.08/60.07 >= [1] X + [0] 217.08/60.07 = [n__isPal(X)] 217.08/60.07 217.08/60.07 [isPal(n__nil())] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [tt()] 217.08/60.07 217.08/60.07 [a()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__a()] 217.08/60.07 217.08/60.07 [e()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__e()] 217.08/60.07 217.08/60.07 [i()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__i()] 217.08/60.07 217.08/60.07 [o()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__o()] 217.08/60.07 217.08/60.07 [u()] = [2] 217.08/60.07 >= [2] 217.08/60.07 = [n__u()] 217.08/60.07 217.08/60.07 217.08/60.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 217.08/60.07 217.08/60.07 We are left with following problem, upon which TcT provides the 217.08/60.07 certificate MAYBE. 217.08/60.07 217.08/60.07 Strict Trs: 217.08/60.07 { __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.07 , nil() -> n__nil() 217.08/60.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.07 , isList(V) -> isNeList(activate(V)) 217.08/60.07 , isList(X) -> n__isList(X) 217.08/60.07 , isNeList(X) -> n__isNeList(X) 217.08/60.07 , isPal(X) -> n__isPal(X) } 217.08/60.07 Weak Trs: 217.08/60.07 { __(X1, X2) -> n____(X1, X2) 217.08/60.07 , __(X, nil()) -> X 217.08/60.07 , __(nil(), X) -> X 217.08/60.07 , and(tt(), X) -> activate(X) 217.08/60.07 , activate(X) -> X 217.08/60.07 , activate(n__nil()) -> nil() 217.08/60.07 , activate(n__isList(X)) -> isList(X) 217.08/60.07 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.07 , activate(n__isPal(X)) -> isPal(X) 217.08/60.07 , activate(n__a()) -> a() 217.08/60.07 , activate(n__e()) -> e() 217.08/60.07 , activate(n__i()) -> i() 217.08/60.07 , activate(n__o()) -> o() 217.08/60.07 , activate(n__u()) -> u() 217.08/60.07 , isList(n__nil()) -> tt() 217.08/60.07 , isList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isNeList(V) -> isQid(activate(V)) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.07 , isNeList(n____(V1, V2)) -> 217.08/60.07 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.07 , isQid(n__a()) -> tt() 217.08/60.07 , isQid(n__e()) -> tt() 217.08/60.07 , isQid(n__i()) -> tt() 217.08/60.07 , isQid(n__o()) -> tt() 217.08/60.07 , isQid(n__u()) -> tt() 217.08/60.07 , isNePal(V) -> isQid(activate(V)) 217.08/60.07 , isNePal(n____(I, n____(P, I))) -> 217.08/60.07 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.07 , isPal(V) -> isNePal(activate(V)) 217.08/60.07 , isPal(n__nil()) -> tt() 217.08/60.07 , a() -> n__a() 217.08/60.07 , e() -> n__e() 217.08/60.07 , i() -> n__i() 217.08/60.07 , o() -> n__o() 217.08/60.07 , u() -> n__u() } 217.08/60.07 Obligation: 217.08/60.07 derivational complexity 217.08/60.07 Answer: 217.08/60.07 MAYBE 217.08/60.07 217.08/60.07 We use the processor 'matrix interpretation of dimension 1' to 217.08/60.07 orient following rules strictly. 217.08/60.07 217.08/60.07 Trs: { isList(V) -> isNeList(activate(V)) } 217.08/60.07 217.08/60.07 The induced complexity on above rules (modulo remaining rules) is 217.08/60.07 YES(?,O(n^1)) . These rules are moved into the corresponding weak 217.08/60.08 component(s). 217.08/60.08 217.08/60.08 Sub-proof: 217.08/60.08 ---------- 217.08/60.08 TcT has computed the following triangular matrix interpretation. 217.08/60.08 217.08/60.08 [__](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.08 217.08/60.08 [nil] = [2] 217.08/60.08 217.08/60.08 [and](x1, x2) = [1] x1 + [1] x2 + [0] 217.08/60.08 217.08/60.08 [tt] = [1] 217.08/60.08 217.08/60.08 [activate](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [isList](x1) = [1] x1 + [1] 217.08/60.08 217.08/60.08 [isNeList](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [n__nil] = [2] 217.08/60.08 217.08/60.08 [n____](x1, x2) = [1] x1 + [1] x2 + [2] 217.08/60.08 217.08/60.08 [n__isList](x1) = [1] x1 + [1] 217.08/60.08 217.08/60.08 [isQid](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [n__isNeList](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [isNePal](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [n__isPal](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [isPal](x1) = [1] x1 + [0] 217.08/60.08 217.08/60.08 [n__a] = [2] 217.08/60.08 217.08/60.08 [n__e] = [2] 217.08/60.08 217.08/60.08 [n__i] = [2] 217.08/60.08 217.08/60.08 [n__o] = [2] 217.08/60.08 217.08/60.08 [n__u] = [2] 217.08/60.08 217.08/60.08 [a] = [2] 217.08/60.08 217.08/60.08 [e] = [2] 217.08/60.08 217.08/60.08 [i] = [2] 217.08/60.08 217.08/60.08 [o] = [2] 217.08/60.08 217.08/60.08 [u] = [2] 217.08/60.08 217.08/60.08 The order satisfies the following ordering constraints: 217.08/60.08 217.08/60.08 [__(X1, X2)] = [1] X1 + [1] X2 + [2] 217.08/60.08 >= [1] X1 + [1] X2 + [2] 217.08/60.08 = [n____(X1, X2)] 217.08/60.08 217.08/60.08 [__(X, nil())] = [1] X + [4] 217.08/60.08 > [1] X + [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [4] 217.08/60.08 >= [1] X + [1] Y + [1] Z + [4] 217.08/60.08 = [__(X, __(Y, Z))] 217.08/60.08 217.08/60.08 [__(nil(), X)] = [1] X + [4] 217.08/60.08 > [1] X + [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [nil()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__nil()] 217.08/60.08 217.08/60.08 [and(tt(), X)] = [1] X + [1] 217.08/60.08 > [1] X + [0] 217.08/60.08 = [activate(X)] 217.08/60.08 217.08/60.08 [activate(X)] = [1] X + [0] 217.08/60.08 >= [1] X + [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [activate(n__nil())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [nil()] 217.08/60.08 217.08/60.08 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [2] 217.08/60.08 >= [1] X1 + [1] X2 + [2] 217.08/60.08 = [__(activate(X1), activate(X2))] 217.08/60.08 217.08/60.08 [activate(n__isList(X))] = [1] X + [1] 217.08/60.08 >= [1] X + [1] 217.08/60.08 = [isList(X)] 217.08/60.08 217.08/60.08 [activate(n__isNeList(X))] = [1] X + [0] 217.08/60.08 >= [1] X + [0] 217.08/60.08 = [isNeList(X)] 217.08/60.08 217.08/60.08 [activate(n__isPal(X))] = [1] X + [0] 217.08/60.08 >= [1] X + [0] 217.08/60.08 = [isPal(X)] 217.08/60.08 217.08/60.08 [activate(n__a())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [a()] 217.08/60.08 217.08/60.08 [activate(n__e())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [e()] 217.08/60.08 217.08/60.08 [activate(n__i())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [i()] 217.08/60.08 217.08/60.08 [activate(n__o())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [o()] 217.08/60.08 217.08/60.08 [activate(n__u())] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [u()] 217.08/60.08 217.08/60.08 [isList(V)] = [1] V + [1] 217.08/60.08 > [1] V + [0] 217.08/60.08 = [isNeList(activate(V))] 217.08/60.08 217.08/60.08 [isList(X)] = [1] X + [1] 217.08/60.08 >= [1] X + [1] 217.08/60.08 = [n__isList(X)] 217.08/60.08 217.08/60.08 [isList(n__nil())] = [3] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isList(n____(V1, V2))] = [1] V1 + [1] V2 + [3] 217.08/60.08 > [1] V1 + [1] V2 + [2] 217.08/60.08 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.08 217.08/60.08 [isNeList(V)] = [1] V + [0] 217.08/60.08 >= [1] V + [0] 217.08/60.08 = [isQid(activate(V))] 217.08/60.08 217.08/60.08 [isNeList(X)] = [1] X + [0] 217.08/60.08 >= [1] X + [0] 217.08/60.08 = [n__isNeList(X)] 217.08/60.08 217.08/60.08 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 217.08/60.08 > [1] V1 + [1] V2 + [1] 217.08/60.08 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.08 217.08/60.08 [isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [2] 217.08/60.08 > [1] V1 + [1] V2 + [1] 217.08/60.08 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.08 217.08/60.08 [isQid(n__a())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__e())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__i())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__o())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__u())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isNePal(V)] = [1] V + [0] 217.08/60.08 >= [1] V + [0] 217.08/60.08 = [isQid(activate(V))] 217.08/60.08 217.08/60.08 [isNePal(n____(I, n____(P, I)))] = [2] I + [1] P + [4] 217.08/60.08 > [1] I + [1] P + [0] 217.08/60.08 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.08 217.08/60.08 [isPal(V)] = [1] V + [0] 217.08/60.08 >= [1] V + [0] 217.08/60.08 = [isNePal(activate(V))] 217.08/60.08 217.08/60.08 [isPal(X)] = [1] X + [0] 217.08/60.08 >= [1] X + [0] 217.08/60.08 = [n__isPal(X)] 217.08/60.08 217.08/60.08 [isPal(n__nil())] = [2] 217.08/60.08 > [1] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [a()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__a()] 217.08/60.08 217.08/60.08 [e()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__e()] 217.08/60.08 217.08/60.08 [i()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__i()] 217.08/60.08 217.08/60.08 [o()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__o()] 217.08/60.08 217.08/60.08 [u()] = [2] 217.08/60.08 >= [2] 217.08/60.08 = [n__u()] 217.08/60.08 217.08/60.08 217.08/60.08 We return to the main proof. 217.08/60.08 217.08/60.08 We are left with following problem, upon which TcT provides the 217.08/60.08 certificate MAYBE. 217.08/60.08 217.08/60.08 Strict Trs: 217.08/60.08 { __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.08 , nil() -> n__nil() 217.08/60.08 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.08 , isList(X) -> n__isList(X) 217.08/60.08 , isNeList(X) -> n__isNeList(X) 217.08/60.08 , isPal(X) -> n__isPal(X) } 217.08/60.08 Weak Trs: 217.08/60.08 { __(X1, X2) -> n____(X1, X2) 217.08/60.08 , __(X, nil()) -> X 217.08/60.08 , __(nil(), X) -> X 217.08/60.08 , and(tt(), X) -> activate(X) 217.08/60.08 , activate(X) -> X 217.08/60.08 , activate(n__nil()) -> nil() 217.08/60.08 , activate(n__isList(X)) -> isList(X) 217.08/60.08 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.08 , activate(n__isPal(X)) -> isPal(X) 217.08/60.08 , activate(n__a()) -> a() 217.08/60.08 , activate(n__e()) -> e() 217.08/60.08 , activate(n__i()) -> i() 217.08/60.08 , activate(n__o()) -> o() 217.08/60.08 , activate(n__u()) -> u() 217.08/60.08 , isList(V) -> isNeList(activate(V)) 217.08/60.08 , isList(n__nil()) -> tt() 217.08/60.08 , isList(n____(V1, V2)) -> 217.08/60.08 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.08 , isNeList(V) -> isQid(activate(V)) 217.08/60.08 , isNeList(n____(V1, V2)) -> 217.08/60.08 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.08 , isNeList(n____(V1, V2)) -> 217.08/60.08 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.08 , isQid(n__a()) -> tt() 217.08/60.08 , isQid(n__e()) -> tt() 217.08/60.08 , isQid(n__i()) -> tt() 217.08/60.08 , isQid(n__o()) -> tt() 217.08/60.08 , isQid(n__u()) -> tt() 217.08/60.08 , isNePal(V) -> isQid(activate(V)) 217.08/60.08 , isNePal(n____(I, n____(P, I))) -> 217.08/60.08 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.08 , isPal(V) -> isNePal(activate(V)) 217.08/60.08 , isPal(n__nil()) -> tt() 217.08/60.08 , a() -> n__a() 217.08/60.08 , e() -> n__e() 217.08/60.08 , i() -> n__i() 217.08/60.08 , o() -> n__o() 217.08/60.08 , u() -> n__u() } 217.08/60.08 Obligation: 217.08/60.08 derivational complexity 217.08/60.08 Answer: 217.08/60.08 MAYBE 217.08/60.08 217.08/60.08 We use the processor 'matrix interpretation of dimension 2' to 217.08/60.08 orient following rules strictly. 217.08/60.08 217.08/60.08 Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) } 217.08/60.08 217.08/60.08 The induced complexity on above rules (modulo remaining rules) is 217.08/60.08 YES(?,O(n^2)) . These rules are moved into the corresponding weak 217.08/60.08 component(s). 217.08/60.08 217.08/60.08 Sub-proof: 217.08/60.08 ---------- 217.08/60.08 TcT has computed the following triangular matrix interpretation. 217.08/60.08 217.08/60.08 [__](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 217.08/60.08 [nil] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 217.08/60.08 [0 0] [0 1] [0] 217.08/60.08 217.08/60.08 [tt] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [activate](x1) = [1 0] x1 + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 217.08/60.08 [isList](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [isNeList](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [n__nil] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [n____](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 217.08/60.08 [n__isList](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [isQid](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [n__isNeList](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [isNePal](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [n__isPal](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [isPal](x1) = [1 0] x1 + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 217.08/60.08 [n__a] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [n__e] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [n__i] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [n__o] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [n__u] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [a] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [e] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [i] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [o] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 [u] = [0] 217.08/60.08 [0] 217.08/60.08 217.08/60.08 The order satisfies the following ordering constraints: 217.08/60.08 217.08/60.08 [__(X1, X2)] = [1 1] X1 + [1 0] X2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 >= [1 1] X1 + [1 0] X2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 = [n____(X1, X2)] 217.08/60.08 217.08/60.08 [__(X, nil())] = [1 1] X + [0] 217.08/60.08 [0 1] [1] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [__(__(X, Y), Z)] = [1 2] X + [1 1] Y + [1 0] Z + [1] 217.08/60.08 [0 1] [0 1] [0 1] [2] 217.08/60.08 > [1 1] X + [1 1] Y + [1 0] Z + [0] 217.08/60.08 [0 1] [0 1] [0 1] [2] 217.08/60.08 = [__(X, __(Y, Z))] 217.08/60.08 217.08/60.08 [__(nil(), X)] = [1 0] X + [0] 217.08/60.08 [0 1] [1] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [nil()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__nil()] 217.08/60.08 217.08/60.08 [and(tt(), X)] = [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 = [activate(X)] 217.08/60.08 217.08/60.08 [activate(X)] = [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 1] [0] 217.08/60.08 = [X] 217.08/60.08 217.08/60.08 [activate(n__nil())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [nil()] 217.08/60.08 217.08/60.08 [activate(n____(X1, X2))] = [1 1] X1 + [1 0] X2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 >= [1 1] X1 + [1 0] X2 + [0] 217.08/60.08 [0 1] [0 1] [1] 217.08/60.08 = [__(activate(X1), activate(X2))] 217.08/60.08 217.08/60.08 [activate(n__isList(X))] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isList(X)] 217.08/60.08 217.08/60.08 [activate(n__isNeList(X))] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isNeList(X)] 217.08/60.08 217.08/60.08 [activate(n__isPal(X))] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isPal(X)] 217.08/60.08 217.08/60.08 [activate(n__a())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [a()] 217.08/60.08 217.08/60.08 [activate(n__e())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [e()] 217.08/60.08 217.08/60.08 [activate(n__i())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [i()] 217.08/60.08 217.08/60.08 [activate(n__o())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [o()] 217.08/60.08 217.08/60.08 [activate(n__u())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [u()] 217.08/60.08 217.08/60.08 [isList(V)] = [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isNeList(activate(V))] 217.08/60.08 217.08/60.08 [isList(X)] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [n__isList(X)] 217.08/60.08 217.08/60.08 [isList(n__nil())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 >= [1 0] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 = [and(isList(activate(V1)), n__isList(activate(V2)))] 217.08/60.08 217.08/60.08 [isNeList(V)] = [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isQid(activate(V))] 217.08/60.08 217.08/60.08 [isNeList(X)] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [n__isNeList(X)] 217.08/60.08 217.08/60.08 [isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 >= [1 0] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 = [and(isList(activate(V1)), n__isNeList(activate(V2)))] 217.08/60.08 217.08/60.08 [isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 >= [1 0] V1 + [1 0] V2 + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 = [and(isNeList(activate(V1)), n__isList(activate(V2)))] 217.08/60.08 217.08/60.08 [isQid(n__a())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__e())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__i())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__o())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isQid(n__u())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [isNePal(V)] = [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isQid(activate(V))] 217.08/60.08 217.08/60.08 [isNePal(n____(I, n____(P, I)))] = [2 1] I + [1 1] P + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 >= [1 0] I + [1 0] P + [0] 217.08/60.08 [0 0] [0 0] [0] 217.08/60.08 = [and(isQid(activate(I)), n__isPal(activate(P)))] 217.08/60.08 217.08/60.08 [isPal(V)] = [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] V + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [isNePal(activate(V))] 217.08/60.08 217.08/60.08 [isPal(X)] = [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 >= [1 0] X + [0] 217.08/60.08 [0 0] [0] 217.08/60.08 = [n__isPal(X)] 217.08/60.08 217.08/60.08 [isPal(n__nil())] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [tt()] 217.08/60.08 217.08/60.08 [a()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__a()] 217.08/60.08 217.08/60.08 [e()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__e()] 217.08/60.08 217.08/60.08 [i()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__i()] 217.08/60.08 217.08/60.08 [o()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__o()] 217.08/60.08 217.08/60.08 [u()] = [0] 217.08/60.08 [0] 217.08/60.08 >= [0] 217.08/60.08 [0] 217.08/60.08 = [n__u()] 217.08/60.08 217.08/60.08 217.08/60.08 We return to the main proof. 217.08/60.08 217.08/60.08 We are left with following problem, upon which TcT provides the 217.08/60.08 certificate MAYBE. 217.08/60.08 217.08/60.08 Strict Trs: 217.08/60.08 { nil() -> n__nil() 217.08/60.08 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 217.08/60.08 , isList(X) -> n__isList(X) 217.08/60.08 , isNeList(X) -> n__isNeList(X) 217.08/60.08 , isPal(X) -> n__isPal(X) } 217.08/60.08 Weak Trs: 217.08/60.08 { __(X1, X2) -> n____(X1, X2) 217.08/60.08 , __(X, nil()) -> X 217.08/60.08 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 217.08/60.08 , __(nil(), X) -> X 217.08/60.08 , and(tt(), X) -> activate(X) 217.08/60.08 , activate(X) -> X 217.08/60.08 , activate(n__nil()) -> nil() 217.08/60.08 , activate(n__isList(X)) -> isList(X) 217.08/60.08 , activate(n__isNeList(X)) -> isNeList(X) 217.08/60.08 , activate(n__isPal(X)) -> isPal(X) 217.08/60.08 , activate(n__a()) -> a() 217.08/60.08 , activate(n__e()) -> e() 217.08/60.08 , activate(n__i()) -> i() 217.08/60.08 , activate(n__o()) -> o() 217.08/60.08 , activate(n__u()) -> u() 217.08/60.08 , isList(V) -> isNeList(activate(V)) 217.08/60.08 , isList(n__nil()) -> tt() 217.08/60.08 , isList(n____(V1, V2)) -> 217.08/60.08 and(isList(activate(V1)), n__isList(activate(V2))) 217.08/60.08 , isNeList(V) -> isQid(activate(V)) 217.08/60.08 , isNeList(n____(V1, V2)) -> 217.08/60.08 and(isList(activate(V1)), n__isNeList(activate(V2))) 217.08/60.08 , isNeList(n____(V1, V2)) -> 217.08/60.08 and(isNeList(activate(V1)), n__isList(activate(V2))) 217.08/60.08 , isQid(n__a()) -> tt() 217.08/60.08 , isQid(n__e()) -> tt() 217.08/60.08 , isQid(n__i()) -> tt() 217.08/60.08 , isQid(n__o()) -> tt() 217.08/60.08 , isQid(n__u()) -> tt() 217.08/60.08 , isNePal(V) -> isQid(activate(V)) 217.08/60.08 , isNePal(n____(I, n____(P, I))) -> 217.08/60.08 and(isQid(activate(I)), n__isPal(activate(P))) 217.08/60.08 , isPal(V) -> isNePal(activate(V)) 217.08/60.08 , isPal(n__nil()) -> tt() 217.08/60.08 , a() -> n__a() 217.08/60.08 , e() -> n__e() 217.08/60.08 , i() -> n__i() 217.08/60.08 , o() -> n__o() 217.08/60.08 , u() -> n__u() } 217.08/60.08 Obligation: 217.08/60.08 derivational complexity 217.08/60.08 Answer: 217.08/60.08 MAYBE 217.08/60.08 217.08/60.08 None of the processors succeeded. 217.08/60.08 217.08/60.08 Details of failed attempt(s): 217.08/60.08 ----------------------------- 217.08/60.08 1) 'empty' failed due to the following reason: 217.08/60.08 217.08/60.08 Empty strict component of the problem is NOT empty. 217.08/60.08 217.08/60.08 2) 'Fastest' failed due to the following reason: 217.08/60.08 217.08/60.08 None of the processors succeeded. 217.08/60.08 217.08/60.08 Details of failed attempt(s): 217.08/60.08 ----------------------------- 217.08/60.08 1) 'Fastest' failed due to the following reason: 217.08/60.08 217.08/60.08 None of the processors succeeded. 217.08/60.08 217.08/60.08 Details of failed attempt(s): 217.08/60.08 ----------------------------- 217.08/60.08 1) 'matrix interpretation of dimension 6' failed due to the 217.08/60.08 following reason: 217.08/60.08 217.08/60.08 The input cannot be shown compatible 217.08/60.08 217.08/60.08 2) 'matrix interpretation of dimension 5' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 3) 'matrix interpretation of dimension 4' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 4) 'matrix interpretation of dimension 3' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 5) 'matrix interpretation of dimension 2' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 6) 'matrix interpretation of dimension 1' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 217.08/60.09 2) 'Fastest (timeout of 30 seconds)' failed due to the following 217.08/60.09 reason: 217.08/60.09 217.08/60.09 Computation stopped due to timeout after 30.0 seconds. 217.08/60.09 217.08/60.09 3) 'iteProgress' failed due to the following reason: 217.08/60.09 217.08/60.09 Fail 217.08/60.09 217.08/60.09 4) 'bsearch-matrix' failed due to the following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 217.08/60.09 217.08/60.09 3) 'iteProgress (timeout of 297 seconds)' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 Fail 217.08/60.09 217.08/60.09 4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 217.08/60.09 following reason: 217.08/60.09 217.08/60.09 The input cannot be shown compatible 217.08/60.09 217.08/60.09 217.08/60.09 Arrrr.. 217.34/60.11 EOF