YES Termination Proof using AProVETerm Rewriting System R:
[X, Y, Z, V, V1, V2, I, P]
((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

Termination of R to be shown. 



   TRS
     ↳CSR to TRS Transformation




Zantema-Transformation successful.
Replacement map:
U71(1, 2)
and(1, 2)
U42(1, 2)
isPalListKind(1)
U52(1, 2)
U11(1, 2)
U51(1, 2, 3)
U62(1)
U21(1, 2, 3)
U43(1)
U72(1)
isNePal(1)
isNeList(1)
U53(1)
U31(1, 2)
U12(1)
U23(1)
(1, 2)
U22(1, 2)
isPal(1)
U41(1, 2, 3)
U32(1)
U61(1, 2)
isList(1)
isQid(1)

Old CSR:

((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

new TRS:

((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u



   TRS
     ↳CSRtoTRS
       →TRS1
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

'((X, Y), Z) -> '(X, (Y, Z))
'((X, Y), Z) -> '(Y, Z)
U11'(tt, V) -> U12'(isNeList(a(V)))
U11'(tt, V) -> ISNELIST(a(V))
U11'(tt, V) -> A(V)
ISNELIST(V) -> U31'(isPalListKind(a(V)), a(V))
ISNELIST(V) -> ISPALLISTKIND(a(V))
ISNELIST(V) -> A(V)
ISNELIST((V1, V2)) -> U41'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
ISNELIST((V1, V2)) -> AND(isPalListKind(a(V1)), isPalListKind(a(V2)))
ISNELIST((V1, V2)) -> ISPALLISTKIND(a(V1))
ISNELIST((V1, V2)) -> A(V1)
ISNELIST((V1, V2)) -> A(V2)
ISNELIST((V1, V2)) -> U51'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
A(and(x0, x1)) -> AND(x0, x1)
A(i) -> I
A(e) -> E
A((x0, x1)) -> '(x0, x1)
A(o) -> O
A(isPalListKind(x0)) -> ISPALLISTKIND(x0)
A(nil) -> NIL
A(a) -> A
A(u) -> U
U21'(tt, V1, V2) -> U22'(isList(a(V1)), a(V2))
U21'(tt, V1, V2) -> ISLIST(a(V1))
U21'(tt, V1, V2) -> A(V1)
U21'(tt, V1, V2) -> A(V2)
U22'(tt, V2) -> U23'(isList(a(V2)))
U22'(tt, V2) -> ISLIST(a(V2))
U22'(tt, V2) -> A(V2)
ISLIST(V) -> U11'(isPalListKind(a(V)), a(V))
ISLIST(V) -> ISPALLISTKIND(a(V))
ISLIST(V) -> A(V)
ISLIST((V1, V2)) -> U21'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
ISLIST((V1, V2)) -> AND(isPalListKind(a(V1)), isPalListKind(a(V2)))
ISLIST((V1, V2)) -> ISPALLISTKIND(a(V1))
ISLIST((V1, V2)) -> A(V1)
ISLIST((V1, V2)) -> A(V2)
U31'(tt, V) -> U32'(isQid(a(V)))
U31'(tt, V) -> ISQID(a(V))
U31'(tt, V) -> A(V)
U41'(tt, V1, V2) -> U42'(isList(a(V1)), a(V2))
U41'(tt, V1, V2) -> ISLIST(a(V1))
U41'(tt, V1, V2) -> A(V1)
U41'(tt, V1, V2) -> A(V2)
U42'(tt, V2) -> U43'(isNeList(a(V2)))
U42'(tt, V2) -> ISNELIST(a(V2))
U42'(tt, V2) -> A(V2)
U51'(tt, V1, V2) -> U52'(isNeList(a(V1)), a(V2))
U51'(tt, V1, V2) -> ISNELIST(a(V1))
U51'(tt, V1, V2) -> A(V1)
U51'(tt, V1, V2) -> A(V2)
U52'(tt, V2) -> U53'(isList(a(V2)))
U52'(tt, V2) -> ISLIST(a(V2))
U52'(tt, V2) -> A(V2)
U61'(tt, V) -> U62'(isQid(a(V)))
U61'(tt, V) -> ISQID(a(V))
U61'(tt, V) -> A(V)
U71'(tt, V) -> U72'(isNePal(a(V)))
U71'(tt, V) -> ISNEPAL(a(V))
U71'(tt, V) -> A(V)
ISNEPAL(V) -> U61'(isPalListKind(a(V)), a(V))
ISNEPAL(V) -> ISPALLISTKIND(a(V))
ISNEPAL(V) -> A(V)
ISNEPAL((I, (P, I))) -> AND(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
ISNEPAL((I, (P, I))) -> AND(isQid(a(I)), isPalListKind(a(I)))
ISNEPAL((I, (P, I))) -> ISQID(a(I))
ISNEPAL((I, (P, I))) -> A(I)
ISNEPAL((I, (P, I))) -> ISPAL(a(P))
ISNEPAL((I, (P, I))) -> A(P)
AND(tt, X) -> A(X)
ISPALLISTKIND((V1, V2)) -> AND(isPalListKind(a(V1)), isPalListKind(a(V2)))
ISPALLISTKIND((V1, V2)) -> ISPALLISTKIND(a(V1))
ISPALLISTKIND((V1, V2)) -> A(V1)
ISPALLISTKIND((V1, V2)) -> A(V2)
ISPAL(V) -> U71'(isPalListKind(a(V)), a(V))
ISPAL(V) -> ISPALLISTKIND(a(V))
ISPAL(V) -> A(V)

Furthermore, R contains four SCCs. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳Size-Change Principle
           →DP Problem 2
             ↳Neg POLO
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

'((X, Y), Z) -> '(Y, Z)
'((X, Y), Z) -> '(X, (Y, Z))


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





We number the DPs as follows:
  1. '((X, Y), Z) -> '(Y, Z)
  2. '((X, Y), Z) -> '(X, (Y, Z))
and get the following Size-Change Graph(s):
{2, 1} , {2, 1}
1>1
2=2
{2, 1} , {2, 1}
1>1

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {2, 1}
1>1
{2, 1} , {2, 1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial


We obtain no new DP problems. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Negative Polynomial Order
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

ISPALLISTKIND((V1, V2)) -> A(V2)
ISPALLISTKIND((V1, V2)) -> A(V1)
ISPALLISTKIND((V1, V2)) -> ISPALLISTKIND(a(V1))
ISPALLISTKIND((V1, V2)) -> AND(isPalListKind(a(V1)), isPalListKind(a(V2)))
A(isPalListKind(x0)) -> ISPALLISTKIND(x0)
AND(tt, X) -> A(X)
A(and(x0, x1)) -> AND(x0, x1)


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





The following Dependency Pairs can be strictly oriented using the given order.

ISPALLISTKIND((V1, V2)) -> A(V2)
ISPALLISTKIND((V1, V2)) -> A(V1)
ISPALLISTKIND((V1, V2)) -> ISPALLISTKIND(a(V1))
ISPALLISTKIND((V1, V2)) -> AND(isPalListKind(a(V1)), isPalListKind(a(V2)))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
i -> i
e -> e
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
o -> o
nil -> nil
a -> a
u -> u


Used ordering:
Polynomial Order with Interpretation:

POL( ISPALLISTKIND(x1) ) = x1


POL( (x1, x2) ) = x1 + x2 + 1


POL( A(x1) ) = x1


POL( a(x1) ) = x1


POL( isPalListKind(x1) ) = x1


POL( AND(x1, x2) ) = x2


POL( and(x1, x2) ) = x2


POL( and(x1, x2) ) = x2


POL( i ) = 0


POL( i ) = 0


POL( e ) = 0


POL( e ) = 0


POL( (x1, x2) ) = x1 + x2 + 1


POL( o ) = 0


POL( o ) = 0


POL( isPalListKind(x1) ) = x1


POL( nil ) = 0


POL( nil ) = 0


POL( a ) = 0


POL( a ) = 0


POL( u ) = 0


POL( u ) = 0


POL( tt ) = 0



This results in one new DP problem. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
             ...
               →DP Problem 5
                 ↳Dependency Graph
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

A(isPalListKind(x0)) -> ISPALLISTKIND(x0)
AND(tt, X) -> A(X)
A(and(x0, x1)) -> AND(x0, x1)


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





Using the Dependency Graph the DP problem was split into 1 DP problems.


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
             ...
               →DP Problem 6
                 ↳Size-Change Principle
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

A(and(x0, x1)) -> AND(x0, x1)
AND(tt, X) -> A(X)


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





We number the DPs as follows:
  1. A(and(x0, x1)) -> AND(x0, x1)
  2. AND(tt, X) -> A(X)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
1>2
{2} , {2}
2=1

which lead(s) to this/these maximal multigraph(s):
{1} , {2}
1>1
{2} , {1}
2>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
and(x1, x2) -> and(x1, x2)

We obtain no new DP problems. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
           →DP Problem 3
             ↳Negative Polynomial Order
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

U41'(tt, V1, V2) -> ISLIST(a(V1))
U51'(tt, V1, V2) -> ISNELIST(a(V1))
U21'(tt, V1, V2) -> ISLIST(a(V1))
U22'(tt, V2) -> ISLIST(a(V2))
U21'(tt, V1, V2) -> U22'(isList(a(V1)), a(V2))
ISLIST((V1, V2)) -> U21'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
ISLIST(V) -> U11'(isPalListKind(a(V)), a(V))
U52'(tt, V2) -> ISLIST(a(V2))
U51'(tt, V1, V2) -> U52'(isNeList(a(V1)), a(V2))
ISNELIST((V1, V2)) -> U51'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U42'(tt, V2) -> ISNELIST(a(V2))
U41'(tt, V1, V2) -> U42'(isList(a(V1)), a(V2))
ISNELIST((V1, V2)) -> U41'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U11'(tt, V) -> ISNELIST(a(V))


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





The following Dependency Pairs can be strictly oriented using the given order.

U41'(tt, V1, V2) -> ISLIST(a(V1))
ISLIST((V1, V2)) -> U21'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
ISNELIST((V1, V2)) -> U51'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U41'(tt, V1, V2) -> U42'(isList(a(V1)), a(V2))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
i -> i
e -> e
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
o -> o
nil -> nil
a -> a
u -> u
U11(tt, V) -> U12(isNeList(a(V)))
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U31(tt, V) -> U32(isQid(a(V)))
U41(tt, V1, V2) -> U42(isList(a(V1)), a(V2))
U51(tt, V1, V2) -> U52(isNeList(a(V1)), a(V2))
U12(tt) -> tt
U22(tt, V2) -> U23(isList(a(V2)))
U32(tt) -> tt
U42(tt, V2) -> U43(isNeList(a(V2)))
U52(tt, V2) -> U53(isList(a(V2)))
U23(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
U43(tt) -> tt
U53(tt) -> tt


Used ordering:
Polynomial Order with Interpretation:

POL( U41'(x1, ..., x3) ) = x2 + x3 + 1


POL( ISLIST(x1) ) = x1


POL( a(x1) ) = x1


POL( U21'(x1, ..., x3) ) = x2 + x3


POL( U11'(x1, x2) ) = x2


POL( ISNELIST(x1) ) = x1


POL( U51'(x1, ..., x3) ) = x2 + x3


POL( U52'(x1, x2) ) = x2


POL( U42'(x1, x2) ) = x2


POL( (x1, x2) ) = x1 + x2 + 1


POL( U22'(x1, x2) ) = x2


POL( and(x1, x2) ) = x2


POL( and(x1, x2) ) = x2


POL( i ) = 0


POL( i ) = 0


POL( e ) = 0


POL( e ) = 0


POL( (x1, x2) ) = x1 + x2 + 1


POL( o ) = 0


POL( o ) = 0


POL( isPalListKind(x1) ) = 0


POL( isPalListKind(x1) ) = 0


POL( nil ) = 0


POL( nil ) = 0


POL( a ) = 0


POL( a ) = 0


POL( u ) = 0


POL( u ) = 0


POL( isList(x1) ) = 0


POL( U11(x1, x2) ) = 0


POL( tt ) = 0


POL( U21(x1, ..., x3) ) = 0


POL( isNeList(x1) ) = 0


POL( U31(x1, x2) ) = 0


POL( U41(x1, ..., x3) ) = 0


POL( U51(x1, ..., x3) ) = 0


POL( U12(x1) ) = 0


POL( U22(x1, x2) ) = 0


POL( U32(x1) ) = 0


POL( U42(x1, x2) ) = 0


POL( U52(x1, x2) ) = 0


POL( U23(x1) ) = 0


POL( U43(x1) ) = 0


POL( U53(x1) ) = 0



This results in one new DP problem. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
           →DP Problem 3
             ↳Neg POLO
             ...
               →DP Problem 7
                 ↳Dependency Graph
           →DP Problem 4
             ↳Neg POLO


Dependency Pairs:

U51'(tt, V1, V2) -> ISNELIST(a(V1))
U21'(tt, V1, V2) -> ISLIST(a(V1))
U22'(tt, V2) -> ISLIST(a(V2))
U21'(tt, V1, V2) -> U22'(isList(a(V1)), a(V2))
ISLIST(V) -> U11'(isPalListKind(a(V)), a(V))
U52'(tt, V2) -> ISLIST(a(V2))
U51'(tt, V1, V2) -> U52'(isNeList(a(V1)), a(V2))
U42'(tt, V2) -> ISNELIST(a(V2))
ISNELIST((V1, V2)) -> U41'(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U11'(tt, V) -> ISNELIST(a(V))


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





Using the Dependency Graph resulted in no new DP problems.


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Negative Polynomial Order


Dependency Pairs:

ISPAL(V) -> U71'(isPalListKind(a(V)), a(V))
ISNEPAL((I, (P, I))) -> ISPAL(a(P))
U71'(tt, V) -> ISNEPAL(a(V))


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





The following Dependency Pairs can be strictly oriented using the given order.

ISPAL(V) -> U71'(isPalListKind(a(V)), a(V))
ISNEPAL((I, (P, I))) -> ISPAL(a(P))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
i -> i
e -> e
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
o -> o
nil -> nil
a -> a
u -> u


Used ordering:
Polynomial Order with Interpretation:

POL( ISPAL(x1) ) = x1 + 1


POL( U71'(x1, x2) ) = x2


POL( a(x1) ) = x1


POL( ISNEPAL(x1) ) = x1


POL( (x1, x2) ) = x1 + x2 + 1


POL( (x1, x2) ) = x1 + x2 + 1


POL( isPalListKind(x1) ) = 0


POL( tt ) = 0


POL( and(x1, x2) ) = x2


POL( isPalListKind(x1) ) = 0


POL( and(x1, x2) ) = x2


POL( i ) = 0


POL( i ) = 0


POL( e ) = 0


POL( e ) = 0


POL( o ) = 0


POL( o ) = 0


POL( nil ) = 0


POL( nil ) = 0


POL( a ) = 0


POL( a ) = 0


POL( u ) = 0


POL( u ) = 0



This results in one new DP problem. 


   TRS
     ↳CSRtoTRS
       →TRS1
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Neg POLO
           →DP Problem 3
             ↳Neg POLO
           →DP Problem 4
             ↳Neg POLO
             ...
               →DP Problem 8
                 ↳Dependency Graph


Dependency Pair:

U71'(tt, V) -> ISNEPAL(a(V))


Rules:


((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt, V) -> U12(isNeList(a(V)))
U12(tt) -> tt
isNeList(V) -> U31(isPalListKind(a(V)), a(V))
isNeList((V1, V2)) -> U41(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
isNeList((V1, V2)) -> U51(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
a(and(x0, x1)) -> and(x0, x1)
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(isPalListKind(x0)) -> isPalListKind(x0)
a(nil) -> nil
a(a) -> a
a(u) -> u
U21(tt, V1, V2) -> U22(isList(a(V1)), a(V2))
U22(tt, V2) -> U23(isList(a(V2)))
isList(V) -> U11(isPalListKind(a(V)), a(V))
isList(nil) -> tt
isList((V1, V2)) -> U21(and(isPalListKind(a(V1)), isPalListKind(a(V2))), a(V1), a(V2))
U23(tt) -> tt
U31(tt, V) -> U32(isQid(a(V)))
U32(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> 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
isNePal(V) -> U61(isPalListKind(a(V)), a(V))
isNePal((I, (P, I))) -> and(and(isQid(a(I)), isPalListKind(a(I))), and(isPal(a(P)), isPalListKind(a(P))))
and(tt, X) -> a(X)
and(x0, x1) -> and(x0, x1)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind((V1, V2)) -> and(isPalListKind(a(V1)), isPalListKind(a(V2)))
isPalListKind(x0) -> isPalListKind(x0)
isPal(V) -> U71(isPalListKind(a(V)), a(V))
isPal(nil) -> tt
i -> i
e -> e
o -> o
a -> a
u -> u





Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
1:15 minutes