Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 PoloCSRProof (⇔)
↳4 CSR
↳5 PoloCSRProof (⇔)
↳6 CSR
↳7 PoloCSRProof (⇔)
↳8 CSR
↳9 PoloCSRProof (⇔)
↳10 CSR
↳11 PoloCSRProof (⇔)
↳12 CSR
↳13 PoloCSRProof (⇔)
↳14 CSR
↳15 PoloCSRProof (⇔)
↳16 CSR
↳17 PoloCSRProof (⇔)
↳18 CSR
↳19 PoloCSRProof (⇔)
↳20 CSR
↳21 PoloCSRProof (⇔)
↳22 CSR
↳23 PoloCSRProof (⇔)
↳24 CSR
↳25 PoloCSRProof (⇔)
↳26 CSR
↳27 PoloCSRProof (⇔)
↳28 CSR
↳29 PoloCSRProof (⇔)
↳30 CSR
↳31 PoloCSRProof (⇔)
↳32 CSR
↳33 PoloCSRProof (⇔)
↳34 CSR
↳35 RisEmptyProof (⇔)
↳36 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt, V)) → mark(U12(isPalListKind(V), V))
active(U12(tt, V)) → mark(U13(isNeList(V)))
active(U13(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isPalListKind(V1), V1, V2))
active(U22(tt, V1, V2)) → mark(U23(isPalListKind(V2), V1, V2))
active(U23(tt, V1, V2)) → mark(U24(isPalListKind(V2), V1, V2))
active(U24(tt, V1, V2)) → mark(U25(isList(V1), V2))
active(U25(tt, V2)) → mark(U26(isList(V2)))
active(U26(tt)) → mark(tt)
active(U31(tt, V)) → mark(U32(isPalListKind(V), V))
active(U32(tt, V)) → mark(U33(isQid(V)))
active(U33(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isPalListKind(V1), V1, V2))
active(U42(tt, V1, V2)) → mark(U43(isPalListKind(V2), V1, V2))
active(U43(tt, V1, V2)) → mark(U44(isPalListKind(V2), V1, V2))
active(U44(tt, V1, V2)) → mark(U45(isList(V1), V2))
active(U45(tt, V2)) → mark(U46(isNeList(V2)))
active(U46(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isPalListKind(V1), V1, V2))
active(U52(tt, V1, V2)) → mark(U53(isPalListKind(V2), V1, V2))
active(U53(tt, V1, V2)) → mark(U54(isPalListKind(V2), V1, V2))
active(U54(tt, V1, V2)) → mark(U55(isNeList(V1), V2))
active(U55(tt, V2)) → mark(U56(isList(V2)))
active(U56(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isPalListKind(V), V))
active(U62(tt, V)) → mark(U63(isQid(V)))
active(U63(tt)) → mark(tt)
active(U71(tt, I, P)) → mark(U72(isPalListKind(I), P))
active(U72(tt, P)) → mark(U73(isPal(P), P))
active(U73(tt, P)) → mark(U74(isPalListKind(P)))
active(U74(tt)) → mark(tt)
active(U81(tt, V)) → mark(U82(isPalListKind(V), V))
active(U82(tt, V)) → mark(U83(isNePal(V)))
active(U83(tt)) → mark(tt)
active(U91(tt, V2)) → mark(U92(isPalListKind(V2)))
active(U92(tt)) → mark(tt)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(isPalListKind(V1), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(isPalListKind(V1), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(isPalListKind(V1), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), I, P))
active(isPal(V)) → mark(U81(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(U91(isPalListKind(V1), 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(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(U11(X1, X2)) → U11(active(X1), X2)
active(U12(X1, X2)) → U12(active(X1), X2)
active(U13(X)) → U13(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(U23(X1, X2, X3)) → U23(active(X1), X2, X3)
active(U24(X1, X2, X3)) → U24(active(X1), X2, X3)
active(U25(X1, X2)) → U25(active(X1), X2)
active(U26(X)) → U26(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X1, X2)) → U32(active(X1), X2)
active(U33(X)) → U33(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2, X3)) → U42(active(X1), X2, X3)
active(U43(X1, X2, X3)) → U43(active(X1), X2, X3)
active(U44(X1, X2, X3)) → U44(active(X1), X2, X3)
active(U45(X1, X2)) → U45(active(X1), X2)
active(U46(X)) → U46(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2, X3)) → U52(active(X1), X2, X3)
active(U53(X1, X2, X3)) → U53(active(X1), X2, X3)
active(U54(X1, X2, X3)) → U54(active(X1), X2, X3)
active(U55(X1, X2)) → U55(active(X1), X2)
active(U56(X)) → U56(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X1, X2)) → U62(active(X1), X2)
active(U63(X)) → U63(active(X))
active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)
active(U73(X1, X2)) → U73(active(X1), X2)
active(U74(X)) → U74(active(X))
active(U81(X1, X2)) → U81(active(X1), X2)
active(U82(X1, X2)) → U82(active(X1), X2)
active(U83(X)) → U83(active(X))
active(U91(X1, X2)) → U91(active(X1), X2)
active(U92(X)) → U92(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X1), X2) → mark(U12(X1, X2))
U13(mark(X)) → mark(U13(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
U23(mark(X1), X2, X3) → mark(U23(X1, X2, X3))
U24(mark(X1), X2, X3) → mark(U24(X1, X2, X3))
U25(mark(X1), X2) → mark(U25(X1, X2))
U26(mark(X)) → mark(U26(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X1), X2) → mark(U32(X1, X2))
U33(mark(X)) → mark(U33(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2, X3) → mark(U42(X1, X2, X3))
U43(mark(X1), X2, X3) → mark(U43(X1, X2, X3))
U44(mark(X1), X2, X3) → mark(U44(X1, X2, X3))
U45(mark(X1), X2) → mark(U45(X1, X2))
U46(mark(X)) → mark(U46(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2, X3) → mark(U52(X1, X2, X3))
U53(mark(X1), X2, X3) → mark(U53(X1, X2, X3))
U54(mark(X1), X2, X3) → mark(U54(X1, X2, X3))
U55(mark(X1), X2) → mark(U55(X1, X2))
U56(mark(X)) → mark(U56(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X1), X2) → mark(U62(X1, X2))
U63(mark(X)) → mark(U63(X))
U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))
U73(mark(X1), X2) → mark(U73(X1, X2))
U74(mark(X)) → mark(U74(X))
U81(mark(X1), X2) → mark(U81(X1, X2))
U82(mark(X1), X2) → mark(U82(X1, X2))
U83(mark(X)) → mark(U83(X))
U91(mark(X1), X2) → mark(U91(X1, X2))
U92(mark(X)) → mark(U92(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(U12(X1, X2)) → U12(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(U13(X)) → U13(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(U23(X1, X2, X3)) → U23(proper(X1), proper(X2), proper(X3))
proper(U24(X1, X2, X3)) → U24(proper(X1), proper(X2), proper(X3))
proper(U25(X1, X2)) → U25(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U26(X)) → U26(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X1, X2)) → U32(proper(X1), proper(X2))
proper(U33(X)) → U33(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2, X3)) → U42(proper(X1), proper(X2), proper(X3))
proper(U43(X1, X2, X3)) → U43(proper(X1), proper(X2), proper(X3))
proper(U44(X1, X2, X3)) → U44(proper(X1), proper(X2), proper(X3))
proper(U45(X1, X2)) → U45(proper(X1), proper(X2))
proper(U46(X)) → U46(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2, X3)) → U52(proper(X1), proper(X2), proper(X3))
proper(U53(X1, X2, X3)) → U53(proper(X1), proper(X2), proper(X3))
proper(U54(X1, X2, X3)) → U54(proper(X1), proper(X2), proper(X3))
proper(U55(X1, X2)) → U55(proper(X1), proper(X2))
proper(U56(X)) → U56(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X1, X2)) → U62(proper(X1), proper(X2))
proper(U63(X)) → U63(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))
proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(U73(X1, X2)) → U73(proper(X1), proper(X2))
proper(isPal(X)) → isPal(proper(X))
proper(U74(X)) → U74(proper(X))
proper(U81(X1, X2)) → U81(proper(X1), proper(X2))
proper(U82(X1, X2)) → U82(proper(X1), proper(X2))
proper(U83(X)) → U83(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(U91(X1, X2)) → U91(proper(X1), proper(X2))
proper(U92(X)) → U92(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
U12(ok(X1), ok(X2)) → ok(U12(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
U13(ok(X)) → ok(U13(X))
isNeList(ok(X)) → ok(isNeList(X))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
U23(ok(X1), ok(X2), ok(X3)) → ok(U23(X1, X2, X3))
U24(ok(X1), ok(X2), ok(X3)) → ok(U24(X1, X2, X3))
U25(ok(X1), ok(X2)) → ok(U25(X1, X2))
isList(ok(X)) → ok(isList(X))
U26(ok(X)) → ok(U26(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X1), ok(X2)) → ok(U32(X1, X2))
U33(ok(X)) → ok(U33(X))
isQid(ok(X)) → ok(isQid(X))
U41(ok(X1), ok(X2), ok(X3)) → ok(U41(X1, X2, X3))
U42(ok(X1), ok(X2), ok(X3)) → ok(U42(X1, X2, X3))
U43(ok(X1), ok(X2), ok(X3)) → ok(U43(X1, X2, X3))
U44(ok(X1), ok(X2), ok(X3)) → ok(U44(X1, X2, X3))
U45(ok(X1), ok(X2)) → ok(U45(X1, X2))
U46(ok(X)) → ok(U46(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2), ok(X3)) → ok(U52(X1, X2, X3))
U53(ok(X1), ok(X2), ok(X3)) → ok(U53(X1, X2, X3))
U54(ok(X1), ok(X2), ok(X3)) → ok(U54(X1, X2, X3))
U55(ok(X1), ok(X2)) → ok(U55(X1, X2))
U56(ok(X)) → ok(U56(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X1), ok(X2)) → ok(U62(X1, X2))
U63(ok(X)) → ok(U63(X))
U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))
U73(ok(X1), ok(X2)) → ok(U73(X1, X2))
isPal(ok(X)) → ok(isPal(X))
U74(ok(X)) → ok(U74(X))
U81(ok(X1), ok(X2)) → ok(U81(X1, X2))
U82(ok(X1), ok(X2)) → ok(U82(X1, X2))
U83(ok(X)) → ok(U83(X))
isNePal(ok(X)) → ok(isNePal(X))
U91(ok(X1), ok(X2)) → ok(U91(X1, X2))
U92(ok(X)) → ok(U92(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

(1) QTRSToCSRProof (EQUIVALENT transformation)

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt, V)) → mark(U12(isPalListKind(V), V))
active(U12(tt, V)) → mark(U13(isNeList(V)))
active(U13(tt)) → mark(tt)
active(U21(tt, V1, V2)) → mark(U22(isPalListKind(V1), V1, V2))
active(U22(tt, V1, V2)) → mark(U23(isPalListKind(V2), V1, V2))
active(U23(tt, V1, V2)) → mark(U24(isPalListKind(V2), V1, V2))
active(U24(tt, V1, V2)) → mark(U25(isList(V1), V2))
active(U25(tt, V2)) → mark(U26(isList(V2)))
active(U26(tt)) → mark(tt)
active(U31(tt, V)) → mark(U32(isPalListKind(V), V))
active(U32(tt, V)) → mark(U33(isQid(V)))
active(U33(tt)) → mark(tt)
active(U41(tt, V1, V2)) → mark(U42(isPalListKind(V1), V1, V2))
active(U42(tt, V1, V2)) → mark(U43(isPalListKind(V2), V1, V2))
active(U43(tt, V1, V2)) → mark(U44(isPalListKind(V2), V1, V2))
active(U44(tt, V1, V2)) → mark(U45(isList(V1), V2))
active(U45(tt, V2)) → mark(U46(isNeList(V2)))
active(U46(tt)) → mark(tt)
active(U51(tt, V1, V2)) → mark(U52(isPalListKind(V1), V1, V2))
active(U52(tt, V1, V2)) → mark(U53(isPalListKind(V2), V1, V2))
active(U53(tt, V1, V2)) → mark(U54(isPalListKind(V2), V1, V2))
active(U54(tt, V1, V2)) → mark(U55(isNeList(V1), V2))
active(U55(tt, V2)) → mark(U56(isList(V2)))
active(U56(tt)) → mark(tt)
active(U61(tt, V)) → mark(U62(isPalListKind(V), V))
active(U62(tt, V)) → mark(U63(isQid(V)))
active(U63(tt)) → mark(tt)
active(U71(tt, I, P)) → mark(U72(isPalListKind(I), P))
active(U72(tt, P)) → mark(U73(isPal(P), P))
active(U73(tt, P)) → mark(U74(isPalListKind(P)))
active(U74(tt)) → mark(tt)
active(U81(tt, V)) → mark(U82(isPalListKind(V), V))
active(U82(tt, V)) → mark(U83(isNePal(V)))
active(U83(tt)) → mark(tt)
active(U91(tt, V2)) → mark(U92(isPalListKind(V2)))
active(U92(tt)) → mark(tt)
active(isList(V)) → mark(U11(isPalListKind(V), V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(U21(isPalListKind(V1), V1, V2))
active(isNeList(V)) → mark(U31(isPalListKind(V), V))
active(isNeList(__(V1, V2))) → mark(U41(isPalListKind(V1), V1, V2))
active(isNeList(__(V1, V2))) → mark(U51(isPalListKind(V1), V1, V2))
active(isNePal(V)) → mark(U61(isPalListKind(V), V))
active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), I, P))
active(isPal(V)) → mark(U81(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(U91(isPalListKind(V1), 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(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(U11(X1, X2)) → U11(active(X1), X2)
active(U12(X1, X2)) → U12(active(X1), X2)
active(U13(X)) → U13(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(U23(X1, X2, X3)) → U23(active(X1), X2, X3)
active(U24(X1, X2, X3)) → U24(active(X1), X2, X3)
active(U25(X1, X2)) → U25(active(X1), X2)
active(U26(X)) → U26(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X1, X2)) → U32(active(X1), X2)
active(U33(X)) → U33(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2, X3)) → U42(active(X1), X2, X3)
active(U43(X1, X2, X3)) → U43(active(X1), X2, X3)
active(U44(X1, X2, X3)) → U44(active(X1), X2, X3)
active(U45(X1, X2)) → U45(active(X1), X2)
active(U46(X)) → U46(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2, X3)) → U52(active(X1), X2, X3)
active(U53(X1, X2, X3)) → U53(active(X1), X2, X3)
active(U54(X1, X2, X3)) → U54(active(X1), X2, X3)
active(U55(X1, X2)) → U55(active(X1), X2)
active(U56(X)) → U56(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X1, X2)) → U62(active(X1), X2)
active(U63(X)) → U63(active(X))
active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)
active(U73(X1, X2)) → U73(active(X1), X2)
active(U74(X)) → U74(active(X))
active(U81(X1, X2)) → U81(active(X1), X2)
active(U82(X1, X2)) → U82(active(X1), X2)
active(U83(X)) → U83(active(X))
active(U91(X1, X2)) → U91(active(X1), X2)
active(U92(X)) → U92(active(X))
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X1), X2) → mark(U12(X1, X2))
U13(mark(X)) → mark(U13(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
U23(mark(X1), X2, X3) → mark(U23(X1, X2, X3))
U24(mark(X1), X2, X3) → mark(U24(X1, X2, X3))
U25(mark(X1), X2) → mark(U25(X1, X2))
U26(mark(X)) → mark(U26(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X1), X2) → mark(U32(X1, X2))
U33(mark(X)) → mark(U33(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2, X3) → mark(U42(X1, X2, X3))
U43(mark(X1), X2, X3) → mark(U43(X1, X2, X3))
U44(mark(X1), X2, X3) → mark(U44(X1, X2, X3))
U45(mark(X1), X2) → mark(U45(X1, X2))
U46(mark(X)) → mark(U46(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2, X3) → mark(U52(X1, X2, X3))
U53(mark(X1), X2, X3) → mark(U53(X1, X2, X3))
U54(mark(X1), X2, X3) → mark(U54(X1, X2, X3))
U55(mark(X1), X2) → mark(U55(X1, X2))
U56(mark(X)) → mark(U56(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X1), X2) → mark(U62(X1, X2))
U63(mark(X)) → mark(U63(X))
U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))
U73(mark(X1), X2) → mark(U73(X1, X2))
U74(mark(X)) → mark(U74(X))
U81(mark(X1), X2) → mark(U81(X1, X2))
U82(mark(X1), X2) → mark(U82(X1, X2))
U83(mark(X)) → mark(U83(X))
U91(mark(X1), X2) → mark(U91(X1, X2))
U92(mark(X)) → mark(U92(X))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(U12(X1, X2)) → U12(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(U13(X)) → U13(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(U23(X1, X2, X3)) → U23(proper(X1), proper(X2), proper(X3))
proper(U24(X1, X2, X3)) → U24(proper(X1), proper(X2), proper(X3))
proper(U25(X1, X2)) → U25(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U26(X)) → U26(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X1, X2)) → U32(proper(X1), proper(X2))
proper(U33(X)) → U33(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2, X3)) → U42(proper(X1), proper(X2), proper(X3))
proper(U43(X1, X2, X3)) → U43(proper(X1), proper(X2), proper(X3))
proper(U44(X1, X2, X3)) → U44(proper(X1), proper(X2), proper(X3))
proper(U45(X1, X2)) → U45(proper(X1), proper(X2))
proper(U46(X)) → U46(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2, X3)) → U52(proper(X1), proper(X2), proper(X3))
proper(U53(X1, X2, X3)) → U53(proper(X1), proper(X2), proper(X3))
proper(U54(X1, X2, X3)) → U54(proper(X1), proper(X2), proper(X3))
proper(U55(X1, X2)) → U55(proper(X1), proper(X2))
proper(U56(X)) → U56(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X1, X2)) → U62(proper(X1), proper(X2))
proper(U63(X)) → U63(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))
proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(U73(X1, X2)) → U73(proper(X1), proper(X2))
proper(isPal(X)) → isPal(proper(X))
proper(U74(X)) → U74(proper(X))
proper(U81(X1, X2)) → U81(proper(X1), proper(X2))
proper(U82(X1, X2)) → U82(proper(X1), proper(X2))
proper(U83(X)) → U83(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(U91(X1, X2)) → U91(proper(X1), proper(X2))
proper(U92(X)) → U92(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
U12(ok(X1), ok(X2)) → ok(U12(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
U13(ok(X)) → ok(U13(X))
isNeList(ok(X)) → ok(isNeList(X))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
U23(ok(X1), ok(X2), ok(X3)) → ok(U23(X1, X2, X3))
U24(ok(X1), ok(X2), ok(X3)) → ok(U24(X1, X2, X3))
U25(ok(X1), ok(X2)) → ok(U25(X1, X2))
isList(ok(X)) → ok(isList(X))
U26(ok(X)) → ok(U26(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X1), ok(X2)) → ok(U32(X1, X2))
U33(ok(X)) → ok(U33(X))
isQid(ok(X)) → ok(isQid(X))
U41(ok(X1), ok(X2), ok(X3)) → ok(U41(X1, X2, X3))
U42(ok(X1), ok(X2), ok(X3)) → ok(U42(X1, X2, X3))
U43(ok(X1), ok(X2), ok(X3)) → ok(U43(X1, X2, X3))
U44(ok(X1), ok(X2), ok(X3)) → ok(U44(X1, X2, X3))
U45(ok(X1), ok(X2)) → ok(U45(X1, X2))
U46(ok(X)) → ok(U46(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2), ok(X3)) → ok(U52(X1, X2, X3))
U53(ok(X1), ok(X2), ok(X3)) → ok(U53(X1, X2, X3))
U54(ok(X1), ok(X2), ok(X3)) → ok(U54(X1, X2, X3))
U55(ok(X1), ok(X2)) → ok(U55(X1, X2))
U56(ok(X)) → ok(U56(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X1), ok(X2)) → ok(U62(X1, X2))
U63(ok(X)) → ok(U63(X))
U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))
U73(ok(X1), ok(X2)) → ok(U73(X1, X2))
isPal(ok(X)) → ok(isPal(X))
U74(ok(X)) → ok(U74(X))
U81(ok(X1), ok(X2)) → ok(U81(X1, X2))
U82(ok(X1), ok(X2)) → ok(U82(X1, X2))
U83(ok(X)) → ok(U83(X))
isNePal(ok(X)) → ok(isNePal(X))
U91(ok(X1), ok(X2)) → ok(U91(X1, X2))
U92(ok(X)) → ok(U92(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
Special symbols used for the transformation (see [GM04]):
top: top, active: active, mark: mark, ok: ok, proper: proper
The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).

(2) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(3) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

__(X, nil) → X
__(nil, X) → X
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2, x3)) = 2·x1   
POL(U23(x1, x2, x3)) = x1   
POL(U24(x1, x2, x3)) = x1   
POL(U25(x1, x2)) = x1   
POL(U26(x1)) = 2·x1   
POL(U31(x1, x2)) = x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = 2·x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2, x3)) = 2·x1   
POL(U53(x1, x2, x3)) = x1   
POL(U54(x1, x2, x3)) = 2·x1   
POL(U55(x1, x2)) = 2·x1   
POL(U56(x1)) = x1   
POL(U61(x1, x2)) = 2·x1   
POL(U62(x1, x2)) = 2·x1   
POL(U63(x1)) = 2·x1   
POL(U71(x1, x2, x3)) = 2·x1   
POL(U72(x1, x2)) = x1   
POL(U73(x1, x2)) = 2·x1   
POL(U74(x1)) = x1   
POL(U81(x1, x2)) = x1   
POL(U82(x1, x2)) = x1   
POL(U83(x1)) = 2·x1   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(a) = 1   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 1   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(4) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(5) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

isPal(nil) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = x1   
POL(U22(x1, x2, x3)) = 2·x1   
POL(U23(x1, x2, x3)) = x1   
POL(U24(x1, x2, x3)) = 2·x1   
POL(U25(x1, x2)) = 2·x1   
POL(U26(x1)) = 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = 2·x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2, x3)) = 2·x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U54(x1, x2, x3)) = x1   
POL(U55(x1, x2)) = x1   
POL(U56(x1)) = 2·x1   
POL(U61(x1, x2)) = x1 + 2·x2   
POL(U62(x1, x2)) = 2·x1 + x2   
POL(U63(x1)) = x1   
POL(U71(x1, x2, x3)) = x1 + 2·x3   
POL(U72(x1, x2)) = 2·x1 + 2·x2   
POL(U73(x1, x2)) = x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1, x2)) = x1 + 2·x2   
POL(U82(x1, x2)) = 2·x1 + 2·x2   
POL(U83(x1)) = x1   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(a) = 1   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 2·x1   
POL(isPal(x1)) = 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(6) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(7) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

__(__(X, Y), Z) → __(X, __(Y, Z))
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = x1   
POL(U21(x1, x2, x3)) = x1   
POL(U22(x1, x2, x3)) = 2·x1   
POL(U23(x1, x2, x3)) = x1   
POL(U24(x1, x2, x3)) = 2·x1   
POL(U25(x1, x2)) = x1   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = 2·x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U54(x1, x2, x3)) = 2·x1   
POL(U55(x1, x2)) = x1   
POL(U56(x1)) = x1   
POL(U61(x1, x2)) = 2·x1   
POL(U62(x1, x2)) = 2·x1   
POL(U63(x1)) = x1   
POL(U71(x1, x2, x3)) = 2·x1   
POL(U72(x1, x2)) = x1   
POL(U73(x1, x2)) = 2·x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1, x2)) = x1   
POL(U82(x1, x2)) = x1   
POL(U83(x1)) = 2·x1   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 0   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 1   


(8) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(9) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = x1   
POL(U22(x1, x2, x3)) = 2·x1   
POL(U23(x1, x2, x3)) = x1   
POL(U24(x1, x2, x3)) = 2·x1   
POL(U25(x1, x2)) = 2·x1   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = 2·x1   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = x1   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = 2·x1   
POL(U46(x1)) = x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U54(x1, x2, x3)) = x1   
POL(U55(x1, x2)) = x1   
POL(U56(x1)) = x1   
POL(U61(x1, x2)) = 2·x1 + x2   
POL(U62(x1, x2)) = 2·x1 + x2   
POL(U63(x1)) = x1   
POL(U71(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U72(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U73(x1, x2)) = x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U82(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U83(x1)) = 2·x1   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 1   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(10) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(11) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U61(tt, V) → U62(isPalListKind(V), V)
U63(tt) → tt
U83(tt) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = x1   
POL(U22(x1, x2, x3)) = 2·x1   
POL(U23(x1, x2, x3)) = 2·x1   
POL(U24(x1, x2, x3)) = 2·x1   
POL(U25(x1, x2)) = 2·x1   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = 2·x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = 2·x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = 2·x1   
POL(U52(x1, x2, x3)) = 2·x1   
POL(U53(x1, x2, x3)) = x1   
POL(U54(x1, x2, x3)) = x1   
POL(U55(x1, x2)) = 2·x1   
POL(U56(x1)) = 2·x1   
POL(U61(x1, x2)) = 2 + x1 + 2·x2   
POL(U62(x1, x2)) = 1 + x1 + x2   
POL(U63(x1)) = 1 + x1   
POL(U71(x1, x2, x3)) = 2·x1 + x2 + 2·x3   
POL(U72(x1, x2)) = 2·x1 + 2·x2   
POL(U73(x1, x2)) = 2·x1 + x2   
POL(U74(x1)) = 2·x1   
POL(U81(x1, x2)) = x1   
POL(U83(x1)) = 1 + x1   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 2   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(12) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U62(tt, V) → U63(isQid(V))
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(13) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U71(tt, I, P) → U72(isPalListKind(I), P)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1 + x2   
POL(U12(x1, x2)) = 2·x1 + x2   
POL(U13(x1)) = x1   
POL(U21(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U22(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U23(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U24(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U25(x1, x2)) = x1 + x2   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1 + x2   
POL(U32(x1, x2)) = x1 + x2   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U42(x1, x2, x3)) = 2 + x1 + x2 + 2·x3   
POL(U43(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U44(x1, x2, x3)) = 2·x1 + x2 + 2·x3   
POL(U45(x1, x2)) = x1 + x2   
POL(U46(x1)) = x1   
POL(U51(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U52(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U53(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U54(x1, x2, x3)) = x1 + x2 + 2·x3   
POL(U55(x1, x2)) = x1 + x2   
POL(U56(x1)) = x1   
POL(U61(x1, x2)) = 1 + 2·x1 + x2   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(U63(x1)) = 1 + x1   
POL(U71(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U72(x1, x2)) = 2·x1 + x2   
POL(U73(x1, x2)) = x1   
POL(U74(x1)) = x1   
POL(U81(x1, x2)) = 2·x1 + x2   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 2   
POL(e) = 2   
POL(i) = 1   
POL(isList(x1)) = x1   
POL(isNeList(x1)) = x1   
POL(isNePal(x1)) = 1 + 2·x1   
POL(isPal(x1)) = x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(14) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U62(tt, V) → U63(isQid(V))
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(15) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U54(tt, V1, V2) → U55(isNeList(V1), V2)
isNePal(V) → U61(isPalListKind(V), V)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U23(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U24(x1, x2, x3)) = 2·x1 + 2·x2   
POL(U25(x1, x2)) = x1   
POL(U26(x1)) = 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = 2·x1   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = x1 + x2 + 2·x3   
POL(U45(x1, x2)) = x1 + 2·x2   
POL(U46(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U54(x1, x2, x3)) = 2 + x1 + x2 + x3   
POL(U55(x1, x2)) = 2·x1   
POL(U56(x1)) = 2·x1   
POL(U61(x1, x2)) = 1 + 2·x1 + x2   
POL(U62(x1, x2)) = 2·x1 + x2   
POL(U63(x1)) = 2·x1   
POL(U72(x1, x2)) = 2 + x1 + 2·x2   
POL(U73(x1, x2)) = 2·x1   
POL(U74(x1)) = x1   
POL(U81(x1, x2)) = 1 + x1   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + 2·x2   
POL(a) = 2   
POL(e) = 1   
POL(i) = 1   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   


(16) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U62(tt, V) → U63(isQid(V))
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U55: {1}
U56: {1}
U62: {1}
U63: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(17) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U24(tt, V1, V2) → U25(isList(V1), V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U56(tt) → tt
U72(tt, P) → U73(isPal(P), P)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = x1   
POL(U22(x1, x2, x3)) = 2 + x1 + 2·x2 + 2·x3   
POL(U23(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U24(x1, x2, x3)) = 2 + x1 + 2·x2 + 2·x3   
POL(U25(x1, x2)) = 2·x1 + x2   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U44(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U45(x1, x2)) = x1 + x2   
POL(U46(x1)) = x1   
POL(U51(x1, x2, x3)) = 2·x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U55(x1, x2)) = 1 + 2·x1 + x2   
POL(U56(x1)) = 1 + 2·x1   
POL(U62(x1, x2)) = 1 + x1 + x2   
POL(U63(x1)) = 1 + 2·x1   
POL(U72(x1, x2)) = 2 + x1 + x2   
POL(U73(x1, x2)) = 2·x1   
POL(U74(x1)) = x1   
POL(U81(x1, x2)) = x1   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + 2·x2   
POL(a) = 1   
POL(e) = 1   
POL(i) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 1   


(18) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U55(tt, V2) → U56(isList(V2))
U62(tt, V) → U63(isQid(V))
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U55: {1}
U56: {1}
U62: {1}
U63: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(19) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U55(tt, V2) → U56(isList(V2))
U62(tt, V) → U63(isQid(V))
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = x1   
POL(U13(x1)) = x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3   
POL(U23(x1, x2, x3)) = 1 + 2·x1 + x2   
POL(U24(x1, x2, x3)) = 2·x1   
POL(U25(x1, x2)) = 1 + 2·x1   
POL(U26(x1)) = 1 + 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = 2·x1   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U45(x1, x2)) = 2 + 2·x1 + x2   
POL(U46(x1)) = 1 + x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = 2·x1   
POL(U55(x1, x2)) = 2 + x1 + x2   
POL(U56(x1)) = 1 + 2·x1   
POL(U62(x1, x2)) = 2 + 2·x1 + x2   
POL(U63(x1)) = 1 + x1   
POL(U73(x1, x2)) = 2 + x1 + x2   
POL(U74(x1)) = 1 + 2·x1   
POL(U81(x1, x2)) = x1 + 2·x2   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 1   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isPal(x1)) = 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(20) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U25(tt, V2) → U26(isList(V2))
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isPal(V) → U81(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
isPal: empty set
U81: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(21) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U12(tt, V) → U13(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isPal(V) → U81(isPalListKind(V), V)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2 + 2·x1   
POL(U12(x1, x2)) = 2 + 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 1 + 2·x1   
POL(U25(x1, x2)) = 2 + 2·x1 + x2   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2, x3)) = x1   
POL(U43(x1, x2, x3)) = x1   
POL(U51(x1, x2, x3)) = 2·x1   
POL(U52(x1, x2, x3)) = x1   
POL(U53(x1, x2, x3)) = x1   
POL(U81(x1, x2)) = 1 + x1   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + 2·x2   
POL(a) = 1   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = 2   
POL(isNeList(x1)) = 0   
POL(isPal(x1)) = 2 + x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(22) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U13(tt) → tt
U25(tt, V2) → U26(isList(V2))
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(23) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U13(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
isList(V) → U11(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1, x2)) = x1   
POL(U13(x1)) = 1 + 2·x1   
POL(U25(x1, x2)) = 2 + x1 + 2·x2   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 2·x1 + 2·x2   
POL(U32(x1, x2)) = x1 + x2   
POL(U33(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2 + 2·x1 + x2 + x3   
POL(U42(x1, x2, x3)) = 1 + x1   
POL(U43(x1, x2, x3)) = 1 + x1   
POL(U51(x1, x2, x3)) = 2 + x1 + 2·x2 + 2·x3   
POL(U52(x1, x2, x3)) = 2 + x1 + x3   
POL(U53(x1, x2, x3)) = 2 + 2·x1   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2 + x1 + x2   
POL(a) = 1   
POL(e) = 0   
POL(i) = 1   
POL(isList(x1)) = 2 + 2·x1   
POL(isNeList(x1)) = 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 2   


(24) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, V) → U12(isPalListKind(V), V)
U25(tt, V2) → U26(isList(V2))
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
isNeList: empty set
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(25) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U11(tt, V) → U12(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2 + x1   
POL(U12(x1, x2)) = 1 + 2·x1   
POL(U25(x1, x2)) = 1 + 2·x1 + x2   
POL(U26(x1)) = x1   
POL(U31(x1, x2)) = 1 + x1   
POL(U32(x1, x2)) = 1 + 2·x1   
POL(U33(x1)) = x1   
POL(U42(x1, x2, x3)) = 2 + x1 + 2·x2 + 2·x3   
POL(U43(x1, x2, x3)) = 1 + 2·x1 + x3   
POL(U51(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U52(x1, x2, x3)) = 1 + 2·x1 + 2·x3   
POL(U53(x1, x2, x3)) = 1 + 2·x1 + x3   
POL(U91(x1, x2)) = x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = x1 + 2·x2   
POL(a) = 1   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 1   
POL(isNeList(x1)) = 1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 1   


(26) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U25(tt, V2) → U26(isList(V2))
U31(tt, V) → U32(isPalListKind(V), V)
U33(tt) → tt
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
tt: empty set
isPalListKind: empty set
isNeList: empty set
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U52: {1}
U53: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(27) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U33(tt) → tt
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U25(x1, x2)) = 1 + x1 + x2   
POL(U26(x1)) = 1 + 2·x1   
POL(U31(x1, x2)) = x1 + x2   
POL(U32(x1, x2)) = x1   
POL(U33(x1)) = 1 + 2·x1   
POL(U52(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U53(x1, x2, x3)) = 1 + x1 + x2 + 2·x3   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 0   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 1 + 2·x1   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 1   


(28) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U25(tt, V2) → U26(isList(V2))
U31(tt, V) → U32(isPalListKind(V), V)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
tt: empty set
isPalListKind: empty set
isNeList: empty set
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

(29) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U25(tt, V2) → U26(isList(V2))
U92(tt) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
Used ordering:
Polynomial interpretation [POLO]:

POL(U25(x1, x2)) = 2·x1 + 2·x2   
POL(U26(x1)) = 1 + x1   
POL(U31(x1, x2)) = x1 + x2   
POL(U32(x1, x2)) = x1   
POL(U91(x1, x2)) = 1 + x1 + x2   
POL(U92(x1)) = 1 + x1   
POL(__(x1, x2)) = 2 + x1 + 2·x2   
POL(a) = 0   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 2 + x1   
POL(isNeList(x1)) = 2 + 2·x1   
POL(isPalListKind(x1)) = 2 + x1   
POL(nil) = 2   
POL(o) = 0   
POL(tt) = 2   
POL(u) = 0   


(30) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U31(tt, V) → U32(isPalListKind(V), V)
U91(tt, V2) → U92(isPalListKind(V2))
isNeList(V) → U31(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt

The replacement map contains the following entries:

tt: empty set
isPalListKind: empty set
isNeList: empty set
U31: {1}
U32: {1}
U91: {1}
U92: {1}
a: empty set
o: empty set
u: empty set

(31) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U91(tt, V2) → U92(isPalListKind(V2))
isNeList(V) → U31(isPalListKind(V), V)
Used ordering:
Polynomial interpretation [POLO]:

POL(U31(x1, x2)) = x1   
POL(U32(x1, x2)) = 2·x1   
POL(U91(x1, x2)) = 2 + x1   
POL(U92(x1)) = 1 + 2·x1   
POL(a) = 2   
POL(isNeList(x1)) = 2 + x1   
POL(isPalListKind(x1)) = 0   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 0   


(32) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U31(tt, V) → U32(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt

The replacement map contains the following entries:

tt: empty set
isPalListKind: empty set
U31: {1}
U32: {1}
a: empty set
o: empty set
u: empty set

(33) PoloCSRProof (EQUIVALENT transformation)

The following rules can be removed because they are oriented strictly by a µ-monotonic polynomial ordering:

U31(tt, V) → U32(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U31(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U32(x1, x2)) = 1 + x1   
POL(a) = 2   
POL(isPalListKind(x1)) = 2 + 2·x1   
POL(o) = 2   
POL(tt) = 1   
POL(u) = 2   


(34) Obligation:

Context-sensitive rewrite system:
R is empty.

(35) RisEmptyProof (EQUIVALENT transformation)

The CSR R is empty. Hence, termination is trivially proven.

(36) TRUE