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