YES(?,O(n^2)) 31.73/11.04 YES(?,O(n^2)) 31.73/11.04 31.73/11.04 Problem: 31.73/11.04 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.04 __(X,nil()) -> X 31.73/11.04 __(nil(),X) -> X 31.73/11.04 and(tt(),X) -> activate(X) 31.73/11.04 isList(V) -> isNeList(activate(V)) 31.73/11.04 isList(n__nil()) -> tt() 31.73/11.04 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.04 isNeList(V) -> isQid(activate(V)) 31.73/11.04 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.04 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.04 isNePal(V) -> isQid(activate(V)) 31.73/11.04 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.04 isPal(V) -> isNePal(activate(V)) 31.73/11.04 isPal(n__nil()) -> tt() 31.73/11.04 isQid(n__a()) -> tt() 31.73/11.04 isQid(n__e()) -> tt() 31.73/11.04 isQid(n__i()) -> tt() 31.73/11.04 isQid(n__o()) -> tt() 31.73/11.04 isQid(n__u()) -> tt() 31.73/11.04 nil() -> n__nil() 31.73/11.04 __(X1,X2) -> n____(X1,X2) 31.73/11.04 isList(X) -> n__isList(X) 31.73/11.04 isNeList(X) -> n__isNeList(X) 31.73/11.04 isPal(X) -> n__isPal(X) 31.73/11.04 a() -> n__a() 31.73/11.04 e() -> n__e() 31.73/11.04 i() -> n__i() 31.73/11.04 o() -> n__o() 31.73/11.04 u() -> n__u() 31.73/11.04 activate(n__nil()) -> nil() 31.73/11.04 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.04 activate(n__isList(X)) -> isList(X) 31.73/11.04 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.04 activate(n__isPal(X)) -> isPal(X) 31.73/11.04 activate(n__a()) -> a() 31.73/11.04 activate(n__e()) -> e() 31.73/11.04 activate(n__i()) -> i() 31.73/11.04 activate(n__o()) -> o() 31.73/11.04 activate(n__u()) -> u() 31.73/11.04 activate(X) -> X 31.73/11.04 31.73/11.04 Proof: 31.73/11.04 Complexity Transformation Processor: 31.73/11.04 strict: 31.73/11.04 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.04 __(X,nil()) -> X 31.73/11.04 __(nil(),X) -> X 31.73/11.04 and(tt(),X) -> activate(X) 31.73/11.04 isList(V) -> isNeList(activate(V)) 31.73/11.04 isList(n__nil()) -> tt() 31.73/11.04 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.04 isNeList(V) -> isQid(activate(V)) 31.73/11.04 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.04 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.04 isNePal(V) -> isQid(activate(V)) 31.73/11.04 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.04 isPal(V) -> isNePal(activate(V)) 31.73/11.04 isPal(n__nil()) -> tt() 31.73/11.04 isQid(n__a()) -> tt() 31.73/11.04 isQid(n__e()) -> tt() 31.73/11.04 isQid(n__i()) -> tt() 31.73/11.04 isQid(n__o()) -> tt() 31.73/11.04 isQid(n__u()) -> tt() 31.73/11.04 nil() -> n__nil() 31.73/11.04 __(X1,X2) -> n____(X1,X2) 31.73/11.04 isList(X) -> n__isList(X) 31.73/11.04 isNeList(X) -> n__isNeList(X) 31.73/11.04 isPal(X) -> n__isPal(X) 31.73/11.04 a() -> n__a() 31.73/11.04 e() -> n__e() 31.73/11.04 i() -> n__i() 31.73/11.04 o() -> n__o() 31.73/11.04 u() -> n__u() 31.73/11.04 activate(n__nil()) -> nil() 31.73/11.04 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.04 activate(n__isList(X)) -> isList(X) 31.73/11.04 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.04 activate(n__isPal(X)) -> isPal(X) 31.73/11.04 activate(n__a()) -> a() 31.73/11.04 activate(n__e()) -> e() 31.73/11.04 activate(n__i()) -> i() 31.73/11.04 activate(n__o()) -> o() 31.73/11.04 activate(n__u()) -> u() 31.73/11.04 activate(X) -> X 31.73/11.04 weak: 31.73/11.04 31.73/11.04 Matrix Interpretation Processor: dim=1 31.73/11.04 31.73/11.04 max_matrix: 31.73/11.04 1 31.73/11.04 interpretation: 31.73/11.04 [u] = 0, 31.73/11.04 31.73/11.04 [o] = 0, 31.73/11.04 31.73/11.04 [i] = 0, 31.73/11.04 31.73/11.04 [e] = 0, 31.73/11.04 31.73/11.04 [a] = 0, 31.73/11.04 31.73/11.04 [n__u] = 132, 31.73/11.04 31.73/11.04 [n__o] = 24, 31.73/11.04 31.73/11.04 [n__i] = 200, 31.73/11.04 31.73/11.04 [n__e] = 20, 31.73/11.04 31.73/11.04 [n__a] = 0, 31.73/11.04 31.73/11.04 [isPal](x0) = x0 + 128, 31.73/11.04 31.73/11.04 [n__isPal](x0) = x0 + 196, 31.73/11.04 31.73/11.04 [isNePal](x0) = x0 + 146, 31.73/11.04 31.73/11.04 [n__isNeList](x0) = x0 + 184, 31.73/11.04 31.73/11.04 [isQid](x0) = x0 + 2, 31.73/11.04 31.73/11.04 [n__isList](x0) = x0 + 192, 31.73/11.04 31.73/11.04 [n____](x0, x1) = x0 + x1 + 2, 31.73/11.04 31.73/11.04 [n__nil] = 0, 31.73/11.04 31.73/11.04 [isNeList](x0) = x0 + 210, 31.73/11.04 31.73/11.04 [isList](x0) = x0 + 193, 31.73/11.04 31.73/11.04 [activate](x0) = x0 + 32, 31.73/11.04 31.73/11.04 [and](x0, x1) = x0 + x1 + 33, 31.73/11.04 31.73/11.04 [tt] = 11, 31.73/11.04 31.73/11.04 [nil] = 208, 31.73/11.04 31.73/11.04 [__](x0, x1) = x0 + x1 + 232 31.73/11.04 orientation: 31.73/11.04 __(__(X,Y),Z) = X + Y + Z + 464 >= X + Y + Z + 464 = __(X,__(Y,Z)) 31.73/11.04 31.73/11.04 __(X,nil()) = X + 440 >= X = X 31.73/11.04 31.73/11.04 __(nil(),X) = X + 440 >= X = X 31.73/11.04 31.73/11.04 and(tt(),X) = X + 44 >= X + 32 = activate(X) 31.73/11.04 31.73/11.04 isList(V) = V + 193 >= V + 242 = isNeList(activate(V)) 31.73/11.04 31.73/11.04 isList(n__nil()) = 193 >= 11 = tt() 31.73/11.04 31.73/11.04 isList(n____(V1,V2)) = V1 + V2 + 195 >= V1 + V2 + 482 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.04 31.73/11.04 isNeList(V) = V + 210 >= V + 34 = isQid(activate(V)) 31.73/11.04 31.73/11.04 isNeList(n____(V1,V2)) = V1 + V2 + 212 >= V1 + V2 + 474 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.04 31.73/11.04 isNeList(n____(V1,V2)) = V1 + V2 + 212 >= V1 + V2 + 499 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 31.73/11.05 isNePal(V) = V + 146 >= V + 34 = isQid(activate(V)) 31.73/11.05 31.73/11.05 isNePal(n____(I,__(P,I))) = 2I + P + 380 >= I + P + 295 = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.05 31.73/11.05 isPal(V) = V + 128 >= V + 178 = isNePal(activate(V)) 31.73/11.05 31.73/11.05 isPal(n__nil()) = 128 >= 11 = tt() 31.73/11.05 31.73/11.05 isQid(n__a()) = 2 >= 11 = tt() 31.73/11.05 31.73/11.05 isQid(n__e()) = 22 >= 11 = tt() 31.73/11.05 31.73/11.05 isQid(n__i()) = 202 >= 11 = tt() 31.73/11.05 31.73/11.05 isQid(n__o()) = 26 >= 11 = tt() 31.73/11.05 31.73/11.05 isQid(n__u()) = 134 >= 11 = tt() 31.73/11.05 31.73/11.05 nil() = 208 >= 0 = n__nil() 31.73/11.05 31.73/11.05 __(X1,X2) = X1 + X2 + 232 >= X1 + X2 + 2 = n____(X1,X2) 31.73/11.05 31.73/11.05 isList(X) = X + 193 >= X + 192 = n__isList(X) 31.73/11.05 31.73/11.05 isNeList(X) = X + 210 >= X + 184 = n__isNeList(X) 31.73/11.05 31.73/11.05 isPal(X) = X + 128 >= X + 196 = n__isPal(X) 31.73/11.05 31.73/11.05 a() = 0 >= 0 = n__a() 31.73/11.05 31.73/11.05 e() = 0 >= 20 = n__e() 31.73/11.05 31.73/11.05 i() = 0 >= 200 = n__i() 31.73/11.05 31.73/11.05 o() = 0 >= 24 = n__o() 31.73/11.05 31.73/11.05 u() = 0 >= 132 = n__u() 31.73/11.05 31.73/11.05 activate(n__nil()) = 32 >= 208 = nil() 31.73/11.05 31.73/11.05 activate(n____(X1,X2)) = X1 + X2 + 34 >= X1 + X2 + 232 = __(X1,X2) 31.73/11.05 31.73/11.05 activate(n__isList(X)) = X + 224 >= X + 193 = isList(X) 31.73/11.05 31.73/11.05 activate(n__isNeList(X)) = X + 216 >= X + 210 = isNeList(X) 31.73/11.05 31.73/11.05 activate(n__isPal(X)) = X + 228 >= X + 128 = isPal(X) 31.73/11.05 31.73/11.05 activate(n__a()) = 32 >= 0 = a() 31.73/11.05 31.73/11.05 activate(n__e()) = 52 >= 0 = e() 31.73/11.05 31.73/11.05 activate(n__i()) = 232 >= 0 = i() 31.73/11.05 31.73/11.05 activate(n__o()) = 56 >= 0 = o() 31.73/11.05 31.73/11.05 activate(n__u()) = 164 >= 0 = u() 31.73/11.05 31.73/11.05 activate(X) = X + 32 >= X = X 31.73/11.05 problem: 31.73/11.05 strict: 31.73/11.05 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.05 isList(V) -> isNeList(activate(V)) 31.73/11.05 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.05 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 isPal(V) -> isNePal(activate(V)) 31.73/11.05 isQid(n__a()) -> tt() 31.73/11.05 isPal(X) -> n__isPal(X) 31.73/11.05 a() -> n__a() 31.73/11.05 e() -> n__e() 31.73/11.05 i() -> n__i() 31.73/11.05 o() -> n__o() 31.73/11.05 u() -> n__u() 31.73/11.05 activate(n__nil()) -> nil() 31.73/11.05 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.05 weak: 31.73/11.05 __(X,nil()) -> X 31.73/11.05 __(nil(),X) -> X 31.73/11.05 and(tt(),X) -> activate(X) 31.73/11.05 isList(n__nil()) -> tt() 31.73/11.05 isNeList(V) -> isQid(activate(V)) 31.73/11.05 isNePal(V) -> isQid(activate(V)) 31.73/11.05 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.05 isPal(n__nil()) -> tt() 31.73/11.05 isQid(n__e()) -> tt() 31.73/11.05 isQid(n__i()) -> tt() 31.73/11.05 isQid(n__o()) -> tt() 31.73/11.05 isQid(n__u()) -> tt() 31.73/11.05 nil() -> n__nil() 31.73/11.05 __(X1,X2) -> n____(X1,X2) 31.73/11.05 isList(X) -> n__isList(X) 31.73/11.05 isNeList(X) -> n__isNeList(X) 31.73/11.05 activate(n__isList(X)) -> isList(X) 31.73/11.05 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.05 activate(n__isPal(X)) -> isPal(X) 31.73/11.05 activate(n__a()) -> a() 31.73/11.05 activate(n__e()) -> e() 31.73/11.05 activate(n__i()) -> i() 31.73/11.05 activate(n__o()) -> o() 31.73/11.05 activate(n__u()) -> u() 31.73/11.05 activate(X) -> X 31.73/11.05 Matrix Interpretation Processor: dim=1 31.73/11.05 31.73/11.05 max_matrix: 31.73/11.05 1 31.73/11.05 interpretation: 31.73/11.05 [u] = 8, 31.73/11.05 31.73/11.05 [o] = 138, 31.73/11.05 31.73/11.05 [i] = 0, 31.73/11.05 31.73/11.05 [e] = 0, 31.73/11.05 31.73/11.05 [a] = 0, 31.73/11.05 31.73/11.05 [n__u] = 0, 31.73/11.05 31.73/11.05 [n__o] = 130, 31.73/11.05 31.73/11.05 [n__i] = 0, 31.73/11.05 31.73/11.05 [n__e] = 130, 31.73/11.05 31.73/11.05 [n__a] = 0, 31.73/11.05 31.73/11.05 [isPal](x0) = x0, 31.73/11.05 31.73/11.05 [n__isPal](x0) = x0 + 2, 31.73/11.05 31.73/11.05 [isNePal](x0) = x0 + 216, 31.73/11.05 31.73/11.05 [n__isNeList](x0) = x0 + 169, 31.73/11.05 31.73/11.05 [isQid](x0) = x0 + 122, 31.73/11.05 31.73/11.05 [n__isList](x0) = x0 + 60, 31.73/11.05 31.73/11.05 [n____](x0, x1) = x0 + x1 + 8, 31.73/11.05 31.73/11.05 [n__nil] = 0, 31.73/11.05 31.73/11.05 [isNeList](x0) = x0 + 174, 31.73/11.05 31.73/11.05 [isList](x0) = x0 + 68, 31.73/11.05 31.73/11.05 [activate](x0) = x0 + 8, 31.73/11.05 31.73/11.05 [and](x0, x1) = x0 + x1 + 92, 31.73/11.05 31.73/11.05 [tt] = 0, 31.73/11.05 31.73/11.05 [nil] = 33, 31.73/11.05 31.73/11.05 [__](x0, x1) = x0 + x1 + 8 31.73/11.05 orientation: 31.73/11.05 __(__(X,Y),Z) = X + Y + Z + 16 >= X + Y + Z + 16 = __(X,__(Y,Z)) 31.73/11.05 31.73/11.05 isList(V) = V + 68 >= V + 182 = isNeList(activate(V)) 31.73/11.05 31.73/11.05 isList(n____(V1,V2)) = V1 + V2 + 76 >= V1 + V2 + 236 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 31.73/11.05 isNeList(n____(V1,V2)) = V1 + V2 + 182 >= V1 + V2 + 345 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.05 31.73/11.05 isNeList(n____(V1,V2)) = V1 + V2 + 182 >= V1 + V2 + 342 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 31.73/11.05 isPal(V) = V >= V + 224 = isNePal(activate(V)) 31.73/11.05 31.73/11.05 isQid(n__a()) = 122 >= 0 = tt() 31.73/11.05 31.73/11.05 isPal(X) = X >= X + 2 = n__isPal(X) 31.73/11.05 31.73/11.05 a() = 0 >= 0 = n__a() 31.73/11.05 31.73/11.05 e() = 0 >= 130 = n__e() 31.73/11.05 31.73/11.05 i() = 0 >= 0 = n__i() 31.73/11.05 31.73/11.05 o() = 138 >= 130 = n__o() 31.73/11.05 31.73/11.05 u() = 8 >= 0 = n__u() 31.73/11.05 31.73/11.05 activate(n__nil()) = 8 >= 33 = nil() 31.73/11.05 31.73/11.05 activate(n____(X1,X2)) = X1 + X2 + 16 >= X1 + X2 + 8 = __(X1,X2) 31.73/11.05 31.73/11.05 __(X,nil()) = X + 41 >= X = X 31.73/11.05 31.73/11.05 __(nil(),X) = X + 41 >= X = X 31.73/11.05 31.73/11.05 and(tt(),X) = X + 92 >= X + 8 = activate(X) 31.73/11.05 31.73/11.05 isList(n__nil()) = 68 >= 0 = tt() 31.73/11.05 31.73/11.05 isNeList(V) = V + 174 >= V + 130 = isQid(activate(V)) 31.73/11.05 31.73/11.05 isNePal(V) = V + 216 >= V + 130 = isQid(activate(V)) 31.73/11.05 31.73/11.05 isNePal(n____(I,__(P,I))) = 2I + P + 232 >= I + P + 232 = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.05 31.73/11.05 isPal(n__nil()) = 0 >= 0 = tt() 31.73/11.05 31.73/11.05 isQid(n__e()) = 252 >= 0 = tt() 31.73/11.05 31.73/11.05 isQid(n__i()) = 122 >= 0 = tt() 31.73/11.05 31.73/11.05 isQid(n__o()) = 252 >= 0 = tt() 31.73/11.05 31.73/11.05 isQid(n__u()) = 122 >= 0 = tt() 31.73/11.05 31.73/11.05 nil() = 33 >= 0 = n__nil() 31.73/11.05 31.73/11.05 __(X1,X2) = X1 + X2 + 8 >= X1 + X2 + 8 = n____(X1,X2) 31.73/11.05 31.73/11.05 isList(X) = X + 68 >= X + 60 = n__isList(X) 31.73/11.05 31.73/11.05 isNeList(X) = X + 174 >= X + 169 = n__isNeList(X) 31.73/11.05 31.73/11.05 activate(n__isList(X)) = X + 68 >= X + 68 = isList(X) 31.73/11.05 31.73/11.05 activate(n__isNeList(X)) = X + 177 >= X + 174 = isNeList(X) 31.73/11.05 31.73/11.05 activate(n__isPal(X)) = X + 10 >= X = isPal(X) 31.73/11.05 31.73/11.05 activate(n__a()) = 8 >= 0 = a() 31.73/11.05 31.73/11.05 activate(n__e()) = 138 >= 0 = e() 31.73/11.05 31.73/11.05 activate(n__i()) = 8 >= 0 = i() 31.73/11.05 31.73/11.05 activate(n__o()) = 138 >= 138 = o() 31.73/11.05 31.73/11.05 activate(n__u()) = 8 >= 8 = u() 31.73/11.05 31.73/11.05 activate(X) = X + 8 >= X = X 31.73/11.05 problem: 31.73/11.05 strict: 31.73/11.05 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.05 isList(V) -> isNeList(activate(V)) 31.73/11.05 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.05 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 isPal(V) -> isNePal(activate(V)) 31.73/11.05 isPal(X) -> n__isPal(X) 31.73/11.05 a() -> n__a() 31.73/11.05 e() -> n__e() 31.73/11.05 i() -> n__i() 31.73/11.05 activate(n__nil()) -> nil() 31.73/11.05 weak: 31.73/11.05 isQid(n__a()) -> tt() 31.73/11.05 o() -> n__o() 31.73/11.05 u() -> n__u() 31.73/11.05 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.05 __(X,nil()) -> X 31.73/11.05 __(nil(),X) -> X 31.73/11.05 and(tt(),X) -> activate(X) 31.73/11.05 isList(n__nil()) -> tt() 31.73/11.05 isNeList(V) -> isQid(activate(V)) 31.73/11.05 isNePal(V) -> isQid(activate(V)) 31.73/11.05 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.05 isPal(n__nil()) -> tt() 31.73/11.05 isQid(n__e()) -> tt() 31.73/11.05 isQid(n__i()) -> tt() 31.73/11.05 isQid(n__o()) -> tt() 31.73/11.05 isQid(n__u()) -> tt() 31.73/11.05 nil() -> n__nil() 31.73/11.05 __(X1,X2) -> n____(X1,X2) 31.73/11.05 isList(X) -> n__isList(X) 31.73/11.05 isNeList(X) -> n__isNeList(X) 31.73/11.05 activate(n__isList(X)) -> isList(X) 31.73/11.05 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.05 activate(n__isPal(X)) -> isPal(X) 31.73/11.05 activate(n__a()) -> a() 31.73/11.05 activate(n__e()) -> e() 31.73/11.05 activate(n__i()) -> i() 31.73/11.05 activate(n__o()) -> o() 31.73/11.05 activate(n__u()) -> u() 31.73/11.05 activate(X) -> X 31.73/11.05 Matrix Interpretation Processor: dim=1 31.73/11.05 31.73/11.05 max_matrix: 31.73/11.05 1 31.73/11.05 interpretation: 31.73/11.05 [u] = 0, 31.73/11.05 31.73/11.05 [o] = 16, 31.73/11.05 31.73/11.05 [i] = 0, 31.73/11.05 31.73/11.05 [e] = 0, 31.73/11.05 31.73/11.05 [a] = 0, 31.73/11.05 31.73/11.05 [n__u] = 0, 31.73/11.05 31.73/11.05 [n__o] = 16, 31.73/11.05 31.73/11.05 [n__i] = 22, 31.73/11.05 31.73/11.05 [n__e] = 0, 31.73/11.05 31.73/11.05 [n__a] = 2, 31.73/11.05 31.73/11.05 [isPal](x0) = x0 + 130, 31.73/11.05 31.73/11.05 [n__isPal](x0) = x0 + 208, 31.73/11.05 31.73/11.05 [isNePal](x0) = x0 + 68, 31.73/11.05 31.73/11.05 [n__isNeList](x0) = x0 + 68, 31.73/11.05 31.73/11.05 [isQid](x0) = x0 + 68, 31.73/11.05 31.73/11.05 [n__isList](x0) = x0, 31.73/11.05 31.73/11.05 [n____](x0, x1) = x0 + x1 + 128, 31.73/11.05 31.73/11.05 [n__nil] = 64, 31.73/11.05 31.73/11.05 [isNeList](x0) = x0 + 68, 31.73/11.05 31.73/11.05 [isList](x0) = x0, 31.73/11.05 31.73/11.05 [activate](x0) = x0, 31.73/11.05 31.73/11.05 [and](x0, x1) = x0 + x1 + 4, 31.73/11.05 31.73/11.05 [tt] = 64, 31.73/11.05 31.73/11.05 [nil] = 64, 31.73/11.05 31.73/11.05 [__](x0, x1) = x0 + x1 + 128 31.73/11.05 orientation: 31.73/11.05 __(__(X,Y),Z) = X + Y + Z + 256 >= X + Y + Z + 256 = __(X,__(Y,Z)) 31.73/11.05 31.73/11.05 isList(V) = V >= V + 68 = isNeList(activate(V)) 31.73/11.05 31.73/11.05 isList(n____(V1,V2)) = V1 + V2 + 128 >= V1 + V2 + 4 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 31.73/11.05 isNeList(n____(V1,V2)) = V1 + V2 + 196 >= V1 + V2 + 72 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.05 31.73/11.05 isNeList(n____(V1,V2)) = V1 + V2 + 196 >= V1 + V2 + 72 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.05 31.73/11.05 isPal(V) = V + 130 >= V + 68 = isNePal(activate(V)) 31.73/11.05 31.73/11.05 isPal(X) = X + 130 >= X + 208 = n__isPal(X) 31.73/11.05 31.73/11.05 a() = 0 >= 2 = n__a() 31.73/11.05 31.73/11.05 e() = 0 >= 0 = n__e() 31.73/11.05 31.73/11.05 i() = 0 >= 22 = n__i() 31.73/11.05 31.73/11.05 activate(n__nil()) = 64 >= 64 = nil() 31.73/11.05 31.73/11.05 isQid(n__a()) = 70 >= 64 = tt() 31.73/11.06 31.73/11.06 o() = 16 >= 16 = n__o() 31.73/11.06 31.73/11.06 u() = 0 >= 0 = n__u() 31.73/11.06 31.73/11.06 activate(n____(X1,X2)) = X1 + X2 + 128 >= X1 + X2 + 128 = __(X1,X2) 31.73/11.06 31.73/11.06 __(X,nil()) = X + 192 >= X = X 31.73/11.06 31.73/11.06 __(nil(),X) = X + 192 >= X = X 31.73/11.06 31.73/11.06 and(tt(),X) = X + 68 >= X = activate(X) 31.73/11.06 31.73/11.06 isList(n__nil()) = 64 >= 64 = tt() 31.73/11.06 31.73/11.06 isNeList(V) = V + 68 >= V + 68 = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(V) = V + 68 >= V + 68 = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(n____(I,__(P,I))) = 2I + P + 324 >= I + P + 280 = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.06 31.73/11.06 isPal(n__nil()) = 194 >= 64 = tt() 31.73/11.06 31.73/11.06 isQid(n__e()) = 68 >= 64 = tt() 31.73/11.06 31.73/11.06 isQid(n__i()) = 90 >= 64 = tt() 31.73/11.06 31.73/11.06 isQid(n__o()) = 84 >= 64 = tt() 31.73/11.06 31.73/11.06 isQid(n__u()) = 68 >= 64 = tt() 31.73/11.06 31.73/11.06 nil() = 64 >= 64 = n__nil() 31.73/11.06 31.73/11.06 __(X1,X2) = X1 + X2 + 128 >= X1 + X2 + 128 = n____(X1,X2) 31.73/11.06 31.73/11.06 isList(X) = X >= X = n__isList(X) 31.73/11.06 31.73/11.06 isNeList(X) = X + 68 >= X + 68 = n__isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isList(X)) = X >= X = isList(X) 31.73/11.06 31.73/11.06 activate(n__isNeList(X)) = X + 68 >= X + 68 = isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isPal(X)) = X + 208 >= X + 130 = isPal(X) 31.73/11.06 31.73/11.06 activate(n__a()) = 2 >= 0 = a() 31.73/11.06 31.73/11.06 activate(n__e()) = 0 >= 0 = e() 31.73/11.06 31.73/11.06 activate(n__i()) = 22 >= 0 = i() 31.73/11.06 31.73/11.06 activate(n__o()) = 16 >= 16 = o() 31.73/11.06 31.73/11.06 activate(n__u()) = 0 >= 0 = u() 31.73/11.06 31.73/11.06 activate(X) = X >= X = X 31.73/11.06 problem: 31.73/11.06 strict: 31.73/11.06 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.06 isList(V) -> isNeList(activate(V)) 31.73/11.06 isPal(X) -> n__isPal(X) 31.73/11.06 a() -> n__a() 31.73/11.06 e() -> n__e() 31.73/11.06 i() -> n__i() 31.73/11.06 activate(n__nil()) -> nil() 31.73/11.06 weak: 31.73/11.06 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.06 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 isPal(V) -> isNePal(activate(V)) 31.73/11.06 isQid(n__a()) -> tt() 31.73/11.06 o() -> n__o() 31.73/11.06 u() -> n__u() 31.73/11.06 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.06 __(X,nil()) -> X 31.73/11.06 __(nil(),X) -> X 31.73/11.06 and(tt(),X) -> activate(X) 31.73/11.06 isList(n__nil()) -> tt() 31.73/11.06 isNeList(V) -> isQid(activate(V)) 31.73/11.06 isNePal(V) -> isQid(activate(V)) 31.73/11.06 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.06 isPal(n__nil()) -> tt() 31.73/11.06 isQid(n__e()) -> tt() 31.73/11.06 isQid(n__i()) -> tt() 31.73/11.06 isQid(n__o()) -> tt() 31.73/11.06 isQid(n__u()) -> tt() 31.73/11.06 nil() -> n__nil() 31.73/11.06 __(X1,X2) -> n____(X1,X2) 31.73/11.06 isList(X) -> n__isList(X) 31.73/11.06 isNeList(X) -> n__isNeList(X) 31.73/11.06 activate(n__isList(X)) -> isList(X) 31.73/11.06 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.06 activate(n__isPal(X)) -> isPal(X) 31.73/11.06 activate(n__a()) -> a() 31.73/11.06 activate(n__e()) -> e() 31.73/11.06 activate(n__i()) -> i() 31.73/11.06 activate(n__o()) -> o() 31.73/11.06 activate(n__u()) -> u() 31.73/11.06 activate(X) -> X 31.73/11.06 Matrix Interpretation Processor: dim=1 31.73/11.06 31.73/11.06 max_matrix: 31.73/11.06 1 31.73/11.06 interpretation: 31.73/11.06 [u] = 2, 31.73/11.06 31.73/11.06 [o] = 0, 31.73/11.06 31.73/11.06 [i] = 1, 31.73/11.06 31.73/11.06 [e] = 10, 31.73/11.06 31.73/11.06 [a] = 0, 31.73/11.06 31.73/11.06 [n__u] = 2, 31.73/11.06 31.73/11.06 [n__o] = 0, 31.73/11.06 31.73/11.06 [n__i] = 1, 31.73/11.06 31.73/11.06 [n__e] = 10, 31.73/11.06 31.73/11.06 [n__a] = 0, 31.73/11.06 31.73/11.06 [isPal](x0) = x0, 31.73/11.06 31.73/11.06 [n__isPal](x0) = x0, 31.73/11.06 31.73/11.06 [isNePal](x0) = x0, 31.73/11.06 31.73/11.06 [n__isNeList](x0) = x0, 31.73/11.06 31.73/11.06 [isQid](x0) = x0, 31.73/11.06 31.73/11.06 [n__isList](x0) = x0 + 8, 31.73/11.06 31.73/11.06 [n____](x0, x1) = x0 + x1 + 8, 31.73/11.06 31.73/11.06 [n__nil] = 0, 31.73/11.06 31.73/11.06 [isNeList](x0) = x0, 31.73/11.06 31.73/11.06 [isList](x0) = x0 + 8, 31.73/11.06 31.73/11.06 [activate](x0) = x0, 31.73/11.06 31.73/11.06 [and](x0, x1) = x0 + x1, 31.73/11.06 31.73/11.06 [tt] = 0, 31.73/11.06 31.73/11.06 [nil] = 0, 31.73/11.06 31.73/11.06 [__](x0, x1) = x0 + x1 + 8 31.73/11.06 orientation: 31.73/11.06 __(__(X,Y),Z) = X + Y + Z + 16 >= X + Y + Z + 16 = __(X,__(Y,Z)) 31.73/11.06 31.73/11.06 isList(V) = V + 8 >= V = isNeList(activate(V)) 31.73/11.06 31.73/11.06 isPal(X) = X >= X = n__isPal(X) 31.73/11.06 31.73/11.06 a() = 0 >= 0 = n__a() 31.73/11.06 31.73/11.06 e() = 10 >= 10 = n__e() 31.73/11.06 31.73/11.06 i() = 1 >= 1 = n__i() 31.73/11.06 31.73/11.06 activate(n__nil()) = 0 >= 0 = nil() 31.73/11.06 31.73/11.06 isList(n____(V1,V2)) = V1 + V2 + 16 >= V1 + V2 + 16 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 31.73/11.06 isNeList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 + 8 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.06 31.73/11.06 isNeList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 + 8 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 31.73/11.06 isPal(V) = V >= V = isNePal(activate(V)) 31.73/11.06 31.73/11.06 isQid(n__a()) = 0 >= 0 = tt() 31.73/11.06 31.73/11.06 o() = 0 >= 0 = n__o() 31.73/11.06 31.73/11.06 u() = 2 >= 2 = n__u() 31.73/11.06 31.73/11.06 activate(n____(X1,X2)) = X1 + X2 + 8 >= X1 + X2 + 8 = __(X1,X2) 31.73/11.06 31.73/11.06 __(X,nil()) = X + 8 >= X = X 31.73/11.06 31.73/11.06 __(nil(),X) = X + 8 >= X = X 31.73/11.06 31.73/11.06 and(tt(),X) = X >= X = activate(X) 31.73/11.06 31.73/11.06 isList(n__nil()) = 8 >= 0 = tt() 31.73/11.06 31.73/11.06 isNeList(V) = V >= V = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(V) = V >= V = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(n____(I,__(P,I))) = 2I + P + 16 >= I + P = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.06 31.73/11.06 isPal(n__nil()) = 0 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__e()) = 10 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__i()) = 1 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__o()) = 0 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__u()) = 2 >= 0 = tt() 31.73/11.06 31.73/11.06 nil() = 0 >= 0 = n__nil() 31.73/11.06 31.73/11.06 __(X1,X2) = X1 + X2 + 8 >= X1 + X2 + 8 = n____(X1,X2) 31.73/11.06 31.73/11.06 isList(X) = X + 8 >= X + 8 = n__isList(X) 31.73/11.06 31.73/11.06 isNeList(X) = X >= X = n__isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isList(X)) = X + 8 >= X + 8 = isList(X) 31.73/11.06 31.73/11.06 activate(n__isNeList(X)) = X >= X = isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isPal(X)) = X >= X = isPal(X) 31.73/11.06 31.73/11.06 activate(n__a()) = 0 >= 0 = a() 31.73/11.06 31.73/11.06 activate(n__e()) = 10 >= 10 = e() 31.73/11.06 31.73/11.06 activate(n__i()) = 1 >= 1 = i() 31.73/11.06 31.73/11.06 activate(n__o()) = 0 >= 0 = o() 31.73/11.06 31.73/11.06 activate(n__u()) = 2 >= 2 = u() 31.73/11.06 31.73/11.06 activate(X) = X >= X = X 31.73/11.06 problem: 31.73/11.06 strict: 31.73/11.06 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.06 isPal(X) -> n__isPal(X) 31.73/11.06 a() -> n__a() 31.73/11.06 e() -> n__e() 31.73/11.06 i() -> n__i() 31.73/11.06 activate(n__nil()) -> nil() 31.73/11.06 weak: 31.73/11.06 isList(V) -> isNeList(activate(V)) 31.73/11.06 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.06 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 isPal(V) -> isNePal(activate(V)) 31.73/11.06 isQid(n__a()) -> tt() 31.73/11.06 o() -> n__o() 31.73/11.06 u() -> n__u() 31.73/11.06 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.06 __(X,nil()) -> X 31.73/11.06 __(nil(),X) -> X 31.73/11.06 and(tt(),X) -> activate(X) 31.73/11.06 isList(n__nil()) -> tt() 31.73/11.06 isNeList(V) -> isQid(activate(V)) 31.73/11.06 isNePal(V) -> isQid(activate(V)) 31.73/11.06 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.06 isPal(n__nil()) -> tt() 31.73/11.06 isQid(n__e()) -> tt() 31.73/11.06 isQid(n__i()) -> tt() 31.73/11.06 isQid(n__o()) -> tt() 31.73/11.06 isQid(n__u()) -> tt() 31.73/11.06 nil() -> n__nil() 31.73/11.06 __(X1,X2) -> n____(X1,X2) 31.73/11.06 isList(X) -> n__isList(X) 31.73/11.06 isNeList(X) -> n__isNeList(X) 31.73/11.06 activate(n__isList(X)) -> isList(X) 31.73/11.06 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.06 activate(n__isPal(X)) -> isPal(X) 31.73/11.06 activate(n__a()) -> a() 31.73/11.06 activate(n__e()) -> e() 31.73/11.06 activate(n__i()) -> i() 31.73/11.06 activate(n__o()) -> o() 31.73/11.06 activate(n__u()) -> u() 31.73/11.06 activate(X) -> X 31.73/11.06 Matrix Interpretation Processor: dim=1 31.73/11.06 31.73/11.06 max_matrix: 31.73/11.06 1 31.73/11.06 interpretation: 31.73/11.06 [u] = 2, 31.73/11.06 31.73/11.06 [o] = 8, 31.73/11.06 31.73/11.06 [i] = 1, 31.73/11.06 31.73/11.06 [e] = 0, 31.73/11.06 31.73/11.06 [a] = 1, 31.73/11.06 31.73/11.06 [n__u] = 2, 31.73/11.06 31.73/11.06 [n__o] = 8, 31.73/11.06 31.73/11.06 [n__i] = 0, 31.73/11.06 31.73/11.06 [n__e] = 2, 31.73/11.06 31.73/11.06 [n__a] = 0, 31.73/11.06 31.73/11.06 [isPal](x0) = x0 + 5, 31.73/11.06 31.73/11.06 [n__isPal](x0) = x0 + 4, 31.73/11.06 31.73/11.06 [isNePal](x0) = x0 + 4, 31.73/11.06 31.73/11.06 [n__isNeList](x0) = x0 + 1, 31.73/11.06 31.73/11.06 [isQid](x0) = x0, 31.73/11.06 31.73/11.06 [n__isList](x0) = x0 + 1, 31.73/11.06 31.73/11.06 [n____](x0, x1) = x0 + x1 + 5, 31.73/11.06 31.73/11.06 [n__nil] = 0, 31.73/11.06 31.73/11.06 [isNeList](x0) = x0 + 1, 31.73/11.06 31.73/11.06 [isList](x0) = x0 + 2, 31.73/11.06 31.73/11.06 [activate](x0) = x0 + 1, 31.73/11.06 31.73/11.06 [and](x0, x1) = x0 + x1 + 1, 31.73/11.06 31.73/11.06 [tt] = 0, 31.73/11.06 31.73/11.06 [nil] = 0, 31.73/11.06 31.73/11.06 [__](x0, x1) = x0 + x1 + 5 31.73/11.06 orientation: 31.73/11.06 __(__(X,Y),Z) = X + Y + Z + 10 >= X + Y + Z + 10 = __(X,__(Y,Z)) 31.73/11.06 31.73/11.06 isPal(X) = X + 5 >= X + 4 = n__isPal(X) 31.73/11.06 31.73/11.06 a() = 1 >= 0 = n__a() 31.73/11.06 31.73/11.06 e() = 0 >= 2 = n__e() 31.73/11.06 31.73/11.06 i() = 1 >= 0 = n__i() 31.73/11.06 31.73/11.06 activate(n__nil()) = 1 >= 0 = nil() 31.73/11.06 31.73/11.06 isList(V) = V + 2 >= V + 2 = isNeList(activate(V)) 31.73/11.06 31.73/11.06 isList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 6 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 31.73/11.06 isNeList(n____(V1,V2)) = V1 + V2 + 6 >= V1 + V2 + 6 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.06 31.73/11.06 isNeList(n____(V1,V2)) = V1 + V2 + 6 >= V1 + V2 + 5 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.06 31.73/11.06 isPal(V) = V + 5 >= V + 5 = isNePal(activate(V)) 31.73/11.06 31.73/11.06 isQid(n__a()) = 0 >= 0 = tt() 31.73/11.06 31.73/11.06 o() = 8 >= 8 = n__o() 31.73/11.06 31.73/11.06 u() = 2 >= 2 = n__u() 31.73/11.06 31.73/11.06 activate(n____(X1,X2)) = X1 + X2 + 6 >= X1 + X2 + 5 = __(X1,X2) 31.73/11.06 31.73/11.06 __(X,nil()) = X + 5 >= X = X 31.73/11.06 31.73/11.06 __(nil(),X) = X + 5 >= X = X 31.73/11.06 31.73/11.06 and(tt(),X) = X + 1 >= X + 1 = activate(X) 31.73/11.06 31.73/11.06 isList(n__nil()) = 2 >= 0 = tt() 31.73/11.06 31.73/11.06 isNeList(V) = V + 1 >= V + 1 = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(V) = V + 4 >= V + 1 = isQid(activate(V)) 31.73/11.06 31.73/11.06 isNePal(n____(I,__(P,I))) = 2I + P + 14 >= I + P + 7 = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.06 31.73/11.06 isPal(n__nil()) = 5 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__e()) = 2 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__i()) = 0 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__o()) = 8 >= 0 = tt() 31.73/11.06 31.73/11.06 isQid(n__u()) = 2 >= 0 = tt() 31.73/11.06 31.73/11.06 nil() = 0 >= 0 = n__nil() 31.73/11.06 31.73/11.06 __(X1,X2) = X1 + X2 + 5 >= X1 + X2 + 5 = n____(X1,X2) 31.73/11.06 31.73/11.06 isList(X) = X + 2 >= X + 1 = n__isList(X) 31.73/11.06 31.73/11.06 isNeList(X) = X + 1 >= X + 1 = n__isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isList(X)) = X + 2 >= X + 2 = isList(X) 31.73/11.06 31.73/11.06 activate(n__isNeList(X)) = X + 2 >= X + 1 = isNeList(X) 31.73/11.06 31.73/11.06 activate(n__isPal(X)) = X + 5 >= X + 5 = isPal(X) 31.73/11.06 31.73/11.06 activate(n__a()) = 1 >= 1 = a() 31.73/11.06 31.73/11.06 activate(n__e()) = 3 >= 0 = e() 31.73/11.06 31.73/11.06 activate(n__i()) = 1 >= 1 = i() 31.73/11.06 31.73/11.06 activate(n__o()) = 9 >= 8 = o() 31.73/11.06 31.73/11.06 activate(n__u()) = 3 >= 2 = u() 31.73/11.06 31.73/11.06 activate(X) = X + 1 >= X = X 31.73/11.06 problem: 31.73/11.06 strict: 31.73/11.06 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.07 e() -> n__e() 31.73/11.07 weak: 31.73/11.07 isPal(X) -> n__isPal(X) 31.73/11.07 a() -> n__a() 31.73/11.07 i() -> n__i() 31.73/11.07 activate(n__nil()) -> nil() 31.73/11.07 isList(V) -> isNeList(activate(V)) 31.73/11.07 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.07 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 isPal(V) -> isNePal(activate(V)) 31.73/11.07 isQid(n__a()) -> tt() 31.73/11.07 o() -> n__o() 31.73/11.07 u() -> n__u() 31.73/11.07 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.07 __(X,nil()) -> X 31.73/11.07 __(nil(),X) -> X 31.73/11.07 and(tt(),X) -> activate(X) 31.73/11.07 isList(n__nil()) -> tt() 31.73/11.07 isNeList(V) -> isQid(activate(V)) 31.73/11.07 isNePal(V) -> isQid(activate(V)) 31.73/11.07 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.07 isPal(n__nil()) -> tt() 31.73/11.07 isQid(n__e()) -> tt() 31.73/11.07 isQid(n__i()) -> tt() 31.73/11.07 isQid(n__o()) -> tt() 31.73/11.07 isQid(n__u()) -> tt() 31.73/11.07 nil() -> n__nil() 31.73/11.07 __(X1,X2) -> n____(X1,X2) 31.73/11.07 isList(X) -> n__isList(X) 31.73/11.07 isNeList(X) -> n__isNeList(X) 31.73/11.07 activate(n__isList(X)) -> isList(X) 31.73/11.07 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.07 activate(n__isPal(X)) -> isPal(X) 31.73/11.07 activate(n__a()) -> a() 31.73/11.07 activate(n__e()) -> e() 31.73/11.07 activate(n__i()) -> i() 31.73/11.07 activate(n__o()) -> o() 31.73/11.07 activate(n__u()) -> u() 31.73/11.07 activate(X) -> X 31.73/11.07 Matrix Interpretation Processor: dim=1 31.73/11.07 31.73/11.07 max_matrix: 31.73/11.07 1 31.73/11.07 interpretation: 31.73/11.07 [u] = 1, 31.73/11.07 31.73/11.07 [o] = 1, 31.73/11.07 31.73/11.07 [i] = 3, 31.73/11.07 31.73/11.07 [e] = 1, 31.73/11.07 31.73/11.07 [a] = 1, 31.73/11.07 31.73/11.07 [n__u] = 0, 31.73/11.07 31.73/11.07 [n__o] = 0, 31.73/11.07 31.73/11.07 [n__i] = 2, 31.73/11.07 31.73/11.07 [n__e] = 0, 31.73/11.07 31.73/11.07 [n__a] = 0, 31.73/11.07 31.73/11.07 [isPal](x0) = x0 + 12, 31.73/11.07 31.73/11.07 [n__isPal](x0) = x0 + 11, 31.73/11.07 31.73/11.07 [isNePal](x0) = x0 + 9, 31.73/11.07 31.73/11.07 [n__isNeList](x0) = x0, 31.73/11.07 31.73/11.07 [isQid](x0) = x0, 31.73/11.07 31.73/11.07 [n__isList](x0) = x0 + 2, 31.73/11.07 31.73/11.07 [n____](x0, x1) = x0 + x1 + 9, 31.73/11.07 31.73/11.07 [n__nil] = 1, 31.73/11.07 31.73/11.07 [isNeList](x0) = x0 + 1, 31.73/11.07 31.73/11.07 [isList](x0) = x0 + 2, 31.73/11.07 31.73/11.07 [activate](x0) = x0 + 1, 31.73/11.07 31.73/11.07 [and](x0, x1) = x0 + x1 + 2, 31.73/11.07 31.73/11.07 [tt] = 0, 31.73/11.07 31.73/11.07 [nil] = 1, 31.73/11.07 31.73/11.07 [__](x0, x1) = x0 + x1 + 10 31.73/11.07 orientation: 31.73/11.07 __(__(X,Y),Z) = X + Y + Z + 20 >= X + Y + Z + 20 = __(X,__(Y,Z)) 31.73/11.07 31.73/11.07 e() = 1 >= 0 = n__e() 31.73/11.07 31.73/11.07 isPal(X) = X + 12 >= X + 11 = n__isPal(X) 31.73/11.07 31.73/11.07 a() = 1 >= 0 = n__a() 31.73/11.07 31.73/11.07 i() = 3 >= 2 = n__i() 31.73/11.07 31.73/11.07 activate(n__nil()) = 2 >= 1 = nil() 31.73/11.07 31.73/11.07 isList(V) = V + 2 >= V + 2 = isNeList(activate(V)) 31.73/11.07 31.73/11.07 isList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 8 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 31.73/11.07 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 6 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.07 31.73/11.07 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 7 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 31.73/11.07 isPal(V) = V + 12 >= V + 10 = isNePal(activate(V)) 31.73/11.07 31.73/11.07 isQid(n__a()) = 0 >= 0 = tt() 31.73/11.07 31.73/11.07 o() = 1 >= 0 = n__o() 31.73/11.07 31.73/11.07 u() = 1 >= 0 = n__u() 31.73/11.07 31.73/11.07 activate(n____(X1,X2)) = X1 + X2 + 10 >= X1 + X2 + 10 = __(X1,X2) 31.73/11.07 31.73/11.07 __(X,nil()) = X + 11 >= X = X 31.73/11.07 31.73/11.07 __(nil(),X) = X + 11 >= X = X 31.73/11.07 31.73/11.07 and(tt(),X) = X + 2 >= X + 1 = activate(X) 31.73/11.07 31.73/11.07 isList(n__nil()) = 3 >= 0 = tt() 31.73/11.07 31.73/11.07 isNeList(V) = V + 1 >= V + 1 = isQid(activate(V)) 31.73/11.07 31.73/11.07 isNePal(V) = V + 9 >= V + 1 = isQid(activate(V)) 31.73/11.07 31.73/11.07 isNePal(n____(I,__(P,I))) = 2I + P + 28 >= I + P + 15 = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.07 31.73/11.07 isPal(n__nil()) = 13 >= 0 = tt() 31.73/11.07 31.73/11.07 isQid(n__e()) = 0 >= 0 = tt() 31.73/11.07 31.73/11.07 isQid(n__i()) = 2 >= 0 = tt() 31.73/11.07 31.73/11.07 isQid(n__o()) = 0 >= 0 = tt() 31.73/11.07 31.73/11.07 isQid(n__u()) = 0 >= 0 = tt() 31.73/11.07 31.73/11.07 nil() = 1 >= 1 = n__nil() 31.73/11.07 31.73/11.07 __(X1,X2) = X1 + X2 + 10 >= X1 + X2 + 9 = n____(X1,X2) 31.73/11.07 31.73/11.07 isList(X) = X + 2 >= X + 2 = n__isList(X) 31.73/11.07 31.73/11.07 isNeList(X) = X + 1 >= X = n__isNeList(X) 31.73/11.07 31.73/11.07 activate(n__isList(X)) = X + 3 >= X + 2 = isList(X) 31.73/11.07 31.73/11.07 activate(n__isNeList(X)) = X + 1 >= X + 1 = isNeList(X) 31.73/11.07 31.73/11.07 activate(n__isPal(X)) = X + 12 >= X + 12 = isPal(X) 31.73/11.07 31.73/11.07 activate(n__a()) = 1 >= 1 = a() 31.73/11.07 31.73/11.07 activate(n__e()) = 1 >= 1 = e() 31.73/11.07 31.73/11.07 activate(n__i()) = 3 >= 3 = i() 31.73/11.07 31.73/11.07 activate(n__o()) = 1 >= 1 = o() 31.73/11.07 31.73/11.07 activate(n__u()) = 1 >= 1 = u() 31.73/11.07 31.73/11.07 activate(X) = X + 1 >= X = X 31.73/11.07 problem: 31.73/11.07 strict: 31.73/11.07 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.07 weak: 31.73/11.07 e() -> n__e() 31.73/11.07 isPal(X) -> n__isPal(X) 31.73/11.07 a() -> n__a() 31.73/11.07 i() -> n__i() 31.73/11.07 activate(n__nil()) -> nil() 31.73/11.07 isList(V) -> isNeList(activate(V)) 31.73/11.07 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.07 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 isPal(V) -> isNePal(activate(V)) 31.73/11.07 isQid(n__a()) -> tt() 31.73/11.07 o() -> n__o() 31.73/11.07 u() -> n__u() 31.73/11.07 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.07 __(X,nil()) -> X 31.73/11.07 __(nil(),X) -> X 31.73/11.07 and(tt(),X) -> activate(X) 31.73/11.07 isList(n__nil()) -> tt() 31.73/11.07 isNeList(V) -> isQid(activate(V)) 31.73/11.07 isNePal(V) -> isQid(activate(V)) 31.73/11.07 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.07 isPal(n__nil()) -> tt() 31.73/11.07 isQid(n__e()) -> tt() 31.73/11.07 isQid(n__i()) -> tt() 31.73/11.07 isQid(n__o()) -> tt() 31.73/11.07 isQid(n__u()) -> tt() 31.73/11.07 nil() -> n__nil() 31.73/11.07 __(X1,X2) -> n____(X1,X2) 31.73/11.07 isList(X) -> n__isList(X) 31.73/11.07 isNeList(X) -> n__isNeList(X) 31.73/11.07 activate(n__isList(X)) -> isList(X) 31.73/11.07 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.07 activate(n__isPal(X)) -> isPal(X) 31.73/11.07 activate(n__a()) -> a() 31.73/11.07 activate(n__e()) -> e() 31.73/11.07 activate(n__i()) -> i() 31.73/11.07 activate(n__o()) -> o() 31.73/11.07 activate(n__u()) -> u() 31.73/11.07 activate(X) -> X 31.73/11.07 Matrix Interpretation Processor: dim=2 31.73/11.07 31.73/11.07 max_matrix: 31.73/11.07 [1 1] 31.73/11.07 [0 1] 31.73/11.07 interpretation: 31.73/11.07 [3] 31.73/11.07 [u] = [0], 31.73/11.07 31.73/11.07 [0] 31.73/11.07 [o] = [0], 31.73/11.07 31.73/11.07 [1] 31.73/11.07 [i] = [0], 31.73/11.07 31.73/11.07 [2] 31.73/11.07 [e] = [0], 31.73/11.07 31.73/11.07 [3] 31.73/11.07 [a] = [0], 31.73/11.07 31.73/11.07 [3] 31.73/11.07 [n__u] = [0], 31.73/11.07 31.73/11.07 [0] 31.73/11.07 [n__o] = [0], 31.73/11.07 31.73/11.07 [1] 31.73/11.07 [n__i] = [0], 31.73/11.07 31.73/11.07 [2] 31.73/11.07 [n__e] = [0], 31.73/11.07 31.73/11.07 [3] 31.73/11.07 [n__a] = [0], 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [isPal](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [n__isPal](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [isNePal](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [n__isNeList](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [isQid](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [n__isList](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 1] [0] 31.73/11.07 [n____](x0, x1) = [0 1]x0 + x1 + [2], 31.73/11.07 31.73/11.07 [2] 31.73/11.07 [n__nil] = [0], 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [isNeList](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [isList](x0) = [0 0]x0, 31.73/11.07 31.73/11.07 31.73/11.07 [activate](x0) = x0, 31.73/11.07 31.73/11.07 [1 0] 31.73/11.07 [and](x0, x1) = [0 0]x0 + x1, 31.73/11.07 31.73/11.07 [0] 31.73/11.07 [tt] = [0], 31.73/11.07 31.73/11.07 [2] 31.73/11.07 [nil] = [0], 31.73/11.07 31.73/11.07 [1 1] [0] 31.73/11.07 [__](x0, x1) = [0 1]x0 + x1 + [2] 31.73/11.07 orientation: 31.73/11.07 [1 2] [1 1] [2] [1 1] [1 1] [0] 31.73/11.07 __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [4] >= [0 1]X + [0 1]Y + Z + [4] = __(X,__(Y,Z)) 31.73/11.07 31.73/11.07 [2] [2] 31.73/11.07 e() = [0] >= [0] = n__e() 31.73/11.07 31.73/11.07 [1 0] [1 0] 31.73/11.07 isPal(X) = [0 0]X >= [0 0]X = n__isPal(X) 31.73/11.07 31.73/11.07 [3] [3] 31.73/11.07 a() = [0] >= [0] = n__a() 31.73/11.07 31.73/11.07 [1] [1] 31.73/11.07 i() = [0] >= [0] = n__i() 31.73/11.07 31.73/11.07 [2] [2] 31.73/11.07 activate(n__nil()) = [0] >= [0] = nil() 31.73/11.07 31.73/11.07 [1 0] [1 0] 31.73/11.07 isList(V) = [0 0]V >= [0 0]V = isNeList(activate(V)) 31.73/11.07 31.73/11.07 [1 1] [1 0] [1 0] [1 0] 31.73/11.07 isList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 31.73/11.07 [1 1] [1 0] [1 0] [1 0] 31.73/11.07 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.07 31.73/11.07 [1 1] [1 0] [1 0] [1 0] 31.73/11.07 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.07 31.73/11.07 [1 0] [1 0] 31.73/11.07 isPal(V) = [0 0]V >= [0 0]V = isNePal(activate(V)) 31.73/11.07 31.73/11.07 [3] [0] 31.73/11.07 isQid(n__a()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [0] [0] 31.73/11.07 o() = [0] >= [0] = n__o() 31.73/11.07 31.73/11.07 [3] [3] 31.73/11.07 u() = [0] >= [0] = n__u() 31.73/11.07 31.73/11.07 [1 1] [0] [1 1] [0] 31.73/11.07 activate(n____(X1,X2)) = [0 1]X1 + X2 + [2] >= [0 1]X1 + X2 + [2] = __(X1,X2) 31.73/11.07 31.73/11.07 [1 1] [2] 31.73/11.07 __(X,nil()) = [0 1]X + [2] >= X = X 31.73/11.07 31.73/11.07 [2] 31.73/11.07 __(nil(),X) = X + [2] >= X = X 31.73/11.07 31.73/11.07 31.73/11.07 and(tt(),X) = X >= X = activate(X) 31.73/11.07 31.73/11.07 [2] [0] 31.73/11.07 isList(n__nil()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [1 0] [1 0] 31.73/11.07 isNeList(V) = [0 0]V >= [0 0]V = isQid(activate(V)) 31.73/11.07 31.73/11.07 [1 0] [1 0] 31.73/11.07 isNePal(V) = [0 0]V >= [0 0]V = isQid(activate(V)) 31.73/11.07 31.73/11.07 [2 1] [1 1] [1 0] [1 0] 31.73/11.07 isNePal(n____(I,__(P,I))) = [0 0]I + [0 0]P >= [0 0]I + [0 0]P = and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.07 31.73/11.07 [2] [0] 31.73/11.07 isPal(n__nil()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [2] [0] 31.73/11.07 isQid(n__e()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [1] [0] 31.73/11.07 isQid(n__i()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [0] [0] 31.73/11.07 isQid(n__o()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [3] [0] 31.73/11.07 isQid(n__u()) = [0] >= [0] = tt() 31.73/11.07 31.73/11.07 [2] [2] 31.73/11.07 nil() = [0] >= [0] = n__nil() 31.73/11.08 31.73/11.08 [1 1] [0] [1 1] [0] 31.73/11.08 __(X1,X2) = [0 1]X1 + X2 + [2] >= [0 1]X1 + X2 + [2] = n____(X1,X2) 31.73/11.08 31.73/11.08 [1 0] [1 0] 31.73/11.08 isList(X) = [0 0]X >= [0 0]X = n__isList(X) 31.73/11.08 31.73/11.08 [1 0] [1 0] 31.73/11.08 isNeList(X) = [0 0]X >= [0 0]X = n__isNeList(X) 31.73/11.08 31.73/11.08 [1 0] [1 0] 31.73/11.08 activate(n__isList(X)) = [0 0]X >= [0 0]X = isList(X) 31.73/11.08 31.73/11.08 [1 0] [1 0] 31.73/11.08 activate(n__isNeList(X)) = [0 0]X >= [0 0]X = isNeList(X) 31.73/11.08 31.73/11.08 [1 0] [1 0] 31.73/11.08 activate(n__isPal(X)) = [0 0]X >= [0 0]X = isPal(X) 31.73/11.08 31.73/11.08 [3] [3] 31.73/11.08 activate(n__a()) = [0] >= [0] = a() 31.73/11.08 31.73/11.08 [2] [2] 31.73/11.08 activate(n__e()) = [0] >= [0] = e() 31.73/11.08 31.73/11.08 [1] [1] 31.73/11.08 activate(n__i()) = [0] >= [0] = i() 31.73/11.08 31.73/11.08 [0] [0] 31.73/11.08 activate(n__o()) = [0] >= [0] = o() 31.73/11.08 31.73/11.08 [3] [3] 31.73/11.08 activate(n__u()) = [0] >= [0] = u() 31.73/11.08 31.73/11.08 31.73/11.08 activate(X) = X >= X = X 31.73/11.08 problem: 31.73/11.08 strict: 31.73/11.08 31.73/11.08 weak: 31.73/11.08 __(__(X,Y),Z) -> __(X,__(Y,Z)) 31.73/11.08 e() -> n__e() 31.73/11.08 isPal(X) -> n__isPal(X) 31.73/11.08 a() -> n__a() 31.73/11.08 i() -> n__i() 31.73/11.08 activate(n__nil()) -> nil() 31.73/11.08 isList(V) -> isNeList(activate(V)) 31.73/11.08 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) 31.73/11.08 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) 31.73/11.08 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) 31.73/11.08 isPal(V) -> isNePal(activate(V)) 31.73/11.08 isQid(n__a()) -> tt() 31.73/11.08 o() -> n__o() 31.73/11.08 u() -> n__u() 31.73/11.08 activate(n____(X1,X2)) -> __(X1,X2) 31.73/11.08 __(X,nil()) -> X 31.73/11.08 __(nil(),X) -> X 31.73/11.08 and(tt(),X) -> activate(X) 31.73/11.08 isList(n__nil()) -> tt() 31.73/11.08 isNeList(V) -> isQid(activate(V)) 31.73/11.08 isNePal(V) -> isQid(activate(V)) 31.73/11.08 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) 31.73/11.08 isPal(n__nil()) -> tt() 31.73/11.08 isQid(n__e()) -> tt() 31.73/11.08 isQid(n__i()) -> tt() 31.73/11.08 isQid(n__o()) -> tt() 31.73/11.08 isQid(n__u()) -> tt() 31.73/11.08 nil() -> n__nil() 31.73/11.08 __(X1,X2) -> n____(X1,X2) 31.73/11.08 isList(X) -> n__isList(X) 31.73/11.08 isNeList(X) -> n__isNeList(X) 31.73/11.08 activate(n__isList(X)) -> isList(X) 31.73/11.08 activate(n__isNeList(X)) -> isNeList(X) 31.73/11.08 activate(n__isPal(X)) -> isPal(X) 31.73/11.08 activate(n__a()) -> a() 31.73/11.08 activate(n__e()) -> e() 31.73/11.08 activate(n__i()) -> i() 31.73/11.08 activate(n__o()) -> o() 31.73/11.08 activate(n__u()) -> u() 31.73/11.08 activate(X) -> X 31.73/11.08 Qed 31.73/11.08 EOF