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

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

POL(U11(x1)) = 2·x1   
POL(U21(x1, x2)) = x1   
POL(U22(x1)) = 2·x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 2·x1   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = x1   
POL(U52(x1)) = 2·x1   
POL(U61(x1)) = x1   
POL(U71(x1, x2)) = 2·x1 + 2·x2   
POL(U72(x1)) = x1   
POL(U81(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(a) = 1   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = x1   
POL(isQid(x1)) = 0   
POL(nil) = 1   
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) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
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
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: 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:

__(__(X, Y), Z) → __(X, __(Y, Z))
U42(tt) → tt
U52(tt) → tt
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = 2·x1 + 2·x2   
POL(U22(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U42(x1)) = 1 + x1   
POL(U51(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U52(x1)) = 1 + x1   
POL(U61(x1)) = 2·x1   
POL(U71(x1, x2)) = 2·x1   
POL(U72(x1)) = x1   
POL(U81(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 2   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 2·x1   
POL(isNeList(x1)) = 2·x1   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 2   
POL(o) = 2   
POL(tt) = 0   
POL(u) = 2   


(8) Obligation:

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

U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U51(tt, V2) → U52(isList(V2))
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isNeList(V) → U31(isQid(V))
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
U11: {1}
tt: empty set
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: 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:

U21(tt, V2) → U22(isList(V2))
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U51(tt, V2) → U52(isList(V2))
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = 2 + 2·x1 + x2   
POL(U22(x1)) = x1   
POL(U31(x1)) = 1 + 2·x1   
POL(U41(x1, x2)) = 2 + x1 + x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = 2 + x1   
POL(U52(x1)) = x1   
POL(U61(x1)) = x1   
POL(U71(x1, x2)) = 2·x1   
POL(U72(x1)) = x1   
POL(U81(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + x2   
POL(a) = 2   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 1   
POL(isNeList(x1)) = 1   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isQid(x1)) = 0   
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) → tt
U22(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isNeList(V) → U31(isQid(V))
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
U11: {1}
tt: empty set
U22: {1}
isList: empty set
U31: {1}
isNeList: empty set
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: 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:

U22(tt) → tt
isList(V) → U11(isNeList(V))
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1)) = x1   
POL(U22(x1)) = 2 + 2·x1   
POL(U31(x1)) = 1 + 2·x1   
POL(U61(x1)) = x1   
POL(U71(x1, x2)) = x1   
POL(U72(x1)) = 2·x1   
POL(U81(x1)) = 2·x1   
POL(__(x1, x2)) = 1 + x1 + 2·x2   
POL(a) = 0   
POL(e) = 2   
POL(i) = 0   
POL(isList(x1)) = 2 + 2·x1   
POL(isNeList(x1)) = 1 + 2·x1   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 0   
POL(isQid(x1)) = 0   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 1   


(12) Obligation:

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

U11(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isNeList(V) → U31(isQid(V))
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
U11: {1}
tt: empty set
U31: {1}
isNeList: empty set
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: 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:

U11(tt) → tt
U72(tt) → tt
U81(tt) → tt
isNeList(V) → U31(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isQid(a) → tt
isQid(e) → tt
isQid(o) → tt
isQid(u) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x1)) = 2 + 2·x1   
POL(U31(x1)) = 1 + x1   
POL(U61(x1)) = x1   
POL(U71(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U72(x1)) = 1 + x1   
POL(U81(x1)) = 1 + x1   
POL(__(x1, x2)) = 1 + x1 + 2·x2   
POL(a) = 2   
POL(e) = 2   
POL(i) = 1   
POL(isNeList(x1)) = 2 + x1   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = 2 + x1   
POL(isQid(x1)) = x1   
POL(o) = 2   
POL(tt) = 1   
POL(u) = 2   


(14) Obligation:

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

U61(tt) → tt
U71(tt, P) → U72(isPal(P))
isNePal(V) → U61(isQid(V))
isQid(i) → tt

The replacement map contains the following entries:

tt: empty set
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
isQid: empty set
isNePal: empty set
i: empty set

(15) PoloCSRProof (EQUIVALENT transformation)

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

U71(tt, P) → U72(isPal(P))
isNePal(V) → U61(isQid(V))
Used ordering:
Polynomial interpretation [POLO]:

POL(U61(x1)) = 2·x1   
POL(U71(x1, x2)) = 2 + x1 + x2   
POL(U72(x1)) = 1 + x1   
POL(i) = 2   
POL(isNePal(x1)) = 1 + 2·x1   
POL(isPal(x1)) = 0   
POL(isQid(x1)) = 0   
POL(tt) = 0   


(16) Obligation:

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

U61(tt) → tt
isQid(i) → tt

The replacement map contains the following entries:

tt: empty set
U61: {1}
isQid: empty set
i: empty set

(17) PoloCSRProof (EQUIVALENT transformation)

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

U61(tt) → tt
isQid(i) → tt
Used ordering:
Polynomial interpretation [POLO]:

POL(U61(x1)) = 2 + 2·x1   
POL(i) = 2   
POL(isQid(x1)) = 2 + 2·x1   
POL(tt) = 1   


(18) Obligation:

Context-sensitive rewrite system:
R is empty.

(19) RisEmptyProof (EQUIVALENT transformation)

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

(20) TRUE