YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  U11(tt(),V) -> U12(isNeList(activate(V)))
  U12(tt()) -> tt()
  U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
  U22(tt(),V2) -> U23(isList(activate(V2)))
  U23(tt()) -> tt()
  U31(tt(),V) -> U32(isQid(activate(V)))
  U32(tt()) -> tt()
  U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
  U42(tt(),V2) -> U43(isNeList(activate(V2)))
  U43(tt()) -> tt()
  U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
  U52(tt(),V2) -> U53(isList(activate(V2)))
  U53(tt()) -> tt()
  U61(tt(),V) -> U62(isQid(activate(V)))
  U62(tt()) -> tt()
  U71(tt(),V) -> U72(isNePal(activate(V)))
  U72(tt()) -> tt()
  and(tt(),X) -> activate(X)
  isList(V) -> U11(isPalListKind(activate(V)),activate(V))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
  isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
  isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
  isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
  isPal(n__nil()) -> tt()
  isPalListKind(n__a()) -> tt()
  isPalListKind(n__e()) -> tt()
  isPalListKind(n__i()) -> tt()
  isPalListKind(n__nil()) -> tt()
  isPalListKind(n__o()) -> tt()
  isPalListKind(n__u()) -> tt()
  isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
  isQid(n__a()) -> tt()
  isQid(n__e()) -> tt()
  isQid(n__i()) -> tt()
  isQid(n__o()) -> tt()
  isQid(n__u()) -> tt()
  nil() -> n__nil()
  __(X1,X2) -> n____(X1,X2)
  isPalListKind(X) -> n__isPalListKind(X)
  and(X1,X2) -> n__and(X1,X2)
  a() -> n__a()
  e() -> n__e()
  i() -> n__i()
  o() -> n__o()
  u() -> n__u()
  activate(n__nil()) -> nil()
  activate(n____(X1,X2)) -> __(X1,X2)
  activate(n__isPalListKind(X)) -> isPalListKind(X)
  activate(n__and(X1,X2)) -> and(X1,X2)
  activate(n__a()) -> a()
  activate(n__e()) -> e()
  activate(n__i()) -> i()
  activate(n__o()) -> o()
  activate(n__u()) -> u()
  activate(X) -> X

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)
p3: U11#(tt(),V) -> U12#(isNeList(activate(V)))
p4: U11#(tt(),V) -> isNeList#(activate(V))
p5: U11#(tt(),V) -> activate#(V)
p6: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p7: U21#(tt(),V1,V2) -> isList#(activate(V1))
p8: U21#(tt(),V1,V2) -> activate#(V1)
p9: U21#(tt(),V1,V2) -> activate#(V2)
p10: U22#(tt(),V2) -> U23#(isList(activate(V2)))
p11: U22#(tt(),V2) -> isList#(activate(V2))
p12: U22#(tt(),V2) -> activate#(V2)
p13: U31#(tt(),V) -> U32#(isQid(activate(V)))
p14: U31#(tt(),V) -> isQid#(activate(V))
p15: U31#(tt(),V) -> activate#(V)
p16: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p17: U41#(tt(),V1,V2) -> isList#(activate(V1))
p18: U41#(tt(),V1,V2) -> activate#(V1)
p19: U41#(tt(),V1,V2) -> activate#(V2)
p20: U42#(tt(),V2) -> U43#(isNeList(activate(V2)))
p21: U42#(tt(),V2) -> isNeList#(activate(V2))
p22: U42#(tt(),V2) -> activate#(V2)
p23: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p24: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p25: U51#(tt(),V1,V2) -> activate#(V1)
p26: U51#(tt(),V1,V2) -> activate#(V2)
p27: U52#(tt(),V2) -> U53#(isList(activate(V2)))
p28: U52#(tt(),V2) -> isList#(activate(V2))
p29: U52#(tt(),V2) -> activate#(V2)
p30: U61#(tt(),V) -> U62#(isQid(activate(V)))
p31: U61#(tt(),V) -> isQid#(activate(V))
p32: U61#(tt(),V) -> activate#(V)
p33: U71#(tt(),V) -> U72#(isNePal(activate(V)))
p34: U71#(tt(),V) -> isNePal#(activate(V))
p35: U71#(tt(),V) -> activate#(V)
p36: and#(tt(),X) -> activate#(X)
p37: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p38: isList#(V) -> isPalListKind#(activate(V))
p39: isList#(V) -> activate#(V)
p40: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p41: isList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p42: isList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p43: isList#(n____(V1,V2)) -> activate#(V1)
p44: isList#(n____(V1,V2)) -> activate#(V2)
p45: isNeList#(V) -> U31#(isPalListKind(activate(V)),activate(V))
p46: isNeList#(V) -> isPalListKind#(activate(V))
p47: isNeList#(V) -> activate#(V)
p48: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p49: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p50: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p51: isNeList#(n____(V1,V2)) -> activate#(V1)
p52: isNeList#(n____(V1,V2)) -> activate#(V2)
p53: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p54: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p55: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p56: isNeList#(n____(V1,V2)) -> activate#(V1)
p57: isNeList#(n____(V1,V2)) -> activate#(V2)
p58: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V))
p59: isNePal#(V) -> isPalListKind#(activate(V))
p60: isNePal#(V) -> activate#(V)
p61: isNePal#(n____(I,__(P,I))) -> and#(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
p62: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPalListKind(activate(I)))
p63: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I))
p64: isNePal#(n____(I,__(P,I))) -> activate#(I)
p65: isNePal#(n____(I,__(P,I))) -> isPal#(activate(P))
p66: isNePal#(n____(I,__(P,I))) -> activate#(P)
p67: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V))
p68: isPal#(V) -> isPalListKind#(activate(V))
p69: isPal#(V) -> activate#(V)
p70: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p71: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p72: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p73: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p74: activate#(n__nil()) -> nil#()
p75: activate#(n____(X1,X2)) -> __#(X1,X2)
p76: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p77: activate#(n__and(X1,X2)) -> and#(X1,X2)
p78: activate#(n__a()) -> a#()
p79: activate#(n__e()) -> e#()
p80: activate#(n__i()) -> i#()
p81: activate#(n__o()) -> o#()
p82: activate#(n__u()) -> u#()

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p34, p65, p67}
  {p4, p6, p7, p11, p16, p17, p21, p23, p24, p28, p37, p40, p48, p53}
  {p36, p70, p71, p72, p73, p76, p77}
  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isNePal#(n____(I,__(P,I))) -> isPal#(activate(P))
p2: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V))
p3: U71#(tt(),V) -> isNePal#(activate(V))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNePal#_A(x1) = ((0,1),(0,0)) x1 + (8,3)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (30,12)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (32,14)
          isPal#_A(x1) = ((1,1),(0,0)) x1 + (29,3)
          activate_A(x1) = x1 + (2,2)
          U71#_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (9,3)
          isPalListKind_A(x1) = ((1,0),(0,0)) x1 + (4,15)
          tt_A() = (3,2)
          nil_A() = (6,0)
          and_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (2,2)
          n__nil_A() = (4,0)
          n__and_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (1,1)
          a_A() = (1,2)
          n__a_A() = (0,1)
          e_A() = (6,0)
          n__e_A() = (4,0)
          i_A() = (4,3)
          n__i_A() = (4,2)
          o_A() = (5,4)
          n__o_A() = (4,2)
          u_A() = (5,3)
          n__u_A() = (4,2)
          n__isPalListKind_A(x1) = ((1,0),(0,0)) x1 + (4,13)
  
    precedence:
    
      isNePal# = isPal# > U71# > n____ = activate = isPalListKind = tt = and = n__and = a = e = n__e = i = n__i = o = n__o = u = n__isPalListKind > __ = n__a > n__u > nil = n__nil
    
    partial status:
  
      pi(isNePal#) = []
      pi(n____) = [1]
      pi(__) = []
      pi(isPal#) = []
      pi(activate) = []
      pi(U71#) = []
      pi(isPalListKind) = []
      pi(tt) = []
      pi(nil) = []
      pi(and) = []
      pi(n__nil) = []
      pi(n__and) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []
      pi(n__isPalListKind) = []

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isNePal#(n____(I,__(P,I))) -> isPal#(activate(P))
p2: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: U52#(tt(),V2) -> isList#(activate(V2))
p2: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p3: U21#(tt(),V1,V2) -> isList#(activate(V1))
p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p5: U11#(tt(),V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p7: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p9: U41#(tt(),V1,V2) -> isList#(activate(V1))
p10: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p11: U42#(tt(),V2) -> isNeList#(activate(V2))
p12: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p13: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p14: U22#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          U52#_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,0)) x2 + (21,1)
          tt_A() = (25,2)
          isList#_A(x1) = ((1,1),(1,0)) x1 + (13,3)
          activate_A(x1) = x1 + (0,5)
          n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (38,42)
          U21#_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,0)) x3 + (28,3)
          and_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (1,25)
          isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (89,6)
          n__isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (89,1)
          U11#_A(x1,x2) = ((1,1),(1,0)) x2 + (7,3)
          isNeList#_A(x1) = ((1,1),(1,0)) x1 + (1,3)
          U51#_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,0)) x3 + (27,36)
          U41#_A(x1,x2,x3) = ((1,1),(1,0)) x2 + ((1,1),(1,0)) x3 + (29,3)
          U42#_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,1),(1,0)) x2 + (17,3)
          isList_A(x1) = ((1,1),(0,0)) x1 + (93,4)
          isNeList_A(x1) = ((1,1),(0,1)) x1 + (95,30)
          U22#_A(x1,x2) = ((1,1),(1,0)) x2 + (19,3)
          U23_A(x1) = (26,3)
          U43_A(x1) = (26,2)
          U53_A(x1) = (26,3)
          U12_A(x1) = (26,3)
          U22_A(x1,x2) = (27,3)
          U32_A(x1) = (26,3)
          U42_A(x1,x2) = (27,2)
          U52_A(x1,x2) = (27,3)
          isQid_A(x1) = ((1,0),(0,0)) x1 + (0,4)
          n__a_A() = (26,1)
          n__e_A() = (26,1)
          n__i_A() = (26,2)
          n__o_A() = (26,1)
          n__u_A() = (26,1)
          ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (38,42)
          nil_A() = (0,1)
          U11_A(x1,x2) = ((0,1),(0,0)) x2 + (87,3)
          U21_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,1),(0,0)) x2 + (3,3)
          U31_A(x1,x2) = (27,3)
          U41_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (29,43)
          U51_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((1,0),(0,0)) x3 + (39,1)
          n__nil_A() = (0,1)
          a_A() = (26,1)
          e_A() = (26,1)
          i_A() = (26,2)
          o_A() = (26,2)
          u_A() = (26,2)
          n__and_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (1,25)
  
    precedence:
    
      U43 > isList# = U21# = U11# = isNeList# = U51# = U41# = U42# = U22# > activate = isPalListKind = isNeList = U23 = n__e = e > and = n__and > n__isPalListKind > U52# > U11 = u > n__o = o > isList > tt = U32 = isQid = U31 > i > U12 > __ > nil = n__nil > a > U53 > n__a > n__i > n__u > U52 = U51 > n____ = U22 = U42 = U21 = U41
    
    partial status:
  
      pi(U52#) = []
      pi(tt) = []
      pi(isList#) = []
      pi(activate) = [1]
      pi(n____) = [2]
      pi(U21#) = []
      pi(and) = [2]
      pi(isPalListKind) = []
      pi(n__isPalListKind) = []
      pi(U11#) = []
      pi(isNeList#) = []
      pi(U51#) = []
      pi(U41#) = []
      pi(U42#) = []
      pi(isList) = []
      pi(isNeList) = []
      pi(U22#) = []
      pi(U23) = []
      pi(U43) = []
      pi(U53) = []
      pi(U12) = []
      pi(U22) = []
      pi(U32) = []
      pi(U42) = []
      pi(U52) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []
      pi(n__and) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> isList#(activate(V1))
p3: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p4: U11#(tt(),V) -> isNeList#(activate(V))
p5: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p6: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p7: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p8: U41#(tt(),V1,V2) -> isList#(activate(V1))
p9: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p10: U42#(tt(),V2) -> isNeList#(activate(V2))
p11: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p12: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p13: U22#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p12, p13}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p3: U22#(tt(),V2) -> isList#(activate(V2))
p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p5: U11#(tt(),V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p7: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p8: U42#(tt(),V2) -> isNeList#(activate(V2))
p9: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p10: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p11: U41#(tt(),V1,V2) -> isList#(activate(V1))
p12: U21#(tt(),V1,V2) -> isList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isList#_A(x1) = ((1,1),(1,0)) x1 + (33,30)
          n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (182,90)
          U21#_A(x1,x2,x3) = ((0,1),(0,0)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,0)) x3 + (65,60)
          and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (13,1)
          isPalListKind_A(x1) = (16,2)
          activate_A(x1) = x1 + (15,1)
          n__isPalListKind_A(x1) = (1,1)
          tt_A() = (8,2)
          U22#_A(x1,x2) = ((1,1),(1,0)) x2 + (50,45)
          isList_A(x1) = ((0,1),(0,1)) x1 + (92,60)
          U11#_A(x1,x2) = ((1,0),(1,0)) x2 + (17,15)
          isNeList#_A(x1) = ((1,0),(1,0)) x1 + (1,0)
          U41#_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,0),(1,0)) x3 + (92,45)
          U42#_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(1,0)) x2 + (15,15)
          U51#_A(x1,x2,x3) = x1 + ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (9,13)
          U43_A(x1) = (9,3)
          U53_A(x1) = (9,3)
          U32_A(x1) = ((1,1),(0,0)) x1 + (1,3)
          U42_A(x1,x2) = (10,3)
          isNeList_A(x1) = ((0,0),(0,1)) x1 + (17,3)
          U52_A(x1,x2) = (10,3)
          isQid_A(x1) = (9,3)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          U23_A(x1) = ((0,0),(0,1)) x1 + (93,0)
          U31_A(x1,x2) = (14,3)
          U41_A(x1,x2,x3) = (16,3)
          U51_A(x1,x2,x3) = ((0,0),(0,1)) x3 + (11,3)
          U12_A(x1) = ((1,1),(0,1)) x1
          U22_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(0,1)) x2 + (86,61)
          ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (182,90)
          nil_A() = (1,3)
          U11_A(x1,x2) = ((0,1),(0,1)) x2 + (22,4)
          U21_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,0),(0,1)) x3 + (180,62)
          n__nil_A() = (0,2)
          a_A() = (2,1)
          e_A() = (1,1)
          i_A() = (2,2)
          o_A() = (2,2)
          u_A() = (2,2)
          n__and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (13,1)
  
    precedence:
    
      i > n__a > U51# > n__i > n__isPalListKind = o > U41# > isList# = U21# = and = isPalListKind = activate = U22# = U11# = isNeList# = U42# = U53 = U32 = isNeList = U31 = U51 > __ > n__and > n____ > nil = n__nil > U43 > u > n__u > n__e = e > isQid > a > n__o > U23 = U22 = U21 > U42 = U41 > U52 > tt = isList = U12 = U11
    
    partial status:
  
      pi(isList#) = []
      pi(n____) = [1]
      pi(U21#) = []
      pi(and) = []
      pi(isPalListKind) = []
      pi(activate) = []
      pi(n__isPalListKind) = []
      pi(tt) = []
      pi(U22#) = []
      pi(isList) = []
      pi(U11#) = []
      pi(isNeList#) = []
      pi(U41#) = []
      pi(U42#) = []
      pi(U51#) = [1, 2]
      pi(U43) = []
      pi(U53) = []
      pi(U32) = []
      pi(U42) = []
      pi(isNeList) = []
      pi(U52) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(U23) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(U12) = []
      pi(U22) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []
      pi(n__and) = [2]

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p3: U22#(tt(),V2) -> isList#(activate(V2))
p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p5: U11#(tt(),V) -> isNeList#(activate(V))
p6: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p7: U42#(tt(),V2) -> isNeList#(activate(V2))
p8: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p9: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p10: U41#(tt(),V1,V2) -> isList#(activate(V1))
p11: U21#(tt(),V1,V2) -> isList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p11}
  {p8, p9}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> isList#(activate(V1))
p3: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p4: U22#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isList#_A(x1) = ((1,0),(1,1)) x1 + (23,1)
          n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (36,0)
          U21#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (58,5)
          and_A(x1,x2) = x1 + x2 + (11,0)
          isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (21,2)
          activate_A(x1) = x1 + (0,2)
          n__isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (21,0)
          tt_A() = (25,2)
          U22#_A(x1,x2) = ((1,0),(1,1)) x2 + (24,3)
          isList_A(x1) = ((1,1),(0,1)) x1 + (22,4)
          U43_A(x1) = (26,2)
          U53_A(x1) = (26,6)
          U32_A(x1) = ((1,0),(0,0)) x1 + (1,3)
          U42_A(x1,x2) = (27,2)
          isNeList_A(x1) = x1 + (5,10)
          U52_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,0),(0,1)) x2 + (25,6)
          isQid_A(x1) = ((1,0),(0,0)) x1 + (2,4)
          n__a_A() = (24,1)
          n__e_A() = (24,1)
          n__i_A() = (24,0)
          n__o_A() = (24,0)
          n__u_A() = (24,1)
          U23_A(x1) = (26,3)
          U31_A(x1,x2) = ((1,0),(0,0)) x2 + (4,3)
          U41_A(x1,x2,x3) = ((0,0),(0,1)) x3 + (28,5)
          U51_A(x1,x2,x3) = ((0,1),(0,0)) x2 + x3 + (38,8)
          U12_A(x1) = ((1,1),(0,0)) x1 + (1,3)
          U22_A(x1,x2) = (27,3)
          ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (36,0)
          nil_A() = (25,3)
          U11_A(x1,x2) = ((1,1),(0,0)) x2 + (19,3)
          U21_A(x1,x2,x3) = ((0,1),(0,1)) x1 + (35,1)
          n__nil_A() = (25,2)
          a_A() = (24,1)
          e_A() = (24,1)
          i_A() = (24,1)
          o_A() = (24,0)
          u_A() = (24,1)
          n__and_A(x1,x2) = x1 + x2 + (11,0)
  
    precedence:
    
      n__u = u > isList# = n__o = o > U21# > and = isPalListKind = activate = n__isPalListKind > i > isNeList = U41 = U51 = __ > U52 > U53 > U31 > U42 > n____ > U32 > nil > n__a = a > n__nil > n__and > n__e = e > U43 > isQid > U22# > U23 = U12 = U22 = U11 > n__i > isList = U21 > tt
    
    partial status:
  
      pi(isList#) = []
      pi(n____) = [1, 2]
      pi(U21#) = [3]
      pi(and) = []
      pi(isPalListKind) = []
      pi(activate) = [1]
      pi(n__isPalListKind) = []
      pi(tt) = []
      pi(U22#) = []
      pi(isList) = [1]
      pi(U43) = []
      pi(U53) = []
      pi(U32) = []
      pi(U42) = []
      pi(isNeList) = []
      pi(U52) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(U23) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(U12) = []
      pi(U22) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []
      pi(n__and) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> isList#(activate(V1))
p3: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> isList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isList#_A(x1) = ((0,1),(0,1)) x1 + (1,0)
          n_____A(x1,x2) = ((0,0),(1,1)) x1 + x2 + (6,7)
          U21#_A(x1,x2,x3) = ((0,1),(0,1)) x2 + ((0,1),(0,0)) x3 + (4,2)
          and_A(x1,x2) = ((0,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (5,0)
          isPalListKind_A(x1) = (16,2)
          activate_A(x1) = ((1,1),(0,1)) x1 + (7,2)
          n__isPalListKind_A(x1) = (9,0)
          tt_A() = (8,2)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (20,8)
          nil_A() = (1,3)
          n__nil_A() = (1,1)
          a_A() = (10,3)
          n__a_A() = (9,1)
          e_A() = (1,1)
          n__e_A() = (1,1)
          i_A() = (9,1)
          n__i_A() = (1,1)
          o_A() = (2,3)
          n__o_A() = (1,1)
          u_A() = (2,1)
          n__u_A() = (1,0)
          n__and_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (1,0)
  
    precedence:
    
      tt > isList# > nil = n__nil = e > U21# > and = isPalListKind = activate = a = n__a = n__e = i = o = n__o = u = n__u = n__and > __ > n____ = n__isPalListKind = n__i
    
    partial status:
  
      pi(isList#) = []
      pi(n____) = []
      pi(U21#) = []
      pi(and) = []
      pi(isPalListKind) = []
      pi(activate) = []
      pi(n__isPalListKind) = []
      pi(tt) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []
      pi(n__and) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p2: U51#(tt(),V1,V2) -> isNeList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNeList#_A(x1) = ((1,0),(0,0)) x1 + (2,5)
          n_____A(x1,x2) = x1 + x2 + (8,4)
          U51#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (6,5)
          and_A(x1,x2) = ((0,1),(0,1)) x1 + ((1,1),(1,1)) x2 + (2,0)
          isPalListKind_A(x1) = ((1,0),(1,0)) x1 + (2,1)
          activate_A(x1) = ((1,0),(1,1)) x1 + (3,4)
          n__isPalListKind_A(x1) = ((1,0),(0,0)) x1
          tt_A() = (4,4)
          ___A(x1,x2) = x1 + x2 + (8,4)
          nil_A() = (4,0)
          n__nil_A() = (3,0)
          a_A() = (4,2)
          n__a_A() = (3,1)
          e_A() = (4,1)
          n__e_A() = (3,0)
          i_A() = (4,2)
          n__i_A() = (3,1)
          o_A() = (4,2)
          n__o_A() = (3,1)
          u_A() = (4,1)
          n__u_A() = (3,0)
          n__and_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,1),(0,1)) x2
  
    precedence:
    
      isNeList# = and = isPalListKind = activate = n__isPalListKind = nil > U51# > n____ = __ > n__nil > n__u > n__e > u > n__i > tt > n__a > a = e > i = n__o > o > n__and
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(U51#) = []
      pi(and) = []
      pi(isPalListKind) = []
      pi(activate) = []
      pi(n__isPalListKind) = []
      pi(tt) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []
      pi(n__and) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__and(X1,X2)) -> and#(X1,X2)
p3: and#(tt(),X) -> activate#(X)
p4: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p5: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p6: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p7: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPalListKind#_A(x1) = ((0,1),(0,1)) x1 + (4,1)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2
          activate#_A(x1) = ((0,1),(0,1)) x1 + (4,1)
          n__and_A(x1,x2) = x1 + ((1,1),(0,1)) x2
          and#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,1)) x2 + (3,1)
          tt_A() = (3,2)
          n__isPalListKind_A(x1) = ((0,0),(0,1)) x1
          activate_A(x1) = ((1,1),(0,1)) x1 + (2,0)
          isPalListKind_A(x1) = ((0,1),(0,1)) x1 + (1,0)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,0)
          nil_A() = (4,3)
          and_A(x1,x2) = x1 + ((1,1),(0,1)) x2
          n__nil_A() = (4,3)
          a_A() = (5,3)
          n__a_A() = (4,3)
          e_A() = (8,3)
          n__e_A() = (4,3)
          i_A() = (5,3)
          n__i_A() = (4,3)
          o_A() = (8,3)
          n__o_A() = (4,3)
          u_A() = (5,3)
          n__u_A() = (4,3)
  
    precedence:
    
      a = u > n__a > n__and = n__isPalListKind = activate = isPalListKind = and = e = n__e = i = n__o > n____ > __ > isPalListKind# = activate# = and# > n__u > tt = nil = n__nil = n__i > o
    
    partial status:
  
      pi(isPalListKind#) = []
      pi(n____) = [1, 2]
      pi(activate#) = []
      pi(n__and) = []
      pi(and#) = []
      pi(tt) = []
      pi(n__isPalListKind) = []
      pi(activate) = []
      pi(isPalListKind) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(and) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__and(X1,X2)) -> and#(X1,X2)
p3: and#(tt(),X) -> activate#(X)
p4: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p5: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p6: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p4: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p5: activate#(n__and(X1,X2)) -> and#(X1,X2)
p6: and#(tt(),X) -> activate#(X)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPalListKind#_A(x1) = ((1,1),(1,1)) x1 + (5,1)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (5,0)
          activate#_A(x1) = ((1,1),(1,0)) x1 + (6,3)
          n__isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (4,0)
          activate_A(x1) = x1 + (0,2)
          n__and_A(x1,x2) = x2 + (2,0)
          and#_A(x1,x2) = ((1,1),(1,0)) x2 + (7,3)
          tt_A() = (4,2)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (5,0)
          nil_A() = (5,1)
          and_A(x1,x2) = x2 + (2,2)
          isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (4,2)
          n__a_A() = (0,1)
          n__e_A() = (5,1)
          n__i_A() = (5,1)
          n__nil_A() = (5,1)
          n__o_A() = (5,2)
          n__u_A() = (5,1)
          a_A() = (0,1)
          e_A() = (5,1)
          i_A() = (5,1)
          o_A() = (5,2)
          u_A() = (5,1)
  
    precedence:
    
      isPalListKind# = n____ = activate# = n__isPalListKind = activate = n__and = and# = __ = nil = and = isPalListKind = n__nil = n__o = n__u = e = o = u > n__e > n__a = a > tt > n__i = i
    
    partial status:
  
      pi(isPalListKind#) = []
      pi(n____) = []
      pi(activate#) = []
      pi(n__isPalListKind) = []
      pi(activate) = []
      pi(n__and) = []
      pi(and#) = []
      pi(tt) = []
      pi(__) = []
      pi(nil) = []
      pi(and) = []
      pi(isPalListKind) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__nil) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p4: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p5: activate#(n__and(X1,X2)) -> and#(X1,X2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p3: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p4: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPalListKind#_A(x1) = ((1,1),(1,0)) x1 + (2,2)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (13,0)
          activate#_A(x1) = ((1,1),(1,0)) x1 + (14,2)
          n__isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (0,1)
          activate_A(x1) = x1 + (6,3)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (14,1)
          nil_A() = (2,2)
          and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (5,3)
          tt_A() = (0,2)
          isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (5,4)
          n__a_A() = (1,1)
          n__e_A() = (0,1)
          n__i_A() = (0,1)
          n__nil_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          n__and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (1,0)
          a_A() = (7,2)
          e_A() = (1,2)
          i_A() = (1,2)
          o_A() = (7,2)
          u_A() = (2,2)
  
    precedence:
    
      n__isPalListKind = and = tt = isPalListKind > n____ = activate = __ > n__e > n__nil > nil > n__u > n__and > e > n__i = i > n__o = o > n__a > a > u > isPalListKind# = activate#
    
    partial status:
  
      pi(isPalListKind#) = []
      pi(n____) = [1, 2]
      pi(activate#) = []
      pi(n__isPalListKind) = []
      pi(activate) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(and) = []
      pi(tt) = []
      pi(isPalListKind) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__nil) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__and) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPalListKind#_A(x1) = x1
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (10,0)
          activate#_A(x1) = x1
          n__isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (2,0)
          activate_A(x1) = x1 + (2,0)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (10,0)
          nil_A() = (3,1)
          and_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (3,0)
          tt_A() = (0,0)
          isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (2,0)
          n__a_A() = (1,0)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__nil_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          n__and_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (3,0)
          a_A() = (3,0)
          e_A() = (2,1)
          i_A() = (2,1)
          o_A() = (1,1)
          u_A() = (2,1)
  
    precedence:
    
      n__isPalListKind = and = isPalListKind = n__and > isPalListKind# > n____ = activate# = __ = tt > activate = n__i > n__a = a > i > nil = n__nil > o > n__o > n__e = e = u > n__u
    
    partial status:
  
      pi(isPalListKind#) = [1]
      pi(n____) = []
      pi(activate#) = [1]
      pi(n__isPalListKind) = []
      pi(activate) = [1]
      pi(__) = []
      pi(nil) = []
      pi(and) = []
      pi(tt) = []
      pi(isPalListKind) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__nil) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__and) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21, r32, r33, r34, r35, r36, r37, r38, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPalListKind#_A(x1) = ((0,1),(1,1)) x1 + (2,7)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (8,15)
          activate_A(x1) = x1 + (2,7)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (8,15)
          nil_A() = (4,1)
          and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (3,2)
          tt_A() = (5,2)
          isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (2,7)
          n__a_A() = (6,1)
          n__e_A() = (4,1)
          n__i_A() = (4,1)
          n__nil_A() = (4,1)
          n__o_A() = (4,1)
          n__u_A() = (4,1)
          n__isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (2,0)
          n__and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (2,1)
          a_A() = (7,2)
          e_A() = (5,2)
          i_A() = (5,2)
          o_A() = (5,2)
          u_A() = (5,2)
  
    precedence:
    
      isPalListKind# = activate = and = isPalListKind = n__a = n__e = n__i = n__o = n__isPalListKind = n__and = a = e = i = o = u > __ = tt > nil = n__nil > n__u > n____
    
    partial status:
  
      pi(isPalListKind#) = []
      pi(n____) = []
      pi(activate) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(and) = []
      pi(tt) = []
      pi(isPalListKind) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__nil) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__isPalListKind) = []
      pi(n__and) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          __#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,2)
          ___A(x1,x2) = x1 + x2 + (2,1)
          nil_A() = (1,1)
          n_____A(x1,x2) = (1,1)
  
    precedence:
    
      __ > __# = nil = n____
    
    partial status:
  
      pi(__#) = [1]
      pi(__) = []
      pi(nil) = []
      pi(n____) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: a() -> n__a()
r49: e() -> n__e()
r50: i() -> n__i()
r51: o() -> n__o()
r52: u() -> n__u()
r53: activate(n__nil()) -> nil()
r54: activate(n____(X1,X2)) -> __(X1,X2)
r55: activate(n__isPalListKind(X)) -> isPalListKind(X)
r56: activate(n__and(X1,X2)) -> and(X1,X2)
r57: activate(n__a()) -> a()
r58: activate(n__e()) -> e()
r59: activate(n__i()) -> i()
r60: activate(n__o()) -> o()
r61: activate(n__u()) -> u()
r62: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          __#_A(x1,x2) = ((1,1),(0,1)) x1 + (2,2)
          ___A(x1,x2) = x1 + x2 + (1,1)
          nil_A() = (1,1)
          n_____A(x1,x2) = (0,0)
  
    precedence:
    
      __ > __# = nil = n____
    
    partial status:
  
      pi(__#) = [1]
      pi(__) = []
      pi(nil) = []
      pi(n____) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.