YES
0 QTRS
↳1 QTRSRRRProof (⇔, 592 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 93 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 56 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 0 ms)
↳8 QTRS
↳9 RisEmptyProof (⇔, 0 ms)
↳10 YES
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt, V)) → mark(U12(isNeList(V)))
active(U12(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isList(V1), V2))
active(U22(tt, V2)) → mark(U23(isList(V2)))
active(U23(tt)) → mark(tt)
active(U31(tt, V)) → mark(U32(isQid(V)))
active(U32(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isList(V1), V2))
active(U42(tt, V2)) → mark(U43(isNeList(V2)))
active(U43(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isNeList(V1), V2))
active(U52(tt, V2)) → mark(U53(isList(V2)))
active(U53(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isQid(V)))
active(U62(tt)) → mark(tt)
active(U71(tt, V)) → mark(U72(isNePal(V)))
active(U72(tt)) → mark(tt)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))))
active(isPal(V)) → mark(U71(isPalListKind(V), V))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(V1, V2))) → mark(and(isPalListKind(V1), isPalListKind(V2)))
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNeList(X)) → active(isNeList(X))
mark(U21(X1, X2, X3)) → active(U21(mark(X1), X2, X3))
mark(U22(X1, X2)) → active(U22(mark(X1), X2))
mark(isList(X)) → active(isList(X))
mark(U23(X)) → active(U23(mark(X)))
mark(U31(X1, X2)) → active(U31(mark(X1), X2))
mark(U32(X)) → active(U32(mark(X)))
mark(isQid(X)) → active(isQid(X))
mark(U41(X1, X2, X3)) → active(U41(mark(X1), X2, X3))
mark(U42(X1, X2)) → active(U42(mark(X1), X2))
mark(U43(X)) → active(U43(mark(X)))
mark(U51(X1, X2, X3)) → active(U51(mark(X1), X2, X3))
mark(U52(X1, X2)) → active(U52(mark(X1), X2))
mark(U53(X)) → active(U53(mark(X)))
mark(U61(X1, X2)) → active(U61(mark(X1), X2))
mark(U62(X)) → active(U62(mark(X)))
mark(U71(X1, X2)) → active(U71(mark(X1), X2))
mark(U72(X)) → active(U72(mark(X)))
mark(isNePal(X)) → active(isNePal(X))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isPalListKind(X)) → active(isPalListKind(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
U21(mark(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, mark(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, mark(X3)) → U21(X1, X2, X3)
U21(active(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, active(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, active(X3)) → U21(X1, X2, X3)
U22(mark(X1), X2) → U22(X1, X2)
U22(X1, mark(X2)) → U22(X1, X2)
U22(active(X1), X2) → U22(X1, X2)
U22(X1, active(X2)) → U22(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
U23(mark(X)) → U23(X)
U23(active(X)) → U23(X)
U31(mark(X1), X2) → U31(X1, X2)
U31(X1, mark(X2)) → U31(X1, X2)
U31(active(X1), X2) → U31(X1, X2)
U31(X1, active(X2)) → U31(X1, X2)
U32(mark(X)) → U32(X)
U32(active(X)) → U32(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
U41(mark(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, mark(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, mark(X3)) → U41(X1, X2, X3)
U41(active(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, active(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, active(X3)) → U41(X1, X2, X3)
U42(mark(X1), X2) → U42(X1, X2)
U42(X1, mark(X2)) → U42(X1, X2)
U42(active(X1), X2) → U42(X1, X2)
U42(X1, active(X2)) → U42(X1, X2)
U43(mark(X)) → U43(X)
U43(active(X)) → U43(X)
U51(mark(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, mark(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, mark(X3)) → U51(X1, X2, X3)
U51(active(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, active(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, active(X3)) → U51(X1, X2, X3)
U52(mark(X1), X2) → U52(X1, X2)
U52(X1, mark(X2)) → U52(X1, X2)
U52(active(X1), X2) → U52(X1, X2)
U52(X1, active(X2)) → U52(X1, X2)
U53(mark(X)) → U53(X)
U53(active(X)) → U53(X)
U61(mark(X1), X2) → U61(X1, X2)
U61(X1, mark(X2)) → U61(X1, X2)
U61(active(X1), X2) → U61(X1, X2)
U61(X1, active(X2)) → U61(X1, X2)
U62(mark(X)) → U62(X)
U62(active(X)) → U62(X)
U71(mark(X1), X2) → U71(X1, X2)
U71(X1, mark(X2)) → U71(X1, X2)
U71(active(X1), X2) → U71(X1, X2)
U71(X1, active(X2)) → U71(X1, X2)
U72(mark(X)) → U72(X)
U72(active(X)) → U72(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isPalListKind(mark(X)) → isPalListKind(X)
isPalListKind(active(X)) → isPalListKind(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)
_2 > U213 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U213 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > U213 > [U222, isList1, U522] > U531 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U213 > [U222, isList1, U522] > U531 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > U413 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U413 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > U413 > [U222, isList1, U522] > U531 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U413 > [U222, isList1, U522] > U531 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > U513 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U513 > [U222, isList1, U522] > U112 > U121 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > U513 > [U222, isList1, U522] > U531 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > U513 > [U222, isList1, U522] > U531 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > and2 > [U312, U321]
_2 > isPal1 > [nil, tt] > [isNeList1, U422] > [U312, U321]
_2 > isPal1 > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2 > isPal1 > U712 > isNePal1 > U612 > [U312, U321]
a > [nil, tt] > [isNeList1, U422] > [U312, U321]
a > [nil, tt] > isNePal1 > U612 > [U312, U321]
e > [nil, tt] > [isNeList1, U422] > [U312, U321]
e > [nil, tt] > isNePal1 > U612 > [U312, U321]
i > [nil, tt] > [isNeList1, U422] > [U312, U321]
i > [nil, tt] > isNePal1 > U612 > [U312, U321]
o > [nil, tt] > [isNeList1, U422] > [U312, U321]
o > [nil, tt] > isNePal1 > U612 > [U312, U321]
u > [nil, tt] > [isNeList1, U422] > [U312, U321]
u > [nil, tt] > isNePal1 > U612 > [U312, U321]
_2: [1,2]
nil: multiset
U112: multiset
tt: multiset
U121: multiset
isNeList1: [1]
U213: [2,1,3]
U222: multiset
isList1: multiset
U312: [2,1]
U321: [1]
U413: [2,3,1]
U422: [2,1]
U513: [3,2,1]
U522: multiset
U531: [1]
U612: [2,1]
U712: multiset
isNePal1: [1]
and2: multiset
isPal1: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt, V)) → mark(U12(isNeList(V)))
active(U12(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isList(V1), V2))
active(U22(tt, V2)) → mark(U23(isList(V2)))
active(U31(tt, V)) → mark(U32(isQid(V)))
active(U32(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isList(V1), V2))
active(U42(tt, V2)) → mark(U43(isNeList(V2)))
active(U51(tt, V1, V2)) → mark(U52(isNeList(V1), V2))
active(U52(tt, V2)) → mark(U53(isList(V2)))
active(U53(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isQid(V)))
active(U71(tt, V)) → mark(U72(isNePal(V)))
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))))
active(isPal(V)) → mark(U71(isPalListKind(V), V))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(V1, V2))) → mark(and(isPalListKind(V1), isPalListKind(V2)))
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(U23(tt)) → mark(tt)
active(U43(tt)) → mark(tt)
active(U62(tt)) → mark(tt)
active(U72(tt)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNeList(X)) → active(isNeList(X))
mark(U21(X1, X2, X3)) → active(U21(mark(X1), X2, X3))
mark(U22(X1, X2)) → active(U22(mark(X1), X2))
mark(isList(X)) → active(isList(X))
mark(U23(X)) → active(U23(mark(X)))
mark(U31(X1, X2)) → active(U31(mark(X1), X2))
mark(U32(X)) → active(U32(mark(X)))
mark(isQid(X)) → active(isQid(X))
mark(U41(X1, X2, X3)) → active(U41(mark(X1), X2, X3))
mark(U42(X1, X2)) → active(U42(mark(X1), X2))
mark(U43(X)) → active(U43(mark(X)))
mark(U51(X1, X2, X3)) → active(U51(mark(X1), X2, X3))
mark(U52(X1, X2)) → active(U52(mark(X1), X2))
mark(U53(X)) → active(U53(mark(X)))
mark(U61(X1, X2)) → active(U61(mark(X1), X2))
mark(U62(X)) → active(U62(mark(X)))
mark(U71(X1, X2)) → active(U71(mark(X1), X2))
mark(U72(X)) → active(U72(mark(X)))
mark(isNePal(X)) → active(isNePal(X))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isPalListKind(X)) → active(isPalListKind(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
U21(mark(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, mark(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, mark(X3)) → U21(X1, X2, X3)
U21(active(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, active(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, active(X3)) → U21(X1, X2, X3)
U22(mark(X1), X2) → U22(X1, X2)
U22(X1, mark(X2)) → U22(X1, X2)
U22(active(X1), X2) → U22(X1, X2)
U22(X1, active(X2)) → U22(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
U23(mark(X)) → U23(X)
U23(active(X)) → U23(X)
U31(mark(X1), X2) → U31(X1, X2)
U31(X1, mark(X2)) → U31(X1, X2)
U31(active(X1), X2) → U31(X1, X2)
U31(X1, active(X2)) → U31(X1, X2)
U32(mark(X)) → U32(X)
U32(active(X)) → U32(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
U41(mark(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, mark(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, mark(X3)) → U41(X1, X2, X3)
U41(active(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, active(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, active(X3)) → U41(X1, X2, X3)
U42(mark(X1), X2) → U42(X1, X2)
U42(X1, mark(X2)) → U42(X1, X2)
U42(active(X1), X2) → U42(X1, X2)
U42(X1, active(X2)) → U42(X1, X2)
U43(mark(X)) → U43(X)
U43(active(X)) → U43(X)
U51(mark(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, mark(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, mark(X3)) → U51(X1, X2, X3)
U51(active(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, active(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, active(X3)) → U51(X1, X2, X3)
U52(mark(X1), X2) → U52(X1, X2)
U52(X1, mark(X2)) → U52(X1, X2)
U52(active(X1), X2) → U52(X1, X2)
U52(X1, active(X2)) → U52(X1, X2)
U53(mark(X)) → U53(X)
U53(active(X)) → U53(X)
U61(mark(X1), X2) → U61(X1, X2)
U61(X1, mark(X2)) → U61(X1, X2)
U61(active(X1), X2) → U61(X1, X2)
U61(X1, active(X2)) → U61(X1, X2)
U62(mark(X)) → U62(X)
U62(active(X)) → U62(X)
U71(mark(X1), X2) → U71(X1, X2)
U71(X1, mark(X2)) → U71(X1, X2)
U71(active(X1), X2) → U71(X1, X2)
U71(X1, active(X2)) → U71(X1, X2)
U72(mark(X)) → U72(X)
U72(active(X)) → U72(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isPalListKind(mark(X)) → isPalListKind(X)
isPalListKind(active(X)) → isPalListKind(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(U11(x1, x2)) = 1 + x1 + x2
POL(U12(x1)) = 2·x1
POL(U21(x1, x2, x3)) = x1 + x2 + x3
POL(U22(x1, x2)) = x1 + x2
POL(U23(x1)) = 2 + x1
POL(U31(x1, x2)) = 2·x1 + x2
POL(U32(x1)) = x1
POL(U41(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(U42(x1, x2)) = x1 + x2
POL(U43(x1)) = 1 + 2·x1
POL(U51(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U52(x1, x2)) = 1 + x1 + 2·x2
POL(U53(x1)) = 1 + x1
POL(U61(x1, x2)) = 1 + x1 + x2
POL(U62(x1)) = 1 + 2·x1
POL(U71(x1, x2)) = 2·x1 + 2·x2
POL(U72(x1)) = 2·x1
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2
POL(a) = 1
POL(active(x1)) = x1
POL(and(x1, x2)) = 1 + x1 + 2·x2
POL(e) = 1
POL(i) = 1
POL(isList(x1)) = 2 + x1
POL(isNeList(x1)) = 1 + x1
POL(isNePal(x1)) = 1 + x1
POL(isPal(x1)) = 1 + x1
POL(isPalListKind(x1)) = 1 + 2·x1
POL(isQid(x1)) = 2 + 2·x1
POL(mark(x1)) = x1
POL(nil) = 1
POL(o) = 1
POL(tt) = 2
POL(u) = 1
active(U23(tt)) → mark(tt)
active(U43(tt)) → mark(tt)
active(U62(tt)) → mark(tt)
active(U72(tt)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNeList(X)) → active(isNeList(X))
mark(U21(X1, X2, X3)) → active(U21(mark(X1), X2, X3))
mark(U22(X1, X2)) → active(U22(mark(X1), X2))
mark(isList(X)) → active(isList(X))
mark(U23(X)) → active(U23(mark(X)))
mark(U31(X1, X2)) → active(U31(mark(X1), X2))
mark(U32(X)) → active(U32(mark(X)))
mark(isQid(X)) → active(isQid(X))
mark(U41(X1, X2, X3)) → active(U41(mark(X1), X2, X3))
mark(U42(X1, X2)) → active(U42(mark(X1), X2))
mark(U43(X)) → active(U43(mark(X)))
mark(U51(X1, X2, X3)) → active(U51(mark(X1), X2, X3))
mark(U52(X1, X2)) → active(U52(mark(X1), X2))
mark(U53(X)) → active(U53(mark(X)))
mark(U61(X1, X2)) → active(U61(mark(X1), X2))
mark(U62(X)) → active(U62(mark(X)))
mark(U71(X1, X2)) → active(U71(mark(X1), X2))
mark(U72(X)) → active(U72(mark(X)))
mark(isNePal(X)) → active(isNePal(X))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isPalListKind(X)) → active(isPalListKind(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
U21(mark(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, mark(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, mark(X3)) → U21(X1, X2, X3)
U21(active(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, active(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, active(X3)) → U21(X1, X2, X3)
U22(mark(X1), X2) → U22(X1, X2)
U22(X1, mark(X2)) → U22(X1, X2)
U22(active(X1), X2) → U22(X1, X2)
U22(X1, active(X2)) → U22(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
U23(mark(X)) → U23(X)
U23(active(X)) → U23(X)
U31(mark(X1), X2) → U31(X1, X2)
U31(X1, mark(X2)) → U31(X1, X2)
U31(active(X1), X2) → U31(X1, X2)
U31(X1, active(X2)) → U31(X1, X2)
U32(mark(X)) → U32(X)
U32(active(X)) → U32(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
U41(mark(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, mark(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, mark(X3)) → U41(X1, X2, X3)
U41(active(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, active(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, active(X3)) → U41(X1, X2, X3)
U42(mark(X1), X2) → U42(X1, X2)
U42(X1, mark(X2)) → U42(X1, X2)
U42(active(X1), X2) → U42(X1, X2)
U42(X1, active(X2)) → U42(X1, X2)
U43(mark(X)) → U43(X)
U43(active(X)) → U43(X)
U51(mark(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, mark(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, mark(X3)) → U51(X1, X2, X3)
U51(active(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, active(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, active(X3)) → U51(X1, X2, X3)
U52(mark(X1), X2) → U52(X1, X2)
U52(X1, mark(X2)) → U52(X1, X2)
U52(active(X1), X2) → U52(X1, X2)
U52(X1, active(X2)) → U52(X1, X2)
U53(mark(X)) → U53(X)
U53(active(X)) → U53(X)
U61(mark(X1), X2) → U61(X1, X2)
U61(X1, mark(X2)) → U61(X1, X2)
U61(active(X1), X2) → U61(X1, X2)
U61(X1, active(X2)) → U61(X1, X2)
U62(mark(X)) → U62(X)
U62(active(X)) → U62(X)
U71(mark(X1), X2) → U71(X1, X2)
U71(X1, mark(X2)) → U71(X1, X2)
U71(active(X1), X2) → U71(X1, X2)
U71(X1, active(X2)) → U71(X1, X2)
U72(mark(X)) → U72(X)
U72(active(X)) → U72(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isPalListKind(mark(X)) → isPalListKind(X)
isPalListKind(active(X)) → isPalListKind(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(U11(x1, x2)) = 2 + x1 + x2
POL(U12(x1)) = 2 + x1
POL(U21(x1, x2, x3)) = 2 + x1 + x2 + x3
POL(U22(x1, x2)) = 2 + x1 + x2
POL(U23(x1)) = 2 + x1
POL(U31(x1, x2)) = 2 + x1 + x2
POL(U32(x1)) = 2 + x1
POL(U41(x1, x2, x3)) = 2 + x1 + x2 + x3
POL(U42(x1, x2)) = 2 + x1 + x2
POL(U43(x1)) = 2 + x1
POL(U51(x1, x2, x3)) = 2 + x1 + x2 + x3
POL(U52(x1, x2)) = 2 + x1 + x2
POL(U53(x1)) = 2 + x1
POL(U61(x1, x2)) = 2 + x1 + x2
POL(U62(x1)) = 2 + x1
POL(U71(x1, x2)) = 2 + x1 + x2
POL(U72(x1)) = 2 + x1
POL(__(x1, x2)) = 2 + x1 + x2
POL(a) = 1
POL(active(x1)) = 1 + x1
POL(and(x1, x2)) = 2 + x1 + x2
POL(e) = 1
POL(i) = 1
POL(isList(x1)) = 1 + x1
POL(isNeList(x1)) = 1 + x1
POL(isNePal(x1)) = 1 + x1
POL(isPal(x1)) = 1 + x1
POL(isPalListKind(x1)) = 1 + x1
POL(isQid(x1)) = 1 + x1
POL(mark(x1)) = 1 + 2·x1
POL(nil) = 0
POL(o) = 1
POL(tt) = 1
POL(u) = 1
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNeList(X)) → active(isNeList(X))
mark(U21(X1, X2, X3)) → active(U21(mark(X1), X2, X3))
mark(U22(X1, X2)) → active(U22(mark(X1), X2))
mark(isList(X)) → active(isList(X))
mark(U23(X)) → active(U23(mark(X)))
mark(U31(X1, X2)) → active(U31(mark(X1), X2))
mark(U32(X)) → active(U32(mark(X)))
mark(isQid(X)) → active(isQid(X))
mark(U41(X1, X2, X3)) → active(U41(mark(X1), X2, X3))
mark(U42(X1, X2)) → active(U42(mark(X1), X2))
mark(U43(X)) → active(U43(mark(X)))
mark(U51(X1, X2, X3)) → active(U51(mark(X1), X2, X3))
mark(U52(X1, X2)) → active(U52(mark(X1), X2))
mark(U53(X)) → active(U53(mark(X)))
mark(U61(X1, X2)) → active(U61(mark(X1), X2))
mark(U62(X)) → active(U62(mark(X)))
mark(U71(X1, X2)) → active(U71(mark(X1), X2))
mark(U72(X)) → active(U72(mark(X)))
mark(isNePal(X)) → active(isNePal(X))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isPalListKind(X)) → active(isPalListKind(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
U21(mark(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, mark(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, mark(X3)) → U21(X1, X2, X3)
U21(active(X1), X2, X3) → U21(X1, X2, X3)
U21(X1, active(X2), X3) → U21(X1, X2, X3)
U21(X1, X2, active(X3)) → U21(X1, X2, X3)
U22(mark(X1), X2) → U22(X1, X2)
U22(X1, mark(X2)) → U22(X1, X2)
U22(active(X1), X2) → U22(X1, X2)
U22(X1, active(X2)) → U22(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
U23(mark(X)) → U23(X)
U23(active(X)) → U23(X)
U31(mark(X1), X2) → U31(X1, X2)
U31(X1, mark(X2)) → U31(X1, X2)
U31(active(X1), X2) → U31(X1, X2)
U31(X1, active(X2)) → U31(X1, X2)
U32(mark(X)) → U32(X)
U32(active(X)) → U32(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
U41(mark(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, mark(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, mark(X3)) → U41(X1, X2, X3)
U41(active(X1), X2, X3) → U41(X1, X2, X3)
U41(X1, active(X2), X3) → U41(X1, X2, X3)
U41(X1, X2, active(X3)) → U41(X1, X2, X3)
U42(mark(X1), X2) → U42(X1, X2)
U42(X1, mark(X2)) → U42(X1, X2)
U42(active(X1), X2) → U42(X1, X2)
U42(X1, active(X2)) → U42(X1, X2)
U43(mark(X)) → U43(X)
U43(active(X)) → U43(X)
U51(mark(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, mark(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, mark(X3)) → U51(X1, X2, X3)
U51(active(X1), X2, X3) → U51(X1, X2, X3)
U51(X1, active(X2), X3) → U51(X1, X2, X3)
U51(X1, X2, active(X3)) → U51(X1, X2, X3)
U52(mark(X1), X2) → U52(X1, X2)
U52(X1, mark(X2)) → U52(X1, X2)
U52(active(X1), X2) → U52(X1, X2)
U52(X1, active(X2)) → U52(X1, X2)
U53(mark(X)) → U53(X)
U53(active(X)) → U53(X)
U61(mark(X1), X2) → U61(X1, X2)
U61(X1, mark(X2)) → U61(X1, X2)
U61(active(X1), X2) → U61(X1, X2)
U61(X1, active(X2)) → U61(X1, X2)
U62(mark(X)) → U62(X)
U62(active(X)) → U62(X)
U71(mark(X1), X2) → U71(X1, X2)
U71(X1, mark(X2)) → U71(X1, X2)
U71(active(X1), X2) → U71(X1, X2)
U71(X1, active(X2)) → U71(X1, X2)
U72(mark(X)) → U72(X)
U72(active(X)) → U72(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isPalListKind(mark(X)) → isPalListKind(X)
isPalListKind(active(X)) → isPalListKind(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(__(x1, x2)) = 2 + x1 + x2
POL(active(x1)) = x1
POL(mark(x1)) = 1 + 2·x1
POL(nil) = 2
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)