YES Termination proof of ../tpdb/TRS/CSR_Maude/palindrome/PALINDROME_complete.trs
Termination of the following Term Rewriting System could be proven:

Q restricted 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


↳ CSR
  ↳ Zantema-Transformation

Q restricted 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

We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted 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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → A(V)
ISNEPAL(V) → A(V)
ISPALLISTKIND(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
U411(tt, V1, V2) → ISLIST(a(V1))
U111(tt, V) → U121(isNeList(a(V)))
A(aInact) → A
U521(tt, V2) → U531(isList(a(V2)))
ISLIST(__Inact(V1, V2)) → U211(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U211(tt, V1, V2) → ISLIST(a(V1))
ISNEPAL(__Inact(I, __(P, I))) → ISQID(a(I))
ISLIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
A(__Inact(x1, x2)) → __1(x1, x2)
ISNELIST(__Inact(V1, V2)) → A(V2)
A(isPalListKindInact(x1)) → ISPALLISTKIND(x1)
A(eInact) → E
U211(tt, V1, V2) → U221(isList(a(V1)), a(V2))
AND(tt, X) → A(X)
ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISLIST(V) → ISPALLISTKIND(a(V))
U311(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → A(V2)
U511(tt, V1, V2) → A(V2)
U511(tt, V1, V2) → ISNELIST(a(V1))
U411(tt, V1, V2) → U421(isList(a(V1)), a(V2))
U311(tt, V) → U321(isQid(a(V)))
U711(tt, V) → U721(isNePal(a(V)))
U711(tt, V) → ISNEPAL(a(V))
ISNEPAL(V) → U611(isPalListKind(a(V)), a(V))
U521(tt, V2) → ISLIST(a(V2))
U411(tt, V1, V2) → A(V1)
ISNELIST(V) → U311(isPalListKind(a(V)), a(V))
U221(tt, V2) → U231(isList(a(V2)))
U311(tt, V) → ISQID(a(V))
U111(tt, V) → ISNELIST(a(V))
U611(tt, V) → U621(isQid(a(V)))
ISPAL(V) → ISPALLISTKIND(a(V))
U421(tt, V2) → A(V2)
ISPAL(V) → U711(isPalListKind(a(V)), a(V))
U521(tt, V2) → A(V2)
ISLIST(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
A(iInact) → I
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISNEPAL(V) → ISPALLISTKIND(a(V))
U611(tt, V) → A(V)
A(nilInact) → NIL
U211(tt, V1, V2) → A(V1)
A(oInact) → O
ISNEPAL(__Inact(I, __(P, I))) → A(I)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
U221(tt, V2) → ISLIST(a(V2))
__1(__(X, Y), Z) → __1(Y, Z)
U511(tt, V1, V2) → U521(isNeList(a(V1)), a(V2))
ISNELIST(__Inact(V1, V2)) → U511(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
ISLIST(__Inact(V1, V2)) → A(V1)
ISLIST(V) → A(V)
ISNEPAL(__Inact(I, __(P, I))) → A(P)
ISNELIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U421(tt, V2) → U431(isNeList(a(V2)))
ISNELIST(__Inact(V1, V2)) → U411(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
U111(tt, V) → A(V)
ISNEPAL(__Inact(I, __(P, I))) → ISPAL(a(P))
ISNEPAL(__Inact(I, __(P, I))) → AND(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
U221(tt, V2) → A(V2)
ISNEPAL(__Inact(I, __(P, I))) → AND(isQid(a(I)), isPalListKindInact(a(I)))
ISNELIST(V) → ISPALLISTKIND(a(V))
A(uInact) → U
U421(tt, V2) → ISNELIST(a(V2))
U611(tt, V) → ISQID(a(V))
ISNELIST(__Inact(V1, V2)) → A(V1)
U711(tt, V) → A(V)
U511(tt, V1, V2) → A(V1)
U211(tt, V1, V2) → A(V2)
ISNELIST(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
U411(tt, V1, V2) → A(V2)
ISNELIST(V) → A(V)

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → A(V)
ISNEPAL(V) → A(V)
ISPALLISTKIND(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
U411(tt, V1, V2) → ISLIST(a(V1))
U111(tt, V) → U121(isNeList(a(V)))
A(aInact) → A
U521(tt, V2) → U531(isList(a(V2)))
ISLIST(__Inact(V1, V2)) → U211(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
U211(tt, V1, V2) → ISLIST(a(V1))
ISNEPAL(__Inact(I, __(P, I))) → ISQID(a(I))
ISLIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
A(__Inact(x1, x2)) → __1(x1, x2)
ISNELIST(__Inact(V1, V2)) → A(V2)
A(isPalListKindInact(x1)) → ISPALLISTKIND(x1)
A(eInact) → E
U211(tt, V1, V2) → U221(isList(a(V1)), a(V2))
AND(tt, X) → A(X)
ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISLIST(V) → ISPALLISTKIND(a(V))
U311(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → A(V2)
U511(tt, V1, V2) → A(V2)
U511(tt, V1, V2) → ISNELIST(a(V1))
U411(tt, V1, V2) → U421(isList(a(V1)), a(V2))
U311(tt, V) → U321(isQid(a(V)))
U711(tt, V) → U721(isNePal(a(V)))
U711(tt, V) → ISNEPAL(a(V))
ISNEPAL(V) → U611(isPalListKind(a(V)), a(V))
U521(tt, V2) → ISLIST(a(V2))
U411(tt, V1, V2) → A(V1)
ISNELIST(V) → U311(isPalListKind(a(V)), a(V))
U221(tt, V2) → U231(isList(a(V2)))
U311(tt, V) → ISQID(a(V))
U111(tt, V) → ISNELIST(a(V))
U611(tt, V) → U621(isQid(a(V)))
ISPAL(V) → ISPALLISTKIND(a(V))
U421(tt, V2) → A(V2)
ISPAL(V) → U711(isPalListKind(a(V)), a(V))
U521(tt, V2) → A(V2)
ISLIST(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
A(iInact) → I
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISNEPAL(V) → ISPALLISTKIND(a(V))
U611(tt, V) → A(V)
A(nilInact) → NIL
U211(tt, V1, V2) → A(V1)
A(oInact) → O
ISNEPAL(__Inact(I, __(P, I))) → A(I)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
U221(tt, V2) → ISLIST(a(V2))
__1(__(X, Y), Z) → __1(Y, Z)
U511(tt, V1, V2) → U521(isNeList(a(V1)), a(V2))
ISNELIST(__Inact(V1, V2)) → U511(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
ISLIST(__Inact(V1, V2)) → A(V1)
ISLIST(V) → A(V)
ISNEPAL(__Inact(I, __(P, I))) → A(P)
ISNELIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U421(tt, V2) → U431(isNeList(a(V2)))
ISNELIST(__Inact(V1, V2)) → U411(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
U111(tt, V) → A(V)
ISNEPAL(__Inact(I, __(P, I))) → ISPAL(a(P))
ISNEPAL(__Inact(I, __(P, I))) → AND(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
U221(tt, V2) → A(V2)
ISNEPAL(__Inact(I, __(P, I))) → AND(isQid(a(I)), isPalListKindInact(a(I)))
ISNELIST(V) → ISPALLISTKIND(a(V))
A(uInact) → U
U421(tt, V2) → ISNELIST(a(V2))
U611(tt, V) → ISQID(a(V))
ISNELIST(__Inact(V1, V2)) → A(V1)
U711(tt, V) → A(V)
U511(tt, V1, V2) → A(V1)
U211(tt, V1, V2) → A(V2)
ISNELIST(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
U411(tt, V1, V2) → A(V2)
ISNELIST(V) → A(V)

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 52 less nodes.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(x1, x2) → __Inact(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
A(andInact(x1, x2)) → AND(x1, x2)
ISPALLISTKIND(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
A(isPalListKindInact(x1)) → ISPALLISTKIND(x1)
AND(tt, X) → A(X)

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISPALLISTKIND(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
A(isPalListKindInact(x1)) → ISPALLISTKIND(x1)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
a(isPalListKindInact(x1)) → isPalListKind(x1)
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
a(andInact(x1, x2)) → and(x1, x2)
and(tt, X) → a(X)
a(uInact) → u
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(x1) → isPalListKindInact(x1)
u → uInact
and(x1, x2) → andInact(x1, x2)
e → eInact
o → oInact
nil → nilInact
i → iInact
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(x1, x2) → __Inact(x1, x2)
a → aInact

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
A(andInact(x1, x2)) → AND(x1, x2)
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISPALLISTKIND(__Inact(V1, V2)) → AND(isPalListKind(a(V1)), isPalListKindInact(a(V2)))

Strictly oriented rules of the TRS R:

isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
and(tt, X) → a(X)
isPalListKind(eInact) → tt
__(X, nil) → X
__(nil, X) → X

Used ordering: POLO with Polynomial interpretation [25]:

POL(A(x1)) = 2·x1   
POL(AND(x1, x2)) = x1 + 2·x2   
POL(ISPALLISTKIND(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + x2   
POL(__Inact(x1, x2)) = 2 + x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(and(x1, x2)) = 1 + x1 + x2   
POL(andInact(x1, x2)) = 1 + x1 + x2   
POL(e) = 1   
POL(eInact) = 1   
POL(i) = 0   
POL(iInact) = 0   
POL(isPalListKind(x1)) = x1   
POL(isPalListKindInact(x1)) = x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A(isPalListKindInact(x1)) → ISPALLISTKIND(x1)
AND(tt, X) → A(X)

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
a(isPalListKindInact(x1)) → isPalListKind(x1)
a(andInact(x1, x2)) → and(x1, x2)
a(uInact) → u
isPalListKind(aInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(x1) → isPalListKindInact(x1)
u → uInact
and(x1, x2) → andInact(x1, x2)
e → eInact
o → oInact
nil → nilInact
i → iInact
__(__(X, Y), Z) → __(X, __(Y, Z))
__(x1, x2) → __Inact(x1, x2)
a → aInact

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesReductionPairsProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → U711(isPalListKind(a(V)), a(V))
U711(tt, V) → ISNEPAL(a(V))
ISNEPAL(__Inact(I, __(P, I))) → ISPAL(a(P))

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

isPalListKind(oInact) → tt
Used ordering: POLO with Polynomial interpretation [25]:

POL(ISNEPAL(x1)) = x1   
POL(ISPAL(x1)) = 2·x1   
POL(U711(x1, x2)) = x1 + x2   
POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(andInact(x1, x2)) = x1 + x2   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isPalListKind(x1)) = x1   
POL(isPalListKindInact(x1)) = x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 1   
POL(oInact) = 1   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesReductionPairsProof
                  ↳ QDP
                    ↳ RuleRemovalProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → U711(isPalListKind(a(V)), a(V))
U711(tt, V) → ISNEPAL(a(V))
ISNEPAL(__Inact(I, __(P, I))) → ISPAL(a(P))

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
a(isPalListKindInact(x1)) → isPalListKind(x1)
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
a(andInact(x1, x2)) → and(x1, x2)
and(tt, X) → a(X)
a(uInact) → u
u → uInact
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(uInact) → tt
isPalListKind(x1) → isPalListKindInact(x1)
and(x1, x2) → andInact(x1, x2)
e → eInact
o → oInact
nil → nilInact
i → iInact
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(x1, x2) → __Inact(x1, x2)
a → aInact

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISPAL(V) → U711(isPalListKind(a(V)), a(V))

Strictly oriented rules of the TRS R:

and(tt, X) → a(X)
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(uInact) → tt
__(X, nil) → X
__(nil, X) → X

Used ordering: POLO with Polynomial interpretation [25]:

POL(ISNEPAL(x1)) = 1 + x1   
POL(ISPAL(x1)) = 1 + 2·x1   
POL(U711(x1, x2)) = x1 + x2   
POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·x1 + x2   
POL(a) = 1   
POL(a(x1)) = x1   
POL(aInact) = 1   
POL(and(x1, x2)) = x1 + x2   
POL(andInact(x1, x2)) = x1 + x2   
POL(e) = 2   
POL(eInact) = 2   
POL(i) = 2   
POL(iInact) = 2   
POL(isPalListKind(x1)) = x1   
POL(isPalListKindInact(x1)) = x1   
POL(nil) = 1   
POL(nilInact) = 1   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 1   
POL(u) = 2   
POL(uInact) = 2   



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesReductionPairsProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U711(tt, V) → ISNEPAL(a(V))
ISNEPAL(__Inact(I, __(P, I))) → ISPAL(a(P))

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
a(isPalListKindInact(x1)) → isPalListKind(x1)
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
a(andInact(x1, x2)) → and(x1, x2)
a(uInact) → u
u → uInact
isPalListKind(aInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(x1) → isPalListKindInact(x1)
and(x1, x2) → andInact(x1, x2)
e → eInact
o → oInact
nil → nilInact
i → iInact
__(__(X, Y), Z) → __(X, __(Y, Z))
__(x1, x2) → __Inact(x1, x2)
a → aInact

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U221(tt, V2) → ISLIST(a(V2))
U511(tt, V1, V2) → U521(isNeList(a(V1)), a(V2))
U411(tt, V1, V2) → U421(isList(a(V1)), a(V2))
U511(tt, V1, V2) → ISNELIST(a(V1))
ISNELIST(__Inact(V1, V2)) → U511(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
U411(tt, V1, V2) → ISLIST(a(V1))
U421(tt, V2) → ISNELIST(a(V2))
U521(tt, V2) → ISLIST(a(V2))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U111(tt, V) → ISNELIST(a(V))
ISLIST(__Inact(V1, V2)) → U211(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
U211(tt, V1, V2) → ISLIST(a(V1))
ISNELIST(__Inact(V1, V2)) → U411(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
U211(tt, V1, V2) → U221(isList(a(V1)), a(V2))

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ISNELIST(__Inact(V1, V2)) → U511(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISLIST(__Inact(V1, V2)) → U211(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
ISNELIST(__Inact(V1, V2)) → U411(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
The remaining pairs can at least be oriented weakly.

U221(tt, V2) → ISLIST(a(V2))
U511(tt, V1, V2) → U521(isNeList(a(V1)), a(V2))
U411(tt, V1, V2) → U421(isList(a(V1)), a(V2))
U511(tt, V1, V2) → ISNELIST(a(V1))
U411(tt, V1, V2) → ISLIST(a(V1))
U421(tt, V2) → ISNELIST(a(V2))
U521(tt, V2) → ISLIST(a(V2))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U111(tt, V) → ISNELIST(a(V))
U211(tt, V1, V2) → ISLIST(a(V1))
U211(tt, V1, V2) → U221(isList(a(V1)), a(V2))
Used ordering: Polynomial interpretation [25]:

POL(ISLIST(x1)) = 1 + x1   
POL(ISNELIST(x1)) = 1 + x1   
POL(U11(x1, x2)) = 0   
POL(U111(x1, x2)) = 1 + x2   
POL(U12(x1)) = 0   
POL(U21(x1, x2, x3)) = 0   
POL(U211(x1, x2, x3)) = 1 + x2 + x3   
POL(U22(x1, x2)) = 0   
POL(U221(x1, x2)) = 1 + x2   
POL(U23(x1)) = 0   
POL(U31(x1, x2)) = 0   
POL(U32(x1)) = 0   
POL(U41(x1, x2, x3)) = 0   
POL(U411(x1, x2, x3)) = 1 + x2 + x3   
POL(U42(x1, x2)) = 0   
POL(U421(x1, x2)) = 1 + x2   
POL(U43(x1)) = 0   
POL(U51(x1, x2, x3)) = 0   
POL(U511(x1, x2, x3)) = 1 + x2 + x3   
POL(U52(x1, x2)) = 0   
POL(U521(x1, x2)) = 1 + x2   
POL(U53(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(__Inact(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(and(x1, x2)) = x2   
POL(andInact(x1, x2)) = x2   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isPalListKindInact(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 1   
POL(oInact) = 1   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   

The following usable rules [17] were oriented:

a → aInact
o → oInact
a(eInact) → e
a(x) → x
__(__(X, Y), Z) → __(X, __(Y, Z))
a(isPalListKindInact(x1)) → isPalListKind(x1)
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
a(andInact(x1, x2)) → and(x1, x2)
and(tt, X) → a(X)
i → iInact
isPalListKind(oInact) → tt
a(aInact) → a
a(uInact) → u
__(x1, x2) → __Inact(x1, x2)
e → eInact
isPalListKind(uInact) → tt
isPalListKind(aInact) → tt
a(oInact) → o
isPalListKind(nilInact) → tt
a(__Inact(x1, x2)) → __(x1, x2)
and(x1, x2) → andInact(x1, x2)
__(X, nil) → X
isPalListKind(iInact) → tt
nil → nilInact
isPalListKind(eInact) → tt
a(iInact) → i
u → uInact
__(nil, X) → X
a(nilInact) → nil
isPalListKind(x1) → isPalListKindInact(x1)



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U111(tt, V) → ISNELIST(a(V))
U221(tt, V2) → ISLIST(a(V2))
U511(tt, V1, V2) → U521(isNeList(a(V1)), a(V2))
U211(tt, V1, V2) → ISLIST(a(V1))
U511(tt, V1, V2) → ISNELIST(a(V1))
U411(tt, V1, V2) → U421(isList(a(V1)), a(V2))
U411(tt, V1, V2) → ISLIST(a(V1))
U521(tt, V2) → ISLIST(a(V2))
U421(tt, V2) → ISNELIST(a(V2))
U211(tt, V1, V2) → U221(isList(a(V1)), a(V2))

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(a(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(a(V1)), a(V2))
U22(tt, V2) → U23(isList(a(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(a(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(a(V1)), a(V2))
U42(tt, V2) → U43(isNeList(a(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(a(V1)), a(V2))
U52(tt, V2) → U53(isList(a(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(a(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(a(V)))
U72(tt) → tt
and(tt, X) → a(X)
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(and(isPalListKind(a(V1)), isPalListKindInact(a(V2))), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → and(and(isQid(a(I)), isPalListKindInact(a(I))), andInact(isPal(a(P)), isPalListKindInact(a(P))))
isPal(V) → U71(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → and(isPalListKind(a(V1)), isPalListKindInact(a(V2)))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
isPalListKind(x1) → isPalListKindInact(x1)
a(isPalListKindInact(x1)) → isPalListKind(x1)
u → uInact
a(uInact) → u
and(x1, x2) → andInact(x1, x2)
a(andInact(x1, x2)) → and(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 11 less nodes.