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 RisEmptyProof (⇔)
↳30 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(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)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(U11(X1, X2)) → U11(active(X1), X2)
active(U12(X)) → U12(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2)) → U22(active(X1), X2)
active(U23(X)) → U23(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X)) → U32(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2)) → U42(active(X1), X2)
active(U43(X)) → U43(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2)) → U52(active(X1), X2)
active(U53(X)) → U53(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))
active(U71(X1, X2)) → U71(active(X1), X2)
active(U72(X)) → U72(active(X))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X)) → mark(U12(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2) → mark(U22(X1, X2))
U23(mark(X)) → mark(U23(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X)) → mark(U32(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2) → mark(U42(X1, X2))
U43(mark(X)) → mark(U43(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2) → mark(U52(X1, X2))
U53(mark(X)) → mark(U53(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))
U71(mark(X1), X2) → mark(U71(X1, X2))
U72(mark(X)) → mark(U72(X))
and(mark(X1), X2) → mark(and(X1, X2))
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(X)) → U12(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2)) → U22(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U23(X)) → U23(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X)) → U32(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2)) → U42(proper(X1), proper(X2))
proper(U43(X)) → U43(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2)) → U52(proper(X1), proper(X2))
proper(U53(X)) → U53(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2)) → U71(proper(X1), proper(X2))
proper(U72(X)) → U72(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(isPal(X)) → isPal(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(X)) → ok(U12(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(U22(X1, X2))
isList(ok(X)) → ok(isList(X))
U23(ok(X)) → ok(U23(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X)) → ok(U32(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(U42(X1, X2))
U43(ok(X)) → ok(U43(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2)) → ok(U52(X1, X2))
U53(ok(X)) → ok(U53(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))
U71(ok(X1), ok(X2)) → ok(U71(X1, X2))
U72(ok(X)) → ok(U72(X))
isNePal(ok(X)) → ok(isNePal(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
isPal(ok(X)) → ok(isPal(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(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)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(U11(X1, X2)) → U11(active(X1), X2)
active(U12(X)) → U12(active(X))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2)) → U22(active(X1), X2)
active(U23(X)) → U23(active(X))
active(U31(X1, X2)) → U31(active(X1), X2)
active(U32(X)) → U32(active(X))
active(U41(X1, X2, X3)) → U41(active(X1), X2, X3)
active(U42(X1, X2)) → U42(active(X1), X2)
active(U43(X)) → U43(active(X))
active(U51(X1, X2, X3)) → U51(active(X1), X2, X3)
active(U52(X1, X2)) → U52(active(X1), X2)
active(U53(X)) → U53(active(X))
active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))
active(U71(X1, X2)) → U71(active(X1), X2)
active(U72(X)) → U72(active(X))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
U12(mark(X)) → mark(U12(X))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2) → mark(U22(X1, X2))
U23(mark(X)) → mark(U23(X))
U31(mark(X1), X2) → mark(U31(X1, X2))
U32(mark(X)) → mark(U32(X))
U41(mark(X1), X2, X3) → mark(U41(X1, X2, X3))
U42(mark(X1), X2) → mark(U42(X1, X2))
U43(mark(X)) → mark(U43(X))
U51(mark(X1), X2, X3) → mark(U51(X1, X2, X3))
U52(mark(X1), X2) → mark(U52(X1, X2))
U53(mark(X)) → mark(U53(X))
U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))
U71(mark(X1), X2) → mark(U71(X1, X2))
U72(mark(X)) → mark(U72(X))
and(mark(X1), X2) → mark(and(X1, X2))
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(X)) → U12(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2)) → U22(proper(X1), proper(X2))
proper(isList(X)) → isList(proper(X))
proper(U23(X)) → U23(proper(X))
proper(U31(X1, X2)) → U31(proper(X1), proper(X2))
proper(U32(X)) → U32(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(U41(X1, X2, X3)) → U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2)) → U42(proper(X1), proper(X2))
proper(U43(X)) → U43(proper(X))
proper(U51(X1, X2, X3)) → U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2)) → U52(proper(X1), proper(X2))
proper(U53(X)) → U53(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))
proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2)) → U71(proper(X1), proper(X2))
proper(U72(X)) → U72(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isPalListKind(X)) → isPalListKind(proper(X))
proper(isPal(X)) → isPal(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(X)) → ok(U12(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(U22(X1, X2))
isList(ok(X)) → ok(isList(X))
U23(ok(X)) → ok(U23(X))
U31(ok(X1), ok(X2)) → ok(U31(X1, X2))
U32(ok(X)) → ok(U32(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(U42(X1, X2))
U43(ok(X)) → ok(U43(X))
U51(ok(X1), ok(X2), ok(X3)) → ok(U51(X1, X2, X3))
U52(ok(X1), ok(X2)) → ok(U52(X1, X2))
U53(ok(X)) → ok(U53(X))
U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))
U71(ok(X1), ok(X2)) → ok(U71(X1, X2))
U72(ok(X)) → ok(U72(X))
isNePal(ok(X)) → ok(isNePal(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isPalListKind(ok(X)) → ok(isPalListKind(X))
isPal(ok(X)) → ok(isPal(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: empty set
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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: empty set
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)) = 2·x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2)) = x1   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = x1   
POL(U42(x1, x2)) = 2·x1   
POL(U43(x1)) = x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2)) = 2·x1   
POL(U53(x1)) = 2·x1   
POL(U61(x1, x2)) = 2·x1   
POL(U62(x1)) = x1   
POL(U71(x1, x2)) = x1   
POL(U72(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(a) = 0   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(e) = 1   
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) = 2   
POL(o) = 1   
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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: empty set
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:

__(__(X, Y), Z) → __(X, __(Y, Z))
U61(tt, V) → U62(isQid(V))
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(nil) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = x1   
POL(U12(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2)) = 2·x1   
POL(U23(x1)) = 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = x1   
POL(U42(x1, x2)) = x1   
POL(U43(x1)) = x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2)) = 2·x1   
POL(U53(x1)) = 2·x1   
POL(U61(x1, x2)) = 1 + x1   
POL(U62(x1)) = x1   
POL(U71(x1, x2)) = 2 + x1 + 2·x2   
POL(U72(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 1   
POL(and(x1, x2)) = x1 + 2·x2   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 1   


(6) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isPal(V) → U71(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: empty set
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:

U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1)) = x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2)) = 2·x1   
POL(U23(x1)) = 2·x1   
POL(U31(x1, x2)) = x1   
POL(U32(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2)) = x1   
POL(U43(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = x1   
POL(U52(x1, x2)) = 2·x1   
POL(U53(x1)) = x1   
POL(U62(x1)) = 1 + x1   
POL(U71(x1, x2)) = 2 + x1 + x2   
POL(U72(x1)) = 1 + x1   
POL(__(x1, x2)) = x1 + 2·x2   
POL(a) = 1   
POL(and(x1, x2)) = x1 + 2·x2   
POL(e) = 2   
POL(i) = 1   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(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) = 1   


(8) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isPal(V) → U71(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U71: {1}
and: {1}
isPalListKind: empty set
isPal: empty set
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:

isPal(V) → U71(isPalListKind(V), V)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 2·x1   
POL(U22(x1, x2)) = 2·x1   
POL(U23(x1)) = 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 2·x1   
POL(U42(x1, x2)) = x1   
POL(U43(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = 2·x1   
POL(U52(x1, x2)) = 2·x1   
POL(U53(x1)) = 2·x1   
POL(U71(x1, x2)) = 2·x1 + x2   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 2   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 0   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isPal(x1)) = 2 + 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 1   


(10) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

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

POL(U11(x1, x2)) = 2·x1 + x2   
POL(U12(x1)) = x1   
POL(U21(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U22(x1, x2)) = x1 + 2·x2   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U41(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U42(x1, x2)) = x1 + 2·x2   
POL(U43(x1)) = x1   
POL(U51(x1, x2, x3)) = 2·x1 + x2 + 2·x3   
POL(U52(x1, x2)) = x1 + 2·x2   
POL(U53(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 0   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 2·x1   
POL(isNeList(x1)) = x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → 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)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

U22(tt, V2) → U23(isList(V2))
isList(nil) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1 + x2   
POL(U12(x1)) = x1   
POL(U21(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(U22(x1, x2)) = 2 + x1 + x2   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = 2·x1 + x2   
POL(U32(x1)) = x1   
POL(U42(x1, x2)) = 2·x1 + 2·x2   
POL(U43(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U52(x1, x2)) = 2·x1 + 2·x2   
POL(U53(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 0   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = x1   
POL(isNeList(x1)) = x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = x1   
POL(nil) = 2   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 1   


(14) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

U21(tt, V1, V2) → U22(isList(V1), V2)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = 2·x1   
POL(U12(x1)) = 2·x1   
POL(U21(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U22(x1, x2)) = 1 + x1 + x2   
POL(U23(x1)) = x1   
POL(U31(x1, x2)) = x1   
POL(U32(x1)) = 2·x1   
POL(U42(x1, x2)) = 2·x1   
POL(U43(x1)) = x1   
POL(U51(x1, x2, x3)) = 2·x1 + 2·x3   
POL(U52(x1, x2)) = 2·x1 + 2·x2   
POL(U53(x1)) = x1   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 1   
POL(i) = 0   
POL(isList(x1)) = 2·x1   
POL(isNeList(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 2   


(16) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNeList: empty set
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
Used ordering:
Polynomial interpretation [POLO]:

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


(18) Obligation:

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

U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNeList: empty set
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

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

POL(U11(x1, x2)) = 2·x1 + x2   
POL(U12(x1)) = x1   
POL(U23(x1)) = 2 + 2·x1   
POL(U31(x1, x2)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U51(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U52(x1, x2)) = 2·x1 + x2   
POL(U53(x1)) = x1   
POL(__(x1, x2)) = 1 + x1 + 2·x2   
POL(a) = 1   
POL(and(x1, x2)) = 2·x1 + x2   
POL(e) = 1   
POL(i) = 1   
POL(isList(x1)) = x1   
POL(isNeList(x1)) = 0   
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(isNeList(V))
U12(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNeList: empty set
isList: empty set
U31: {1}
U32: {1}
isQid: empty set
U51: {1}
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

U11(tt, V) → U12(isNeList(V))
U51(tt, V1, V2) → U52(isNeList(V1), V2)
Used ordering:
Polynomial interpretation [POLO]:

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


(22) Obligation:

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

U12(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNeList: empty set
isList: empty set
U31: {1}
U32: {1}
isQid: empty set
U52: {1}
U53: {1}
and: {1}
isPalListKind: empty set
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:

U12(tt) → tt
U52(tt, V2) → U53(isList(V2))
and(tt, X) → X
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(u) → tt
isQid(a) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = x1   
POL(U12(x1)) = 2·x1   
POL(U31(x1, x2)) = 1 + x1   
POL(U32(x1)) = x1   
POL(U52(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U53(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + 2·x2   
POL(a) = 1   
POL(and(x1, x2)) = 2·x1 + 2·x2   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = x1   
POL(isNeList(x1)) = 1 + x1   
POL(isPalListKind(x1)) = x1   
POL(isQid(x1)) = 2   
POL(nil) = 1   
POL(o) = 1   
POL(tt) = 1   
POL(u) = 2   


(24) Obligation:

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

U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U53(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isNeList(V) → U31(isPalListKind(V), V)
isPalListKind(a) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
isNeList: empty set
isList: empty set
U31: {1}
U32: {1}
isQid: empty set
U53: {1}
and: {1}
isPalListKind: empty set
a: empty set
o: empty set

(25) PoloCSRProof (EQUIVALENT transformation)

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

U53(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isNeList(V) → U31(isPalListKind(V), V)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1, x2)) = x1 + x2   
POL(U31(x1, x2)) = x1 + x2   
POL(U32(x1)) = 2·x1   
POL(U53(x1)) = 1 + x1   
POL(__(x1, x2)) = 1 + x1 + 2·x2   
POL(a) = 2   
POL(and(x1, x2)) = x1 + 2·x2   
POL(isList(x1)) = 1 + 2·x1   
POL(isNeList(x1)) = 2 + x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 1   
POL(o) = 2   
POL(tt) = 0   


(26) Obligation:

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

U31(tt, V) → U32(isQid(V))
U32(tt) → tt
isPalListKind(a) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
tt: empty set
U31: {1}
U32: {1}
isQid: empty set
and: {1}
isPalListKind: empty set
a: empty set
o: empty set

(27) PoloCSRProof (EQUIVALENT transformation)

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

U31(tt, V) → U32(isQid(V))
U32(tt) → tt
isPalListKind(a) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))
Used ordering:
Polynomial interpretation [POLO]:

POL(U31(x1, x2)) = 2 + x1 + 2·x2   
POL(U32(x1)) = 2 + 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 2   
POL(and(x1, x2)) = 1 + x1   
POL(isPalListKind(x1)) = 2 + x1   
POL(isQid(x1)) = x1   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 1   


(28) Obligation:

Context-sensitive rewrite system:
R is empty.

(29) RisEmptyProof (EQUIVALENT transformation)

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

(30) TRUE