YES(?,O(n^2)) 39.14/12.53 YES(?,O(n^2)) 39.14/12.53 39.14/12.53 Problem: 39.14/12.53 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.53 __(X,nil()) -> X 39.14/12.53 __(nil(),X) -> X 39.14/12.53 U11(tt()) -> tt() 39.14/12.53 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.53 U22(tt()) -> tt() 39.14/12.53 U31(tt()) -> tt() 39.14/12.53 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.53 U42(tt()) -> tt() 39.14/12.53 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.53 U52(tt()) -> tt() 39.14/12.53 U61(tt()) -> tt() 39.14/12.53 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.53 U72(tt()) -> tt() 39.14/12.53 U81(tt()) -> tt() 39.14/12.53 isList(V) -> U11(isNeList(activate(V))) 39.14/12.53 isList(n__nil()) -> tt() 39.14/12.53 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.53 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.53 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.53 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.53 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.53 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.53 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.53 isPal(n__nil()) -> tt() 39.14/12.53 isQid(n__a()) -> tt() 39.14/12.53 isQid(n__e()) -> tt() 39.14/12.53 isQid(n__i()) -> tt() 39.14/12.53 isQid(n__o()) -> tt() 39.14/12.53 isQid(n__u()) -> tt() 39.14/12.53 nil() -> n__nil() 39.14/12.53 __(X1,X2) -> n____(X1,X2) 39.14/12.53 a() -> n__a() 39.14/12.53 e() -> n__e() 39.14/12.53 i() -> n__i() 39.14/12.53 o() -> n__o() 39.14/12.53 u() -> n__u() 39.14/12.53 activate(n__nil()) -> nil() 39.14/12.53 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.53 activate(n__a()) -> a() 39.14/12.53 activate(n__e()) -> e() 39.14/12.53 activate(n__i()) -> i() 39.14/12.53 activate(n__o()) -> o() 39.14/12.53 activate(n__u()) -> u() 39.14/12.53 activate(X) -> X 39.14/12.53 39.14/12.53 Proof: 39.14/12.53 Complexity Transformation Processor: 39.14/12.53 strict: 39.14/12.53 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.53 __(X,nil()) -> X 39.14/12.53 __(nil(),X) -> X 39.14/12.53 U11(tt()) -> tt() 39.14/12.53 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.53 U22(tt()) -> tt() 39.14/12.53 U31(tt()) -> tt() 39.14/12.53 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.53 U42(tt()) -> tt() 39.14/12.53 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.53 U52(tt()) -> tt() 39.14/12.53 U61(tt()) -> tt() 39.14/12.53 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.53 U72(tt()) -> tt() 39.14/12.53 U81(tt()) -> tt() 39.14/12.53 isList(V) -> U11(isNeList(activate(V))) 39.14/12.53 isList(n__nil()) -> tt() 39.14/12.53 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.53 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.53 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.53 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.53 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.53 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.53 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.53 isPal(n__nil()) -> tt() 39.14/12.53 isQid(n__a()) -> tt() 39.14/12.53 isQid(n__e()) -> tt() 39.14/12.53 isQid(n__i()) -> tt() 39.14/12.53 isQid(n__o()) -> tt() 39.14/12.53 isQid(n__u()) -> tt() 39.14/12.53 nil() -> n__nil() 39.14/12.53 __(X1,X2) -> n____(X1,X2) 39.14/12.53 a() -> n__a() 39.14/12.53 e() -> n__e() 39.14/12.53 i() -> n__i() 39.14/12.53 o() -> n__o() 39.14/12.53 u() -> n__u() 39.14/12.53 activate(n__nil()) -> nil() 39.14/12.53 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.53 activate(n__a()) -> a() 39.14/12.53 activate(n__e()) -> e() 39.14/12.53 activate(n__i()) -> i() 39.14/12.53 activate(n__o()) -> o() 39.14/12.53 activate(n__u()) -> u() 39.14/12.53 activate(X) -> X 39.14/12.53 weak: 39.14/12.53 39.14/12.53 Matrix Interpretation Processor: dim=1 39.14/12.53 39.14/12.53 max_matrix: 39.14/12.53 1 39.14/12.53 interpretation: 39.14/12.53 [u] = 0, 39.14/12.53 39.14/12.53 [o] = 0, 39.14/12.53 39.14/12.53 [i] = 0, 39.14/12.53 39.14/12.53 [e] = 0, 39.14/12.53 39.14/12.53 [a] = 0, 39.14/12.53 39.14/12.53 [n__u] = 3, 39.14/12.53 39.14/12.53 [n__o] = 6, 39.14/12.53 39.14/12.53 [n__i] = 0, 39.14/12.53 39.14/12.53 [n__e] = 8, 39.14/12.53 39.14/12.53 [n__a] = 12, 39.14/12.53 39.14/12.53 [isNePal](x0) = x0 + 14, 39.14/12.53 39.14/12.53 [isQid](x0) = x0 + 1, 39.14/12.53 39.14/12.53 [n____](x0, x1) = x0 + x1 + 1, 39.14/12.53 39.14/12.53 [n__nil] = 4, 39.14/12.53 39.14/12.53 [U81](x0) = x0 + 12, 39.14/12.53 39.14/12.53 [U72](x0) = x0 + 7, 39.14/12.53 39.14/12.53 [isPal](x0) = x0 + 14, 39.14/12.53 39.14/12.53 [U71](x0, x1) = x0 + x1 + 8, 39.14/12.53 39.14/12.53 [U61](x0) = x0 + 8, 39.14/12.53 39.14/12.53 [U52](x0) = x0 + 2, 39.14/12.53 39.14/12.53 [U51](x0, x1) = x0 + x1 + 10, 39.14/12.53 39.14/12.53 [U42](x0) = x0 + 2, 39.14/12.53 39.14/12.53 [isNeList](x0) = x0 + 14, 39.14/12.53 39.14/12.53 [U41](x0, x1) = x0 + x1 + 4, 39.14/12.53 39.14/12.53 [U31](x0) = x0 + 12, 39.14/12.53 39.14/12.53 [U22](x0) = x0 + 12, 39.14/12.53 39.14/12.53 [isList](x0) = x0 + 14, 39.14/12.53 39.14/12.53 [activate](x0) = x0 + 2, 39.14/12.53 39.14/12.53 [U21](x0, x1) = x0 + x1 + 11, 39.14/12.53 39.14/12.53 [U11](x0) = x0 + 14, 39.14/12.53 39.14/12.53 [tt] = 0, 39.14/12.53 39.14/12.53 [nil] = 8, 39.14/12.53 39.14/12.53 [__](x0, x1) = x0 + x1 39.14/12.53 orientation: 39.14/12.53 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 39.14/12.53 39.14/12.53 __(X,nil()) = X + 8 >= X = X 39.14/12.53 39.14/12.53 __(nil(),X) = X + 8 >= X = X 39.14/12.53 39.14/12.53 U11(tt()) = 14 >= 0 = tt() 39.14/12.53 39.14/12.53 U21(tt(),V2) = V2 + 11 >= V2 + 28 = U22(isList(activate(V2))) 39.14/12.53 39.14/12.53 U22(tt()) = 12 >= 0 = tt() 39.14/12.53 39.14/12.53 U31(tt()) = 12 >= 0 = tt() 39.14/12.54 39.14/12.54 U41(tt(),V2) = V2 + 4 >= V2 + 18 = U42(isNeList(activate(V2))) 39.14/12.54 39.14/12.54 U42(tt()) = 2 >= 0 = tt() 39.14/12.54 39.14/12.54 U51(tt(),V2) = V2 + 10 >= V2 + 18 = U52(isList(activate(V2))) 39.14/12.54 39.14/12.54 U52(tt()) = 2 >= 0 = tt() 39.14/12.54 39.14/12.54 U61(tt()) = 8 >= 0 = tt() 39.14/12.54 39.14/12.54 U71(tt(),P) = P + 8 >= P + 23 = U72(isPal(activate(P))) 39.14/12.54 39.14/12.54 U72(tt()) = 7 >= 0 = tt() 39.14/12.54 39.14/12.54 U81(tt()) = 12 >= 0 = tt() 39.14/12.54 39.14/12.54 isList(V) = V + 14 >= V + 30 = U11(isNeList(activate(V))) 39.14/12.54 39.14/12.54 isList(n__nil()) = 18 >= 0 = tt() 39.14/12.54 39.14/12.54 isList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 29 = U21(isList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isNeList(V) = V + 14 >= V + 15 = U31(isQid(activate(V))) 39.14/12.54 39.14/12.54 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 22 = U41(isList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 28 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isNePal(V) = V + 14 >= V + 11 = U61(isQid(activate(V))) 39.14/12.54 39.14/12.54 isNePal(n____(I,__(P,I))) = 2I + P + 15 >= I + P + 13 = U71(isQid(activate(I)),activate(P)) 39.14/12.54 39.14/12.54 isPal(V) = V + 14 >= V + 28 = U81(isNePal(activate(V))) 39.14/12.54 39.14/12.54 isPal(n__nil()) = 18 >= 0 = tt() 39.14/12.54 39.14/12.54 isQid(n__a()) = 13 >= 0 = tt() 39.14/12.54 39.14/12.54 isQid(n__e()) = 9 >= 0 = tt() 39.14/12.54 39.14/12.54 isQid(n__i()) = 1 >= 0 = tt() 39.14/12.54 39.14/12.54 isQid(n__o()) = 7 >= 0 = tt() 39.14/12.54 39.14/12.54 isQid(n__u()) = 4 >= 0 = tt() 39.14/12.54 39.14/12.54 nil() = 8 >= 4 = n__nil() 39.14/12.54 39.14/12.54 __(X1,X2) = X1 + X2 >= X1 + X2 + 1 = n____(X1,X2) 39.14/12.54 39.14/12.54 a() = 0 >= 12 = n__a() 39.14/12.54 39.14/12.54 e() = 0 >= 8 = n__e() 39.14/12.54 39.14/12.54 i() = 0 >= 0 = n__i() 39.14/12.54 39.14/12.54 o() = 0 >= 6 = n__o() 39.14/12.54 39.14/12.54 u() = 0 >= 3 = n__u() 39.14/12.54 39.14/12.54 activate(n__nil()) = 6 >= 8 = nil() 39.14/12.54 39.14/12.54 activate(n____(X1,X2)) = X1 + X2 + 3 >= X1 + X2 = __(X1,X2) 39.14/12.54 39.14/12.54 activate(n__a()) = 14 >= 0 = a() 39.14/12.54 39.14/12.54 activate(n__e()) = 10 >= 0 = e() 39.14/12.54 39.14/12.54 activate(n__i()) = 2 >= 0 = i() 39.14/12.54 39.14/12.54 activate(n__o()) = 8 >= 0 = o() 39.14/12.54 39.14/12.54 activate(n__u()) = 5 >= 0 = u() 39.14/12.54 39.14/12.54 activate(X) = X + 2 >= X = X 39.14/12.54 problem: 39.14/12.54 strict: 39.14/12.54 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.54 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.54 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.54 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.54 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.54 isList(V) -> U11(isNeList(activate(V))) 39.14/12.54 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.54 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.54 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.54 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.54 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.54 __(X1,X2) -> n____(X1,X2) 39.14/12.54 a() -> n__a() 39.14/12.54 e() -> n__e() 39.14/12.54 i() -> n__i() 39.14/12.54 o() -> n__o() 39.14/12.54 u() -> n__u() 39.14/12.54 activate(n__nil()) -> nil() 39.14/12.54 weak: 39.14/12.54 __(X,nil()) -> X 39.14/12.54 __(nil(),X) -> X 39.14/12.54 U11(tt()) -> tt() 39.14/12.54 U22(tt()) -> tt() 39.14/12.54 U31(tt()) -> tt() 39.14/12.54 U42(tt()) -> tt() 39.14/12.54 U52(tt()) -> tt() 39.14/12.54 U61(tt()) -> tt() 39.14/12.54 U72(tt()) -> tt() 39.14/12.54 U81(tt()) -> tt() 39.14/12.54 isList(n__nil()) -> tt() 39.14/12.54 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.54 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.54 isPal(n__nil()) -> tt() 39.14/12.54 isQid(n__a()) -> tt() 39.14/12.54 isQid(n__e()) -> tt() 39.14/12.54 isQid(n__i()) -> tt() 39.14/12.54 isQid(n__o()) -> tt() 39.14/12.54 isQid(n__u()) -> tt() 39.14/12.54 nil() -> n__nil() 39.14/12.54 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.54 activate(n__a()) -> a() 39.14/12.54 activate(n__e()) -> e() 39.14/12.54 activate(n__i()) -> i() 39.14/12.54 activate(n__o()) -> o() 39.14/12.54 activate(n__u()) -> u() 39.14/12.54 activate(X) -> X 39.14/12.54 Matrix Interpretation Processor: dim=1 39.14/12.54 39.14/12.54 max_matrix: 39.14/12.54 1 39.14/12.54 interpretation: 39.14/12.54 [u] = 29, 39.14/12.54 39.14/12.54 [o] = 29, 39.14/12.54 39.14/12.54 [i] = 29, 39.14/12.54 39.14/12.54 [e] = 29, 39.14/12.54 39.14/12.54 [a] = 29, 39.14/12.54 39.14/12.54 [n__u] = 20, 39.14/12.54 39.14/12.54 [n__o] = 20, 39.14/12.54 39.14/12.54 [n__i] = 20, 39.14/12.54 39.14/12.54 [n__e] = 20, 39.14/12.54 39.14/12.54 [n__a] = 20, 39.14/12.54 39.14/12.54 [isNePal](x0) = x0 + 9, 39.14/12.54 39.14/12.54 [isQid](x0) = x0, 39.14/12.54 39.14/12.54 [n____](x0, x1) = x0 + x1 + 18, 39.14/12.54 39.14/12.54 [n__nil] = 0, 39.14/12.54 39.14/12.54 [U81](x0) = x0, 39.14/12.54 39.14/12.54 [U72](x0) = x0, 39.14/12.54 39.14/12.54 [isPal](x0) = x0 + 20, 39.14/12.54 39.14/12.54 [U71](x0, x1) = x0 + x1 + 9, 39.14/12.54 39.14/12.54 [U61](x0) = x0, 39.14/12.54 39.14/12.54 [U52](x0) = x0, 39.14/12.54 39.14/12.54 [U51](x0, x1) = x0 + x1 + 13, 39.14/12.54 39.14/12.54 [U42](x0) = x0, 39.14/12.54 39.14/12.54 [isNeList](x0) = x0 + 13, 39.14/12.54 39.14/12.54 [U41](x0, x1) = x0 + x1 + 2, 39.14/12.54 39.14/12.54 [U31](x0) = x0, 39.14/12.54 39.14/12.54 [U22](x0) = x0 + 9, 39.14/12.54 39.14/12.54 [isList](x0) = x0 + 20, 39.14/12.54 39.14/12.54 [activate](x0) = x0 + 9, 39.14/12.54 39.14/12.54 [U21](x0, x1) = x0 + x1, 39.14/12.54 39.14/12.54 [U11](x0) = x0, 39.14/12.54 39.14/12.54 [tt] = 20, 39.14/12.54 39.14/12.54 [nil] = 0, 39.14/12.54 39.14/12.54 [__](x0, x1) = x0 + x1 39.14/12.54 orientation: 39.14/12.54 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 39.14/12.54 39.14/12.54 U21(tt(),V2) = V2 + 20 >= V2 + 38 = U22(isList(activate(V2))) 39.14/12.54 39.14/12.54 U41(tt(),V2) = V2 + 22 >= V2 + 22 = U42(isNeList(activate(V2))) 39.14/12.54 39.14/12.54 U51(tt(),V2) = V2 + 33 >= V2 + 29 = U52(isList(activate(V2))) 39.14/12.54 39.14/12.54 U71(tt(),P) = P + 29 >= P + 29 = U72(isPal(activate(P))) 39.14/12.54 39.14/12.54 isList(V) = V + 20 >= V + 22 = U11(isNeList(activate(V))) 39.14/12.54 39.14/12.54 isList(n____(V1,V2)) = V1 + V2 + 38 >= V1 + V2 + 38 = U21(isList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isNeList(V) = V + 13 >= V + 9 = U31(isQid(activate(V))) 39.14/12.54 39.14/12.54 isNeList(n____(V1,V2)) = V1 + V2 + 31 >= V1 + V2 + 40 = U41(isList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isNeList(n____(V1,V2)) = V1 + V2 + 31 >= V1 + V2 + 44 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.54 39.14/12.54 isPal(V) = V + 20 >= V + 18 = U81(isNePal(activate(V))) 39.14/12.54 39.14/12.54 __(X1,X2) = X1 + X2 >= X1 + X2 + 18 = n____(X1,X2) 39.14/12.54 39.14/12.54 a() = 29 >= 20 = n__a() 39.14/12.54 39.14/12.54 e() = 29 >= 20 = n__e() 39.14/12.54 39.14/12.54 i() = 29 >= 20 = n__i() 39.14/12.54 39.14/12.54 o() = 29 >= 20 = n__o() 39.14/12.54 39.14/12.54 u() = 29 >= 20 = n__u() 39.14/12.54 39.14/12.54 activate(n__nil()) = 9 >= 0 = nil() 39.14/12.54 39.14/12.54 __(X,nil()) = X >= X = X 39.14/12.54 39.14/12.54 __(nil(),X) = X >= X = X 39.14/12.54 39.14/12.54 U11(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U22(tt()) = 29 >= 20 = tt() 39.14/12.54 39.14/12.54 U31(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U42(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U52(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U61(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U72(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 U81(tt()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isList(n__nil()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isNePal(V) = V + 9 >= V + 9 = U61(isQid(activate(V))) 39.14/12.54 39.14/12.54 isNePal(n____(I,__(P,I))) = 2I + P + 27 >= I + P + 27 = U71(isQid(activate(I)),activate(P)) 39.14/12.54 39.14/12.54 isPal(n__nil()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isQid(n__a()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isQid(n__e()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isQid(n__i()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isQid(n__o()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 isQid(n__u()) = 20 >= 20 = tt() 39.14/12.54 39.14/12.54 nil() = 0 >= 0 = n__nil() 39.14/12.54 39.14/12.54 activate(n____(X1,X2)) = X1 + X2 + 27 >= X1 + X2 = __(X1,X2) 39.14/12.54 39.14/12.54 activate(n__a()) = 29 >= 29 = a() 39.14/12.54 39.14/12.54 activate(n__e()) = 29 >= 29 = e() 39.14/12.54 39.14/12.54 activate(n__i()) = 29 >= 29 = i() 39.14/12.54 39.14/12.54 activate(n__o()) = 29 >= 29 = o() 39.14/12.54 39.14/12.54 activate(n__u()) = 29 >= 29 = u() 39.14/12.54 39.14/12.54 activate(X) = X + 9 >= X = X 39.14/12.54 problem: 39.14/12.54 strict: 39.14/12.54 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.54 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.54 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.54 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.54 isList(V) -> U11(isNeList(activate(V))) 39.14/12.54 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.54 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.54 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.54 __(X1,X2) -> n____(X1,X2) 39.14/12.54 weak: 39.14/12.54 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.54 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.54 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.54 a() -> n__a() 39.14/12.54 e() -> n__e() 39.14/12.54 i() -> n__i() 39.14/12.54 o() -> n__o() 39.14/12.54 u() -> n__u() 39.14/12.54 activate(n__nil()) -> nil() 39.14/12.54 __(X,nil()) -> X 39.14/12.54 __(nil(),X) -> X 39.14/12.54 U11(tt()) -> tt() 39.14/12.54 U22(tt()) -> tt() 39.14/12.54 U31(tt()) -> tt() 39.14/12.54 U42(tt()) -> tt() 39.14/12.54 U52(tt()) -> tt() 39.14/12.54 U61(tt()) -> tt() 39.14/12.54 U72(tt()) -> tt() 39.14/12.54 U81(tt()) -> tt() 39.14/12.54 isList(n__nil()) -> tt() 39.14/12.54 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.54 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.54 isPal(n__nil()) -> tt() 39.14/12.54 isQid(n__a()) -> tt() 39.14/12.54 isQid(n__e()) -> tt() 39.14/12.54 isQid(n__i()) -> tt() 39.14/12.55 isQid(n__o()) -> tt() 39.14/12.55 isQid(n__u()) -> tt() 39.14/12.55 nil() -> n__nil() 39.14/12.55 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.55 activate(n__a()) -> a() 39.14/12.55 activate(n__e()) -> e() 39.14/12.55 activate(n__i()) -> i() 39.14/12.55 activate(n__o()) -> o() 39.14/12.55 activate(n__u()) -> u() 39.14/12.55 activate(X) -> X 39.14/12.55 Matrix Interpretation Processor: dim=1 39.14/12.55 39.14/12.55 max_matrix: 39.14/12.55 1 39.14/12.55 interpretation: 39.14/12.55 [u] = 0, 39.14/12.55 39.14/12.55 [o] = 2, 39.14/12.55 39.14/12.55 [i] = 1, 39.14/12.55 39.14/12.55 [e] = 0, 39.14/12.55 39.14/12.55 [a] = 4, 39.14/12.55 39.14/12.55 [n__u] = 0, 39.14/12.55 39.14/12.55 [n__o] = 2, 39.14/12.55 39.14/12.55 [n__i] = 1, 39.14/12.55 39.14/12.55 [n__e] = 0, 39.14/12.55 39.14/12.55 [n__a] = 4, 39.14/12.55 39.14/12.55 [isNePal](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [isQid](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [n____](x0, x1) = x0 + x1 + 2, 39.14/12.55 39.14/12.55 [n__nil] = 0, 39.14/12.55 39.14/12.55 [U81](x0) = x0 + 2, 39.14/12.55 39.14/12.55 [U72](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [isPal](x0) = x0 + 10, 39.14/12.55 39.14/12.55 [U71](x0, x1) = x0 + x1 + 2, 39.14/12.55 39.14/12.55 [U61](x0) = x0, 39.14/12.55 39.14/12.55 [U52](x0) = x0, 39.14/12.55 39.14/12.55 [U51](x0, x1) = x0 + x1, 39.14/12.55 39.14/12.55 [U42](x0) = x0 + 6, 39.14/12.55 39.14/12.55 [isNeList](x0) = x0 + 13, 39.14/12.55 39.14/12.55 [U41](x0, x1) = x0 + x1 + 8, 39.14/12.55 39.14/12.55 [U31](x0) = x0 + 5, 39.14/12.55 39.14/12.55 [U22](x0) = x0 + 4, 39.14/12.55 39.14/12.55 [isList](x0) = x0, 39.14/12.55 39.14/12.55 [activate](x0) = x0, 39.14/12.55 39.14/12.55 [U21](x0, x1) = x0 + x1 + 6, 39.14/12.55 39.14/12.55 [U11](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [tt] = 0, 39.14/12.55 39.14/12.55 [nil] = 0, 39.14/12.55 39.14/12.55 [__](x0, x1) = x0 + x1 39.14/12.55 orientation: 39.14/12.55 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 39.14/12.55 39.14/12.55 U21(tt(),V2) = V2 + 6 >= V2 + 4 = U22(isList(activate(V2))) 39.14/12.55 39.14/12.55 U41(tt(),V2) = V2 + 8 >= V2 + 19 = U42(isNeList(activate(V2))) 39.14/12.55 39.14/12.55 U71(tt(),P) = P + 2 >= P + 18 = U72(isPal(activate(P))) 39.14/12.55 39.14/12.55 isList(V) = V >= V + 21 = U11(isNeList(activate(V))) 39.14/12.55 39.14/12.55 isList(n____(V1,V2)) = V1 + V2 + 2 >= V1 + V2 + 6 = U21(isList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 8 = U41(isList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 13 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 __(X1,X2) = X1 + X2 >= X1 + X2 + 2 = n____(X1,X2) 39.14/12.55 39.14/12.55 U51(tt(),V2) = V2 >= V2 = U52(isList(activate(V2))) 39.14/12.55 39.14/12.55 isNeList(V) = V + 13 >= V + 13 = U31(isQid(activate(V))) 39.14/12.55 39.14/12.55 isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V))) 39.14/12.55 39.14/12.55 a() = 4 >= 4 = n__a() 39.14/12.55 39.14/12.55 e() = 0 >= 0 = n__e() 39.14/12.55 39.14/12.55 i() = 1 >= 1 = n__i() 39.14/12.55 39.14/12.55 o() = 2 >= 2 = n__o() 39.14/12.55 39.14/12.55 u() = 0 >= 0 = n__u() 39.14/12.55 39.14/12.55 activate(n__nil()) = 0 >= 0 = nil() 39.14/12.55 39.14/12.55 __(X,nil()) = X >= X = X 39.14/12.55 39.14/12.55 __(nil(),X) = X >= X = X 39.14/12.55 39.14/12.55 U11(tt()) = 8 >= 0 = tt() 39.14/12.55 39.14/12.55 U22(tt()) = 4 >= 0 = tt() 39.14/12.55 39.14/12.55 U31(tt()) = 5 >= 0 = tt() 39.14/12.55 39.14/12.55 U42(tt()) = 6 >= 0 = tt() 39.14/12.55 39.14/12.55 U52(tt()) = 0 >= 0 = tt() 39.14/12.55 39.14/12.55 U61(tt()) = 0 >= 0 = tt() 39.14/12.55 39.14/12.55 U72(tt()) = 8 >= 0 = tt() 39.14/12.55 39.14/12.55 U81(tt()) = 2 >= 0 = tt() 39.14/12.55 39.14/12.55 isList(n__nil()) = 0 >= 0 = tt() 39.14/12.55 39.14/12.55 isNePal(V) = V + 8 >= V + 8 = U61(isQid(activate(V))) 39.14/12.55 39.14/12.55 isNePal(n____(I,__(P,I))) = 2I + P + 10 >= I + P + 10 = U71(isQid(activate(I)),activate(P)) 39.14/12.55 39.14/12.55 isPal(n__nil()) = 10 >= 0 = tt() 39.14/12.55 39.14/12.55 isQid(n__a()) = 12 >= 0 = tt() 39.14/12.55 39.14/12.55 isQid(n__e()) = 8 >= 0 = tt() 39.14/12.55 39.14/12.55 isQid(n__i()) = 9 >= 0 = tt() 39.14/12.55 39.14/12.55 isQid(n__o()) = 10 >= 0 = tt() 39.14/12.55 39.14/12.55 isQid(n__u()) = 8 >= 0 = tt() 39.14/12.55 39.14/12.55 nil() = 0 >= 0 = n__nil() 39.14/12.55 39.14/12.55 activate(n____(X1,X2)) = X1 + X2 + 2 >= X1 + X2 = __(X1,X2) 39.14/12.55 39.14/12.55 activate(n__a()) = 4 >= 4 = a() 39.14/12.55 39.14/12.55 activate(n__e()) = 0 >= 0 = e() 39.14/12.55 39.14/12.55 activate(n__i()) = 1 >= 1 = i() 39.14/12.55 39.14/12.55 activate(n__o()) = 2 >= 2 = o() 39.14/12.55 39.14/12.55 activate(n__u()) = 0 >= 0 = u() 39.14/12.55 39.14/12.55 activate(X) = X >= X = X 39.14/12.55 problem: 39.14/12.55 strict: 39.14/12.55 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.55 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.55 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.55 isList(V) -> U11(isNeList(activate(V))) 39.14/12.55 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.55 __(X1,X2) -> n____(X1,X2) 39.14/12.55 weak: 39.14/12.55 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.55 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.55 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.55 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.55 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.55 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.55 a() -> n__a() 39.14/12.55 e() -> n__e() 39.14/12.55 i() -> n__i() 39.14/12.55 o() -> n__o() 39.14/12.55 u() -> n__u() 39.14/12.55 activate(n__nil()) -> nil() 39.14/12.55 __(X,nil()) -> X 39.14/12.55 __(nil(),X) -> X 39.14/12.55 U11(tt()) -> tt() 39.14/12.55 U22(tt()) -> tt() 39.14/12.55 U31(tt()) -> tt() 39.14/12.55 U42(tt()) -> tt() 39.14/12.55 U52(tt()) -> tt() 39.14/12.55 U61(tt()) -> tt() 39.14/12.55 U72(tt()) -> tt() 39.14/12.55 U81(tt()) -> tt() 39.14/12.55 isList(n__nil()) -> tt() 39.14/12.55 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.55 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.55 isPal(n__nil()) -> tt() 39.14/12.55 isQid(n__a()) -> tt() 39.14/12.55 isQid(n__e()) -> tt() 39.14/12.55 isQid(n__i()) -> tt() 39.14/12.55 isQid(n__o()) -> tt() 39.14/12.55 isQid(n__u()) -> tt() 39.14/12.55 nil() -> n__nil() 39.14/12.55 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.55 activate(n__a()) -> a() 39.14/12.55 activate(n__e()) -> e() 39.14/12.55 activate(n__i()) -> i() 39.14/12.55 activate(n__o()) -> o() 39.14/12.55 activate(n__u()) -> u() 39.14/12.55 activate(X) -> X 39.14/12.55 Matrix Interpretation Processor: dim=1 39.14/12.55 39.14/12.55 max_matrix: 39.14/12.55 1 39.14/12.55 interpretation: 39.14/12.55 [u] = 6, 39.14/12.55 39.14/12.55 [o] = 4, 39.14/12.55 39.14/12.55 [i] = 4, 39.14/12.55 39.14/12.55 [e] = 4, 39.14/12.55 39.14/12.55 [a] = 12, 39.14/12.55 39.14/12.55 [n__u] = 6, 39.14/12.55 39.14/12.55 [n__o] = 4, 39.14/12.55 39.14/12.55 [n__i] = 4, 39.14/12.55 39.14/12.55 [n__e] = 4, 39.14/12.55 39.14/12.55 [n__a] = 12, 39.14/12.55 39.14/12.55 [isNePal](x0) = x0 + 12, 39.14/12.55 39.14/12.55 [isQid](x0) = x0 + 4, 39.14/12.55 39.14/12.55 [n____](x0, x1) = x0 + x1 + 6, 39.14/12.55 39.14/12.55 [n__nil] = 0, 39.14/12.55 39.14/12.55 [U81](x0) = x0 + 1, 39.14/12.55 39.14/12.55 [U72](x0) = x0 + 2, 39.14/12.55 39.14/12.55 [isPal](x0) = x0 + 13, 39.14/12.55 39.14/12.55 [U71](x0, x1) = x0 + x1 + 2, 39.14/12.55 39.14/12.55 [U61](x0) = x0 + 5, 39.14/12.55 39.14/12.55 [U52](x0) = x0 + 2, 39.14/12.55 39.14/12.55 [U51](x0, x1) = x0 + x1 + 6, 39.14/12.55 39.14/12.55 [U42](x0) = x0 + 10, 39.14/12.55 39.14/12.55 [isNeList](x0) = x0 + 6, 39.14/12.55 39.14/12.55 [U41](x0, x1) = x0 + x1, 39.14/12.55 39.14/12.55 [U31](x0) = x0 + 2, 39.14/12.55 39.14/12.55 [U22](x0) = x0, 39.14/12.55 39.14/12.55 [isList](x0) = x0 + 12, 39.14/12.55 39.14/12.55 [activate](x0) = x0, 39.14/12.55 39.14/12.55 [U21](x0, x1) = x0 + x1 + 4, 39.14/12.55 39.14/12.55 [U11](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [tt] = 8, 39.14/12.55 39.14/12.55 [nil] = 0, 39.14/12.55 39.14/12.55 [__](x0, x1) = x0 + x1 39.14/12.55 orientation: 39.14/12.55 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 39.14/12.55 39.14/12.55 U41(tt(),V2) = V2 + 8 >= V2 + 16 = U42(isNeList(activate(V2))) 39.14/12.55 39.14/12.55 U71(tt(),P) = P + 10 >= P + 15 = U72(isPal(activate(P))) 39.14/12.55 39.14/12.55 isList(V) = V + 12 >= V + 14 = U11(isNeList(activate(V))) 39.14/12.55 39.14/12.55 isList(n____(V1,V2)) = V1 + V2 + 18 >= V1 + V2 + 16 = U21(isList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 __(X1,X2) = X1 + X2 >= X1 + X2 + 6 = n____(X1,X2) 39.14/12.55 39.14/12.55 U21(tt(),V2) = V2 + 12 >= V2 + 12 = U22(isList(activate(V2))) 39.14/12.55 39.14/12.55 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.55 39.14/12.55 U51(tt(),V2) = V2 + 14 >= V2 + 14 = U52(isList(activate(V2))) 39.14/12.55 39.14/12.55 isNeList(V) = V + 6 >= V + 6 = U31(isQid(activate(V))) 39.14/12.55 39.14/12.55 isPal(V) = V + 13 >= V + 13 = U81(isNePal(activate(V))) 39.14/12.55 39.14/12.55 a() = 12 >= 12 = n__a() 39.14/12.55 39.14/12.55 e() = 4 >= 4 = n__e() 39.14/12.55 39.14/12.55 i() = 4 >= 4 = n__i() 39.14/12.55 39.14/12.55 o() = 4 >= 4 = n__o() 39.14/12.55 39.14/12.55 u() = 6 >= 6 = n__u() 39.14/12.55 39.14/12.55 activate(n__nil()) = 0 >= 0 = nil() 39.14/12.55 39.14/12.55 __(X,nil()) = X >= X = X 39.14/12.55 39.14/12.55 __(nil(),X) = X >= X = X 39.14/12.55 39.14/12.55 U11(tt()) = 16 >= 8 = tt() 39.14/12.55 39.14/12.55 U22(tt()) = 8 >= 8 = tt() 39.14/12.55 39.14/12.55 U31(tt()) = 10 >= 8 = tt() 39.14/12.55 39.14/12.55 U42(tt()) = 18 >= 8 = tt() 39.14/12.55 39.14/12.55 U52(tt()) = 10 >= 8 = tt() 39.14/12.55 39.14/12.55 U61(tt()) = 13 >= 8 = tt() 39.14/12.55 39.14/12.55 U72(tt()) = 10 >= 8 = tt() 39.14/12.55 39.14/12.55 U81(tt()) = 9 >= 8 = tt() 39.14/12.55 39.14/12.55 isList(n__nil()) = 12 >= 8 = tt() 39.14/12.55 39.14/12.55 isNePal(V) = V + 12 >= V + 9 = U61(isQid(activate(V))) 39.14/12.55 39.14/12.55 isNePal(n____(I,__(P,I))) = 2I + P + 18 >= I + P + 6 = U71(isQid(activate(I)),activate(P)) 39.14/12.55 39.14/12.55 isPal(n__nil()) = 13 >= 8 = tt() 39.14/12.55 39.14/12.55 isQid(n__a()) = 16 >= 8 = tt() 39.14/12.55 39.14/12.55 isQid(n__e()) = 8 >= 8 = tt() 39.14/12.55 39.14/12.55 isQid(n__i()) = 8 >= 8 = tt() 39.14/12.55 39.14/12.55 isQid(n__o()) = 8 >= 8 = tt() 39.14/12.55 39.14/12.55 isQid(n__u()) = 10 >= 8 = tt() 39.14/12.55 39.14/12.55 nil() = 0 >= 0 = n__nil() 39.14/12.55 39.14/12.55 activate(n____(X1,X2)) = X1 + X2 + 6 >= X1 + X2 = __(X1,X2) 39.14/12.55 39.14/12.55 activate(n__a()) = 12 >= 12 = a() 39.14/12.55 39.14/12.55 activate(n__e()) = 4 >= 4 = e() 39.14/12.55 39.14/12.55 activate(n__i()) = 4 >= 4 = i() 39.14/12.55 39.14/12.55 activate(n__o()) = 4 >= 4 = o() 39.14/12.55 39.14/12.55 activate(n__u()) = 6 >= 6 = u() 39.14/12.55 39.14/12.55 activate(X) = X >= X = X 39.14/12.55 problem: 39.14/12.55 strict: 39.14/12.55 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.55 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.55 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.55 isList(V) -> U11(isNeList(activate(V))) 39.14/12.55 __(X1,X2) -> n____(X1,X2) 39.14/12.55 weak: 39.14/12.55 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.55 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.55 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.55 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.55 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.55 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.55 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.55 a() -> n__a() 39.14/12.55 e() -> n__e() 39.14/12.55 i() -> n__i() 39.14/12.55 o() -> n__o() 39.14/12.55 u() -> n__u() 39.14/12.55 activate(n__nil()) -> nil() 39.14/12.55 __(X,nil()) -> X 39.14/12.55 __(nil(),X) -> X 39.14/12.55 U11(tt()) -> tt() 39.14/12.55 U22(tt()) -> tt() 39.14/12.55 U31(tt()) -> tt() 39.14/12.55 U42(tt()) -> tt() 39.14/12.55 U52(tt()) -> tt() 39.14/12.55 U61(tt()) -> tt() 39.14/12.55 U72(tt()) -> tt() 39.14/12.55 U81(tt()) -> tt() 39.14/12.55 isList(n__nil()) -> tt() 39.14/12.55 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.55 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.55 isPal(n__nil()) -> tt() 39.14/12.55 isQid(n__a()) -> tt() 39.14/12.55 isQid(n__e()) -> tt() 39.14/12.55 isQid(n__i()) -> tt() 39.14/12.55 isQid(n__o()) -> tt() 39.14/12.55 isQid(n__u()) -> tt() 39.14/12.55 nil() -> n__nil() 39.14/12.55 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.55 activate(n__a()) -> a() 39.14/12.55 activate(n__e()) -> e() 39.14/12.55 activate(n__i()) -> i() 39.14/12.55 activate(n__o()) -> o() 39.14/12.55 activate(n__u()) -> u() 39.14/12.55 activate(X) -> X 39.14/12.55 Matrix Interpretation Processor: dim=1 39.14/12.55 39.14/12.55 max_matrix: 39.14/12.55 1 39.14/12.55 interpretation: 39.14/12.55 [u] = 8, 39.14/12.55 39.14/12.55 [o] = 21, 39.14/12.55 39.14/12.55 [i] = 32, 39.14/12.55 39.14/12.55 [e] = 5, 39.14/12.55 39.14/12.55 [a] = 8, 39.14/12.55 39.14/12.55 [n__u] = 8, 39.14/12.55 39.14/12.55 [n__o] = 21, 39.14/12.55 39.14/12.55 [n__i] = 32, 39.14/12.55 39.14/12.55 [n__e] = 5, 39.14/12.55 39.14/12.55 [n__a] = 8, 39.14/12.55 39.14/12.55 [isNePal](x0) = x0 + 25, 39.14/12.55 39.14/12.55 [isQid](x0) = x0 + 3, 39.14/12.55 39.14/12.55 [n____](x0, x1) = x0 + x1 + 53, 39.14/12.55 39.14/12.55 [n__nil] = 8, 39.14/12.55 39.14/12.55 [U81](x0) = x0 + 38, 39.14/12.55 39.14/12.55 [U72](x0) = x0 + 4, 39.14/12.55 39.14/12.55 [isPal](x0) = x0 + 63, 39.14/12.55 39.14/12.55 [U71](x0, x1) = x0 + x1 + 60, 39.14/12.55 39.14/12.55 [U61](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [U52](x0) = x0 + 20, 39.14/12.55 39.14/12.55 [U51](x0, x1) = x0 + x1 + 36, 39.14/12.55 39.14/12.55 [U42](x0) = x0 + 36, 39.14/12.55 39.14/12.55 [isNeList](x0) = x0 + 8, 39.14/12.55 39.14/12.55 [U41](x0, x1) = x0 + x1 + 22, 39.14/12.55 39.14/12.55 [U31](x0) = x0 + 4, 39.14/12.55 39.14/12.55 [U22](x0) = x0 + 16, 39.14/12.55 39.14/12.55 [isList](x0) = x0, 39.14/12.55 39.14/12.55 [activate](x0) = x0, 39.14/12.55 39.14/12.55 [U21](x0, x1) = x0 + x1 + 8, 39.14/12.55 39.14/12.55 [U11](x0) = x0 + 49, 39.14/12.55 39.14/12.55 [tt] = 8, 39.14/12.55 39.14/12.55 [nil] = 8, 39.14/12.55 39.14/12.55 [__](x0, x1) = x0 + x1 + 11 39.14/12.55 orientation: 39.14/12.55 __(__(X,Y),Z) = X + Y + Z + 22 >= X + Y + Z + 22 = __(X,__(Y,Z)) 39.14/12.55 39.14/12.55 U41(tt(),V2) = V2 + 30 >= V2 + 44 = U42(isNeList(activate(V2))) 39.14/12.56 39.14/12.56 U71(tt(),P) = P + 68 >= P + 67 = U72(isPal(activate(P))) 39.14/12.56 39.14/12.56 isList(V) = V >= V + 57 = U11(isNeList(activate(V))) 39.14/12.56 39.14/12.56 __(X1,X2) = X1 + X2 + 11 >= X1 + X2 + 53 = n____(X1,X2) 39.14/12.56 39.14/12.56 isList(n____(V1,V2)) = V1 + V2 + 53 >= V1 + V2 + 8 = U21(isList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 U21(tt(),V2) = V2 + 16 >= V2 + 16 = U22(isList(activate(V2))) 39.14/12.56 39.14/12.56 isNeList(n____(V1,V2)) = V1 + V2 + 61 >= V1 + V2 + 22 = U41(isList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 isNeList(n____(V1,V2)) = V1 + V2 + 61 >= V1 + V2 + 44 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 U51(tt(),V2) = V2 + 44 >= V2 + 20 = U52(isList(activate(V2))) 39.14/12.56 39.14/12.56 isNeList(V) = V + 8 >= V + 7 = U31(isQid(activate(V))) 39.14/12.56 39.14/12.56 isPal(V) = V + 63 >= V + 63 = U81(isNePal(activate(V))) 39.14/12.56 39.14/12.56 a() = 8 >= 8 = n__a() 39.14/12.56 39.14/12.56 e() = 5 >= 5 = n__e() 39.14/12.56 39.14/12.56 i() = 32 >= 32 = n__i() 39.14/12.56 39.14/12.56 o() = 21 >= 21 = n__o() 39.14/12.56 39.14/12.56 u() = 8 >= 8 = n__u() 39.14/12.56 39.14/12.56 activate(n__nil()) = 8 >= 8 = nil() 39.14/12.56 39.14/12.56 __(X,nil()) = X + 19 >= X = X 39.14/12.56 39.14/12.56 __(nil(),X) = X + 19 >= X = X 39.14/12.56 39.14/12.56 U11(tt()) = 57 >= 8 = tt() 39.14/12.56 39.14/12.56 U22(tt()) = 24 >= 8 = tt() 39.14/12.56 39.14/12.56 U31(tt()) = 12 >= 8 = tt() 39.14/12.56 39.14/12.56 U42(tt()) = 44 >= 8 = tt() 39.14/12.56 39.14/12.56 U52(tt()) = 28 >= 8 = tt() 39.14/12.56 39.14/12.56 U61(tt()) = 16 >= 8 = tt() 39.14/12.56 39.14/12.56 U72(tt()) = 12 >= 8 = tt() 39.14/12.56 39.14/12.56 U81(tt()) = 46 >= 8 = tt() 39.14/12.56 39.14/12.56 isList(n__nil()) = 8 >= 8 = tt() 39.14/12.56 39.14/12.56 isNePal(V) = V + 25 >= V + 11 = U61(isQid(activate(V))) 39.14/12.56 39.14/12.56 isNePal(n____(I,__(P,I))) = 2I + P + 89 >= I + P + 63 = U71(isQid(activate(I)),activate(P)) 39.14/12.56 39.14/12.56 isPal(n__nil()) = 71 >= 8 = tt() 39.14/12.56 39.14/12.56 isQid(n__a()) = 11 >= 8 = tt() 39.14/12.56 39.14/12.56 isQid(n__e()) = 8 >= 8 = tt() 39.14/12.56 39.14/12.56 isQid(n__i()) = 35 >= 8 = tt() 39.14/12.56 39.14/12.56 isQid(n__o()) = 24 >= 8 = tt() 39.14/12.56 39.14/12.56 isQid(n__u()) = 11 >= 8 = tt() 39.14/12.56 39.14/12.56 nil() = 8 >= 8 = n__nil() 39.14/12.56 39.14/12.56 activate(n____(X1,X2)) = X1 + X2 + 53 >= X1 + X2 + 11 = __(X1,X2) 39.14/12.56 39.14/12.56 activate(n__a()) = 8 >= 8 = a() 39.14/12.56 39.14/12.56 activate(n__e()) = 5 >= 5 = e() 39.14/12.56 39.14/12.56 activate(n__i()) = 32 >= 32 = i() 39.14/12.56 39.14/12.56 activate(n__o()) = 21 >= 21 = o() 39.14/12.56 39.14/12.56 activate(n__u()) = 8 >= 8 = u() 39.14/12.56 39.14/12.56 activate(X) = X >= X = X 39.14/12.56 problem: 39.14/12.56 strict: 39.14/12.56 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.56 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.56 isList(V) -> U11(isNeList(activate(V))) 39.14/12.56 __(X1,X2) -> n____(X1,X2) 39.14/12.56 weak: 39.14/12.56 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.56 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.56 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.56 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.56 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.56 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.56 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.56 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.56 a() -> n__a() 39.14/12.56 e() -> n__e() 39.14/12.56 i() -> n__i() 39.14/12.56 o() -> n__o() 39.14/12.56 u() -> n__u() 39.14/12.56 activate(n__nil()) -> nil() 39.14/12.56 __(X,nil()) -> X 39.14/12.56 __(nil(),X) -> X 39.14/12.56 U11(tt()) -> tt() 39.14/12.56 U22(tt()) -> tt() 39.14/12.56 U31(tt()) -> tt() 39.14/12.56 U42(tt()) -> tt() 39.14/12.56 U52(tt()) -> tt() 39.14/12.56 U61(tt()) -> tt() 39.14/12.56 U72(tt()) -> tt() 39.14/12.56 U81(tt()) -> tt() 39.14/12.56 isList(n__nil()) -> tt() 39.14/12.56 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.56 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.56 isPal(n__nil()) -> tt() 39.14/12.56 isQid(n__a()) -> tt() 39.14/12.56 isQid(n__e()) -> tt() 39.14/12.56 isQid(n__i()) -> tt() 39.14/12.56 isQid(n__o()) -> tt() 39.14/12.56 isQid(n__u()) -> tt() 39.14/12.56 nil() -> n__nil() 39.14/12.56 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.56 activate(n__a()) -> a() 39.14/12.56 activate(n__e()) -> e() 39.14/12.56 activate(n__i()) -> i() 39.14/12.56 activate(n__o()) -> o() 39.14/12.56 activate(n__u()) -> u() 39.14/12.56 activate(X) -> X 39.14/12.56 Matrix Interpretation Processor: dim=1 39.14/12.56 39.14/12.56 max_matrix: 39.14/12.56 1 39.14/12.56 interpretation: 39.14/12.56 [u] = 1, 39.14/12.56 39.14/12.56 [o] = 1, 39.14/12.56 39.14/12.56 [i] = 1, 39.14/12.56 39.14/12.56 [e] = 1, 39.14/12.56 39.14/12.56 [a] = 1, 39.14/12.56 39.14/12.56 [n__u] = 1, 39.14/12.56 39.14/12.56 [n__o] = 1, 39.14/12.56 39.14/12.56 [n__i] = 1, 39.14/12.56 39.14/12.56 [n__e] = 1, 39.14/12.56 39.14/12.56 [n__a] = 1, 39.14/12.56 39.14/12.56 [isNePal](x0) = x0 + 8, 39.14/12.56 39.14/12.56 [isQid](x0) = x0 + 2, 39.14/12.56 39.14/12.56 [n____](x0, x1) = x0 + x1 + 10, 39.14/12.56 39.14/12.56 [n__nil] = 0, 39.14/12.56 39.14/12.56 [U81](x0) = x0 + 2, 39.14/12.56 39.14/12.56 [U72](x0) = x0 + 8, 39.14/12.56 39.14/12.56 [isPal](x0) = x0 + 10, 39.14/12.56 39.14/12.56 [U71](x0, x1) = x0 + x1 + 15, 39.14/12.56 39.14/12.56 [U61](x0) = x0, 39.14/12.56 39.14/12.56 [U52](x0) = x0 + 6, 39.14/12.56 39.14/12.56 [U51](x0, x1) = x0 + x1 + 10, 39.14/12.56 39.14/12.56 [U42](x0) = x0, 39.14/12.56 39.14/12.56 [isNeList](x0) = x0 + 2, 39.14/12.56 39.14/12.56 [U41](x0, x1) = x0 + x1 + 5, 39.14/12.56 39.14/12.56 [U31](x0) = x0, 39.14/12.56 39.14/12.56 [U22](x0) = x0 + 6, 39.14/12.56 39.14/12.56 [isList](x0) = x0 + 7, 39.14/12.56 39.14/12.56 [activate](x0) = x0, 39.14/12.56 39.14/12.56 [U21](x0, x1) = x0 + x1 + 10, 39.14/12.56 39.14/12.56 [U11](x0) = x0, 39.14/12.56 39.14/12.56 [tt] = 3, 39.14/12.56 39.14/12.56 [nil] = 0, 39.14/12.56 39.14/12.56 [__](x0, x1) = x0 + x1 39.14/12.56 orientation: 39.14/12.56 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 39.14/12.56 39.14/12.56 U41(tt(),V2) = V2 + 8 >= V2 + 2 = U42(isNeList(activate(V2))) 39.14/12.56 39.14/12.56 isList(V) = V + 7 >= V + 2 = U11(isNeList(activate(V))) 39.14/12.56 39.14/12.56 __(X1,X2) = X1 + X2 >= X1 + X2 + 10 = n____(X1,X2) 39.14/12.56 39.14/12.56 U71(tt(),P) = P + 18 >= P + 18 = U72(isPal(activate(P))) 39.14/12.56 39.14/12.56 isList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 17 = U21(isList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 U21(tt(),V2) = V2 + 13 >= V2 + 13 = U22(isList(activate(V2))) 39.14/12.56 39.14/12.56 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.56 39.14/12.56 U51(tt(),V2) = V2 + 13 >= V2 + 13 = U52(isList(activate(V2))) 39.14/12.56 39.14/12.56 isNeList(V) = V + 2 >= V + 2 = U31(isQid(activate(V))) 39.14/12.56 39.14/12.56 isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V))) 39.14/12.56 39.14/12.56 a() = 1 >= 1 = n__a() 39.14/12.56 39.14/12.56 e() = 1 >= 1 = n__e() 39.14/12.56 39.14/12.56 i() = 1 >= 1 = n__i() 39.14/12.56 39.14/12.56 o() = 1 >= 1 = n__o() 39.14/12.56 39.14/12.56 u() = 1 >= 1 = n__u() 39.14/12.56 39.14/12.56 activate(n__nil()) = 0 >= 0 = nil() 39.14/12.56 39.14/12.56 __(X,nil()) = X >= X = X 39.14/12.56 39.14/12.56 __(nil(),X) = X >= X = X 39.14/12.56 39.14/12.56 U11(tt()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 U22(tt()) = 9 >= 3 = tt() 39.14/12.56 39.14/12.56 U31(tt()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 U42(tt()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 U52(tt()) = 9 >= 3 = tt() 39.14/12.56 39.14/12.56 U61(tt()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 U72(tt()) = 11 >= 3 = tt() 39.14/12.56 39.14/12.56 U81(tt()) = 5 >= 3 = tt() 39.14/12.56 39.14/12.56 isList(n__nil()) = 7 >= 3 = tt() 39.14/12.56 39.14/12.56 isNePal(V) = V + 8 >= V + 2 = U61(isQid(activate(V))) 39.14/12.56 39.14/12.56 isNePal(n____(I,__(P,I))) = 2I + P + 18 >= I + P + 17 = U71(isQid(activate(I)),activate(P)) 39.14/12.56 39.14/12.56 isPal(n__nil()) = 10 >= 3 = tt() 39.14/12.56 39.14/12.56 isQid(n__a()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 isQid(n__e()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 isQid(n__i()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 isQid(n__o()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 isQid(n__u()) = 3 >= 3 = tt() 39.14/12.56 39.14/12.56 nil() = 0 >= 0 = n__nil() 39.14/12.56 39.14/12.56 activate(n____(X1,X2)) = X1 + X2 + 10 >= X1 + X2 = __(X1,X2) 39.14/12.56 39.14/12.56 activate(n__a()) = 1 >= 1 = a() 39.14/12.56 39.14/12.56 activate(n__e()) = 1 >= 1 = e() 39.14/12.56 39.14/12.56 activate(n__i()) = 1 >= 1 = i() 39.14/12.56 39.14/12.56 activate(n__o()) = 1 >= 1 = o() 39.14/12.56 39.14/12.56 activate(n__u()) = 1 >= 1 = u() 39.14/12.57 39.14/12.57 activate(X) = X >= X = X 39.14/12.57 problem: 39.14/12.57 strict: 39.14/12.57 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.57 __(X1,X2) -> n____(X1,X2) 39.14/12.57 weak: 39.14/12.57 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.57 isList(V) -> U11(isNeList(activate(V))) 39.14/12.57 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.57 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.57 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.57 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.57 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.57 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.57 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.57 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.57 a() -> n__a() 39.14/12.57 e() -> n__e() 39.14/12.57 i() -> n__i() 39.14/12.57 o() -> n__o() 39.14/12.57 u() -> n__u() 39.14/12.57 activate(n__nil()) -> nil() 39.14/12.57 __(X,nil()) -> X 39.14/12.57 __(nil(),X) -> X 39.14/12.57 U11(tt()) -> tt() 39.14/12.57 U22(tt()) -> tt() 39.14/12.57 U31(tt()) -> tt() 39.14/12.57 U42(tt()) -> tt() 39.14/12.57 U52(tt()) -> tt() 39.14/12.57 U61(tt()) -> tt() 39.14/12.57 U72(tt()) -> tt() 39.14/12.57 U81(tt()) -> tt() 39.14/12.57 isList(n__nil()) -> tt() 39.14/12.57 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.57 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.57 isPal(n__nil()) -> tt() 39.14/12.57 isQid(n__a()) -> tt() 39.14/12.57 isQid(n__e()) -> tt() 39.14/12.57 isQid(n__i()) -> tt() 39.14/12.57 isQid(n__o()) -> tt() 39.14/12.57 isQid(n__u()) -> tt() 39.14/12.57 nil() -> n__nil() 39.14/12.57 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.57 activate(n__a()) -> a() 39.14/12.57 activate(n__e()) -> e() 39.14/12.57 activate(n__i()) -> i() 39.14/12.57 activate(n__o()) -> o() 39.14/12.57 activate(n__u()) -> u() 39.14/12.57 activate(X) -> X 39.14/12.57 Matrix Interpretation Processor: dim=1 39.14/12.57 39.14/12.57 max_matrix: 39.14/12.57 1 39.14/12.57 interpretation: 39.14/12.57 [u] = 17, 39.14/12.57 39.14/12.57 [o] = 5, 39.14/12.57 39.14/12.57 [i] = 5, 39.14/12.57 39.14/12.57 [e] = 5, 39.14/12.57 39.14/12.57 [a] = 5, 39.14/12.57 39.14/12.57 [n__u] = 16, 39.14/12.57 39.14/12.57 [n__o] = 4, 39.14/12.57 39.14/12.57 [n__i] = 4, 39.14/12.57 39.14/12.57 [n__e] = 4, 39.14/12.57 39.14/12.57 [n__a] = 4, 39.14/12.57 39.14/12.57 [isNePal](x0) = x0 + 13, 39.14/12.57 39.14/12.57 [isQid](x0) = x0 + 8, 39.14/12.57 39.14/12.57 [n____](x0, x1) = x0 + x1 + 7, 39.14/12.57 39.14/12.57 [n__nil] = 17, 39.14/12.57 39.14/12.57 [U81](x0) = x0 + 5, 39.14/12.57 39.14/12.57 [U72](x0) = x0 + 7, 39.14/12.57 39.14/12.57 [isPal](x0) = x0 + 19, 39.14/12.57 39.14/12.57 [U71](x0, x1) = x0 + x1 + 15, 39.14/12.57 39.14/12.57 [U61](x0) = x0 + 4, 39.14/12.57 39.14/12.57 [U52](x0) = x0, 39.14/12.57 39.14/12.57 [U51](x0, x1) = x0 + x1 + 5, 39.14/12.57 39.14/12.57 [U42](x0) = x0 + 2, 39.14/12.57 39.14/12.57 [isNeList](x0) = x0 + 11, 39.14/12.57 39.14/12.57 [U41](x0, x1) = x0 + x1 + 4, 39.14/12.57 39.14/12.57 [U31](x0) = x0 + 2, 39.14/12.57 39.14/12.57 [U22](x0) = x0, 39.14/12.57 39.14/12.57 [isList](x0) = x0 + 12, 39.14/12.57 39.14/12.57 [activate](x0) = x0 + 1, 39.14/12.57 39.14/12.57 [U21](x0, x1) = x0 + x1 + 1, 39.14/12.57 39.14/12.57 [U11](x0) = x0, 39.14/12.57 39.14/12.57 [tt] = 12, 39.14/12.57 39.14/12.57 [nil] = 18, 39.14/12.57 39.14/12.57 [__](x0, x1) = x0 + x1 + 8 39.14/12.57 orientation: 39.14/12.57 __(__(X,Y),Z) = X + Y + Z + 16 >= X + Y + Z + 16 = __(X,__(Y,Z)) 39.14/12.57 39.14/12.57 __(X1,X2) = X1 + X2 + 8 >= X1 + X2 + 7 = n____(X1,X2) 39.14/12.57 39.14/12.57 U41(tt(),V2) = V2 + 16 >= V2 + 14 = U42(isNeList(activate(V2))) 39.14/12.57 39.14/12.57 isList(V) = V + 12 >= V + 12 = U11(isNeList(activate(V))) 39.14/12.57 39.14/12.57 U71(tt(),P) = P + 27 >= P + 27 = U72(isPal(activate(P))) 39.14/12.57 39.14/12.57 isList(n____(V1,V2)) = V1 + V2 + 19 >= V1 + V2 + 15 = U21(isList(activate(V1)),activate(V2)) 39.14/12.57 39.14/12.57 U21(tt(),V2) = V2 + 13 >= V2 + 13 = U22(isList(activate(V2))) 39.14/12.57 39.14/12.57 isNeList(n____(V1,V2)) = V1 + V2 + 18 >= V1 + V2 + 18 = U41(isList(activate(V1)),activate(V2)) 39.14/12.57 39.14/12.57 isNeList(n____(V1,V2)) = V1 + V2 + 18 >= V1 + V2 + 18 = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.57 39.14/12.57 U51(tt(),V2) = V2 + 17 >= V2 + 13 = U52(isList(activate(V2))) 39.14/12.57 39.14/12.57 isNeList(V) = V + 11 >= V + 11 = U31(isQid(activate(V))) 39.14/12.57 39.14/12.57 isPal(V) = V + 19 >= V + 19 = U81(isNePal(activate(V))) 39.14/12.57 39.14/12.57 a() = 5 >= 4 = n__a() 39.14/12.57 39.14/12.57 e() = 5 >= 4 = n__e() 39.14/12.57 39.14/12.57 i() = 5 >= 4 = n__i() 39.14/12.57 39.14/12.57 o() = 5 >= 4 = n__o() 39.14/12.57 39.14/12.57 u() = 17 >= 16 = n__u() 39.14/12.57 39.14/12.57 activate(n__nil()) = 18 >= 18 = nil() 39.14/12.57 39.14/12.57 __(X,nil()) = X + 26 >= X = X 39.14/12.57 39.14/12.57 __(nil(),X) = X + 26 >= X = X 39.14/12.57 39.14/12.57 U11(tt()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 U22(tt()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 U31(tt()) = 14 >= 12 = tt() 39.14/12.57 39.14/12.57 U42(tt()) = 14 >= 12 = tt() 39.14/12.57 39.14/12.57 U52(tt()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 U61(tt()) = 16 >= 12 = tt() 39.14/12.57 39.14/12.57 U72(tt()) = 19 >= 12 = tt() 39.14/12.57 39.14/12.57 U81(tt()) = 17 >= 12 = tt() 39.14/12.57 39.14/12.57 isList(n__nil()) = 29 >= 12 = tt() 39.14/12.57 39.14/12.57 isNePal(V) = V + 13 >= V + 13 = U61(isQid(activate(V))) 39.14/12.57 39.14/12.57 isNePal(n____(I,__(P,I))) = 2I + P + 28 >= I + P + 25 = U71(isQid(activate(I)),activate(P)) 39.14/12.57 39.14/12.57 isPal(n__nil()) = 36 >= 12 = tt() 39.14/12.57 39.14/12.57 isQid(n__a()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 isQid(n__e()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 isQid(n__i()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 isQid(n__o()) = 12 >= 12 = tt() 39.14/12.57 39.14/12.57 isQid(n__u()) = 24 >= 12 = tt() 39.14/12.57 39.14/12.57 nil() = 18 >= 17 = n__nil() 39.14/12.57 39.14/12.57 activate(n____(X1,X2)) = X1 + X2 + 8 >= X1 + X2 + 8 = __(X1,X2) 39.14/12.57 39.14/12.57 activate(n__a()) = 5 >= 5 = a() 39.14/12.57 39.14/12.57 activate(n__e()) = 5 >= 5 = e() 39.14/12.57 39.14/12.57 activate(n__i()) = 5 >= 5 = i() 39.14/12.57 39.14/12.57 activate(n__o()) = 5 >= 5 = o() 39.14/12.57 39.14/12.57 activate(n__u()) = 17 >= 17 = u() 39.14/12.57 39.14/12.57 activate(X) = X + 1 >= X = X 39.14/12.57 problem: 39.14/12.57 strict: 39.14/12.57 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.57 weak: 39.14/12.57 __(X1,X2) -> n____(X1,X2) 39.14/12.57 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.57 isList(V) -> U11(isNeList(activate(V))) 39.14/12.57 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.57 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.57 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.57 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.57 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.57 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.57 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.57 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.57 a() -> n__a() 39.14/12.57 e() -> n__e() 39.14/12.57 i() -> n__i() 39.14/12.57 o() -> n__o() 39.14/12.57 u() -> n__u() 39.14/12.57 activate(n__nil()) -> nil() 39.14/12.57 __(X,nil()) -> X 39.14/12.57 __(nil(),X) -> X 39.14/12.57 U11(tt()) -> tt() 39.14/12.57 U22(tt()) -> tt() 39.14/12.57 U31(tt()) -> tt() 39.14/12.57 U42(tt()) -> tt() 39.14/12.57 U52(tt()) -> tt() 39.14/12.57 U61(tt()) -> tt() 39.14/12.57 U72(tt()) -> tt() 39.14/12.57 U81(tt()) -> tt() 39.14/12.57 isList(n__nil()) -> tt() 39.14/12.57 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.57 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.57 isPal(n__nil()) -> tt() 39.14/12.57 isQid(n__a()) -> tt() 39.14/12.57 isQid(n__e()) -> tt() 39.14/12.57 isQid(n__i()) -> tt() 39.14/12.57 isQid(n__o()) -> tt() 39.14/12.57 isQid(n__u()) -> tt() 39.14/12.57 nil() -> n__nil() 39.14/12.57 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.57 activate(n__a()) -> a() 39.14/12.57 activate(n__e()) -> e() 39.14/12.57 activate(n__i()) -> i() 39.14/12.57 activate(n__o()) -> o() 39.14/12.57 activate(n__u()) -> u() 39.14/12.57 activate(X) -> X 39.14/12.57 Matrix Interpretation Processor: dim=2 39.14/12.57 39.14/12.57 max_matrix: 39.14/12.57 [1 2] 39.14/12.57 [0 1] 39.14/12.57 interpretation: 39.14/12.57 [0] 39.14/12.57 [u] = [0], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [o] = [0], 39.14/12.57 39.14/12.57 [2] 39.14/12.57 [i] = [0], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [e] = [2], 39.14/12.57 39.14/12.57 [3] 39.14/12.57 [a] = [1], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [n__u] = [0], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [n__o] = [0], 39.14/12.57 39.14/12.57 [2] 39.14/12.57 [n__i] = [0], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [n__e] = [2], 39.14/12.57 39.14/12.57 [3] 39.14/12.57 [n__a] = [1], 39.14/12.57 39.14/12.57 [1 2] [0] 39.14/12.57 [isNePal](x0) = [0 0]x0 + [1], 39.14/12.57 39.14/12.57 [1 0] [0] 39.14/12.57 [isQid](x0) = [0 0]x0 + [1], 39.14/12.57 39.14/12.57 [1 1] [0] 39.14/12.57 [n____](x0, x1) = [0 1]x0 + x1 + [1], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [n__nil] = [1], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [U81](x0) = x0 + [1], 39.14/12.57 39.14/12.57 [1 1] [0] 39.14/12.57 [U72](x0) = [0 0]x0 + [1], 39.14/12.57 39.14/12.57 [1 2] [0] 39.14/12.57 [isPal](x0) = [0 0]x0 + [2], 39.14/12.57 39.14/12.57 [1 0] [1 2] [2] 39.14/12.57 [U71](x0, x1) = [0 0]x0 + [0 0]x1 + [1], 39.14/12.57 39.14/12.57 [1 0] [0] 39.14/12.57 [U61](x0) = [0 0]x0 + [1], 39.14/12.57 39.14/12.57 [1 0] 39.14/12.57 [U52](x0) = [0 0]x0, 39.14/12.57 39.14/12.57 [1 0] [0] 39.14/12.57 [U51](x0, x1) = [0 0]x0 + x1 + [2], 39.14/12.57 39.14/12.57 [1 0] [0] 39.14/12.57 [U42](x0) = [0 0]x0 + [2], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [isNeList](x0) = x0 + [2], 39.14/12.57 39.14/12.57 [1 2] [0] 39.14/12.57 [U41](x0, x1) = [0 0]x0 + x1 + [3], 39.14/12.57 39.14/12.57 [1 0] [0] 39.14/12.57 [U31](x0) = [0 0]x0 + [2], 39.14/12.57 39.14/12.57 [1 0] 39.14/12.57 [U22](x0) = [0 0]x0, 39.14/12.57 39.14/12.57 [1 0] 39.14/12.57 [isList](x0) = [0 0]x0, 39.14/12.57 39.14/12.57 39.14/12.57 [activate](x0) = x0, 39.14/12.57 39.14/12.57 [1 0] 39.14/12.57 [U21](x0, x1) = x0 + [0 0]x1, 39.14/12.57 39.14/12.57 [1 0] 39.14/12.57 [U11](x0) = [0 0]x0, 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [tt] = [0], 39.14/12.57 39.14/12.57 [0] 39.14/12.57 [nil] = [1], 39.14/12.57 39.14/12.57 [1 1] [0] 39.14/12.57 [__](x0, x1) = [0 1]x0 + x1 + [1] 39.14/12.57 orientation: 39.14/12.57 [1 2] [1 1] [1] [1 1] [1 1] [0] 39.14/12.57 __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z)) 39.14/12.57 39.14/12.57 [1 1] [0] [1 1] [0] 39.14/12.57 __(X1,X2) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = n____(X1,X2) 39.14/12.57 39.14/12.57 [0] [1 0] [0] 39.14/12.57 U41(tt(),V2) = V2 + [3] >= [0 0]V2 + [2] = U42(isNeList(activate(V2))) 39.14/12.57 39.14/12.57 [1 0] [1 0] 39.14/12.57 isList(V) = [0 0]V >= [0 0]V = U11(isNeList(activate(V))) 39.14/12.57 39.14/12.57 [1 2] [2] [1 2] [2] 39.14/12.57 U71(tt(),P) = [0 0]P + [1] >= [0 0]P + [1] = U72(isPal(activate(P))) 39.14/12.57 39.14/12.57 [1 1] [1 0] [1 0] [1 0] 39.14/12.57 isList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = U21(isList(activate(V1)),activate(V2)) 39.14/12.57 39.14/12.57 [1 0] [1 0] 39.14/12.57 U21(tt(),V2) = [0 0]V2 >= [0 0]V2 = U22(isList(activate(V2))) 39.14/12.57 39.14/12.57 [1 1] [0] [1 0] [0] 39.14/12.57 isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [3] >= [0 0]V1 + V2 + [3] = U41(isList(activate(V1)),activate(V2)) 39.14/12.57 39.14/12.57 [1 1] [0] [1 0] [0] 39.14/12.57 isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [3] >= [0 0]V1 + V2 + [2] = U51(isNeList(activate(V1)),activate(V2)) 39.14/12.58 39.14/12.58 [0] [1 0] 39.14/12.58 U51(tt(),V2) = V2 + [2] >= [0 0]V2 = U52(isList(activate(V2))) 39.14/12.58 39.14/12.58 [0] [1 0] [0] 39.14/12.58 isNeList(V) = V + [2] >= [0 0]V + [2] = U31(isQid(activate(V))) 39.14/12.58 39.14/12.58 [1 2] [0] [1 2] [0] 39.14/12.58 isPal(V) = [0 0]V + [2] >= [0 0]V + [2] = U81(isNePal(activate(V))) 39.14/12.58 39.14/12.58 [3] [3] 39.14/12.58 a() = [1] >= [1] = n__a() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 e() = [2] >= [2] = n__e() 39.14/12.58 39.14/12.58 [2] [2] 39.14/12.58 i() = [0] >= [0] = n__i() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 o() = [0] >= [0] = n__o() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 u() = [0] >= [0] = n__u() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 activate(n__nil()) = [1] >= [1] = nil() 39.14/12.58 39.14/12.58 [1 1] [0] 39.14/12.58 __(X,nil()) = [0 1]X + [2] >= X = X 39.14/12.58 39.14/12.58 [1] 39.14/12.58 __(nil(),X) = X + [2] >= X = X 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U11(tt()) = [0] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U22(tt()) = [0] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U31(tt()) = [2] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U42(tt()) = [2] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U52(tt()) = [0] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U61(tt()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U72(tt()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 U81(tt()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 isList(n__nil()) = [0] >= [0] = tt() 39.14/12.58 39.14/12.58 [1 2] [0] [1 0] [0] 39.14/12.58 isNePal(V) = [0 0]V + [1] >= [0 0]V + [1] = U61(isQid(activate(V))) 39.14/12.58 39.14/12.58 [2 5] [1 3] [4] [1 0] [1 2] [2] 39.14/12.58 isNePal(n____(I,__(P,I))) = [0 0]I + [0 0]P + [1] >= [0 0]I + [0 0]P + [1] = U71(isQid(activate(I)),activate(P)) 39.14/12.58 39.14/12.58 [2] [0] 39.14/12.58 isPal(n__nil()) = [2] >= [0] = tt() 39.14/12.58 39.14/12.58 [3] [0] 39.14/12.58 isQid(n__a()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 isQid(n__e()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [2] [0] 39.14/12.58 isQid(n__i()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 isQid(n__o()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 isQid(n__u()) = [1] >= [0] = tt() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 nil() = [1] >= [1] = n__nil() 39.14/12.58 39.14/12.58 [1 1] [0] [1 1] [0] 39.14/12.58 activate(n____(X1,X2)) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = __(X1,X2) 39.14/12.58 39.14/12.58 [3] [3] 39.14/12.58 activate(n__a()) = [1] >= [1] = a() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 activate(n__e()) = [2] >= [2] = e() 39.14/12.58 39.14/12.58 [2] [2] 39.14/12.58 activate(n__i()) = [0] >= [0] = i() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 activate(n__o()) = [0] >= [0] = o() 39.14/12.58 39.14/12.58 [0] [0] 39.14/12.58 activate(n__u()) = [0] >= [0] = u() 39.14/12.58 39.14/12.58 39.14/12.58 activate(X) = X >= X = X 39.14/12.58 problem: 39.14/12.58 strict: 39.14/12.58 39.14/12.58 weak: 39.14/12.58 __(__(X,Y),Z) -> __(X,__(Y,Z)) 39.14/12.58 __(X1,X2) -> n____(X1,X2) 39.14/12.58 U41(tt(),V2) -> U42(isNeList(activate(V2))) 39.14/12.58 isList(V) -> U11(isNeList(activate(V))) 39.14/12.58 U71(tt(),P) -> U72(isPal(activate(P))) 39.14/12.58 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 39.14/12.58 U21(tt(),V2) -> U22(isList(activate(V2))) 39.14/12.58 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 39.14/12.58 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 39.14/12.58 U51(tt(),V2) -> U52(isList(activate(V2))) 39.14/12.58 isNeList(V) -> U31(isQid(activate(V))) 39.14/12.58 isPal(V) -> U81(isNePal(activate(V))) 39.14/12.58 a() -> n__a() 39.14/12.58 e() -> n__e() 39.14/12.58 i() -> n__i() 39.14/12.58 o() -> n__o() 39.14/12.58 u() -> n__u() 39.14/12.58 activate(n__nil()) -> nil() 39.14/12.58 __(X,nil()) -> X 39.14/12.58 __(nil(),X) -> X 39.14/12.58 U11(tt()) -> tt() 39.14/12.58 U22(tt()) -> tt() 39.14/12.58 U31(tt()) -> tt() 39.14/12.58 U42(tt()) -> tt() 39.14/12.58 U52(tt()) -> tt() 39.14/12.58 U61(tt()) -> tt() 39.14/12.58 U72(tt()) -> tt() 39.14/12.58 U81(tt()) -> tt() 39.14/12.58 isList(n__nil()) -> tt() 39.14/12.58 isNePal(V) -> U61(isQid(activate(V))) 39.14/12.58 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 39.14/12.58 isPal(n__nil()) -> tt() 39.14/12.58 isQid(n__a()) -> tt() 39.14/12.58 isQid(n__e()) -> tt() 39.14/12.58 isQid(n__i()) -> tt() 39.14/12.58 isQid(n__o()) -> tt() 39.14/12.58 isQid(n__u()) -> tt() 39.14/12.58 nil() -> n__nil() 39.14/12.58 activate(n____(X1,X2)) -> __(X1,X2) 39.14/12.58 activate(n__a()) -> a() 39.14/12.58 activate(n__e()) -> e() 39.14/12.58 activate(n__i()) -> i() 39.14/12.58 activate(n__o()) -> o() 39.14/12.58 activate(n__u()) -> u() 39.14/12.58 activate(X) -> X 39.14/12.58 Qed 39.14/12.58 EOF