YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  and(tt(),X) -> activate(X)
  isList(V) -> isNeList(activate(V))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
  isNeList(V) -> isQid(activate(V))
  isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
  isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
  isNePal(V) -> isQid(activate(V))
  isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
  isPal(V) -> isNePal(activate(V))
  isPal(n__nil()) -> tt()
  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)
  isList(X) -> n__isList(X)
  isNeList(X) -> n__isNeList(X)
  isPal(X) -> n__isPal(X)
  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__isList(X)) -> isList(X)
  activate(n__isNeList(X)) -> isNeList(X)
  activate(n__isPal(X)) -> isPal(X)
  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: and#(tt(),X) -> activate#(X)
p4: isList#(V) -> isNeList#(activate(V))
p5: isList#(V) -> activate#(V)
p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p7: isList#(n____(V1,V2)) -> isList#(activate(V1))
p8: isList#(n____(V1,V2)) -> activate#(V1)
p9: isList#(n____(V1,V2)) -> activate#(V2)
p10: isNeList#(V) -> isQid#(activate(V))
p11: isNeList#(V) -> activate#(V)
p12: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p14: isNeList#(n____(V1,V2)) -> activate#(V1)
p15: isNeList#(n____(V1,V2)) -> activate#(V2)
p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p17: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p18: isNeList#(n____(V1,V2)) -> activate#(V1)
p19: isNeList#(n____(V1,V2)) -> activate#(V2)
p20: isNePal#(V) -> isQid#(activate(V))
p21: isNePal#(V) -> activate#(V)
p22: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p23: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I))
p24: isNePal#(n____(I,__(P,I))) -> activate#(I)
p25: isNePal#(n____(I,__(P,I))) -> activate#(P)
p26: isPal#(V) -> isNePal#(activate(V))
p27: isPal#(V) -> activate#(V)
p28: activate#(n__nil()) -> nil#()
p29: activate#(n____(X1,X2)) -> __#(X1,X2)
p30: activate#(n__isList(X)) -> isList#(X)
p31: activate#(n__isNeList(X)) -> isNeList#(X)
p32: activate#(n__isPal(X)) -> isPal#(X)
p33: activate#(n__a()) -> a#()
p34: activate#(n__e()) -> e#()
p35: activate#(n__i()) -> i#()
p36: activate#(n__o()) -> o#()
p37: activate#(n__u()) -> u#()

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p3, p4, p5, p6, p7, p8, p9, p11, p12, p13, p14, p15, p16, p17, p18, p19, p21, p22, p24, p25, p26, p27, p30, p31, p32}
  {p1, p2}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: activate#(n__isList(X)) -> isList#(X)
p8: isList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(n____(V1,V2)) -> activate#(V1)
p10: isList#(n____(V1,V2)) -> isList#(activate(V1))
p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p12: and#(tt(),X) -> activate#(X)
p13: isList#(V) -> activate#(V)
p14: isList#(V) -> isNeList#(activate(V))
p15: isNeList#(n____(V1,V2)) -> activate#(V1)
p16: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p17: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p18: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p19: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p20: isNeList#(V) -> activate#(V)
p21: isNePal#(n____(I,__(P,I))) -> activate#(I)
p22: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p23: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: 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, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      isPal#_A(x1) = x1
      activate#_A(x1) = x1
      n__isPal_A(x1) = x1
      isNePal#_A(x1) = x1
      activate_A(x1) = x1
      n_____A(x1,x2) = x1 + x2
      ___A(x1,x2) = x1 + x2
      n__isNeList_A(x1) = x1
      isNeList#_A(x1) = x1
      n__isList_A(x1) = x1
      isList#_A(x1) = x1
      and#_A(x1,x2) = x1 + x2
      isList_A(x1) = x1
      tt_A() = 1
      isNeList_A(x1) = x1
      isQid_A(x1) = x1
      isNePal_A(x1) = x1
      and_A(x1,x2) = x2
      nil_A() = 1
      isPal_A(x1) = x1
      n__nil_A() = 1
      a_A() = 1
      n__a_A() = 1
      e_A() = 1
      n__e_A() = 1
      i_A() = 1
      n__i_A() = 1
      o_A() = 1
      n__o_A() = 1
      u_A() = 1
      n__u_A() = 1

The next rules are strictly ordered:

  p12

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: activate#(n__isList(X)) -> isList#(X)
p8: isList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(n____(V1,V2)) -> activate#(V1)
p10: isList#(n____(V1,V2)) -> isList#(activate(V1))
p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p12: isList#(V) -> activate#(V)
p13: isList#(V) -> isNeList#(activate(V))
p14: isNeList#(n____(V1,V2)) -> activate#(V1)
p15: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p17: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p18: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p19: isNeList#(V) -> activate#(V)
p20: isNePal#(n____(I,__(P,I))) -> activate#(I)
p21: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p22: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p12, p13, p14, p15, p17, p19, p20, p22}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isList(X)) -> isList#(X)
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(V) -> activate#(V)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p7: isList#(V) -> activate#(V)
p8: activate#(n__isPal(X)) -> isPal#(X)
p9: isPal#(V) -> isNePal#(activate(V))
p10: isNePal#(V) -> activate#(V)
p11: isNePal#(n____(I,__(P,I))) -> activate#(I)
p12: isNePal#(n____(I,__(P,I))) -> activate#(P)
p13: isList#(n____(V1,V2)) -> isList#(activate(V1))
p14: isList#(n____(V1,V2)) -> activate#(V1)
p15: isList#(n____(V1,V2)) -> activate#(V2)
p16: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p17: isNeList#(n____(V1,V2)) -> activate#(V1)
p18: isNeList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: 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, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      isPal#_A(x1) = x1 + 1
      activate#_A(x1) = x1
      n__isList_A(x1) = x1 + 3
      isList#_A(x1) = x1 + 2
      isNeList#_A(x1) = x1 + 1
      activate_A(x1) = x1 + 1
      n__isNeList_A(x1) = x1 + 1
      n_____A(x1,x2) = x1 + x2 + 5
      n__isPal_A(x1) = x1 + 1
      isNePal#_A(x1) = x1
      ___A(x1,x2) = x1 + x2 + 5
      and_A(x1,x2) = x1 + x2
      tt_A() = 1
      isNePal_A(x1) = x1 + 1
      isQid_A(x1) = 1
      n__a_A() = 1
      n__e_A() = 1
      n__i_A() = 1
      n__o_A() = 1
      n__u_A() = 1
      nil_A() = 1
      isList_A(x1) = x1 + 3
      isNeList_A(x1) = x1 + 1
      n__nil_A() = 1
      isPal_A(x1) = x1 + 2
      a_A() = 1
      e_A() = 1
      i_A() = 1
      o_A() = 1
      u_A() = 1

The next rules are strictly ordered:

  p1, p2, p4, p6, p7, p11, p12, p13, p14, p15, p16, p17, p18

We remove them from the problem.

-- SCC decomposition.

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

p1: isList#(V) -> isNeList#(activate(V))
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: activate#(n__isPal(X)) -> isPal#(X)
p4: isPal#(V) -> isNePal#(activate(V))
p5: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p3, p4, p5}


-- Reduction pair.

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

p1: activate#(n__isPal(X)) -> isPal#(X)
p2: isPal#(V) -> isNePal#(activate(V))
p3: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: 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, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      activate#_A(x1) = x1
      n__isPal_A(x1) = x1 + 4
      isPal#_A(x1) = x1 + 3
      isNePal#_A(x1) = x1 + 1
      activate_A(x1) = x1 + 1
      and_A(x1,x2) = x2 + 1
      tt_A() = 1
      isNePal_A(x1) = x1 + 4
      isQid_A(x1) = 1
      n_____A(x1,x2) = x1 + x2 + 1
      ___A(x1,x2) = x1 + x2 + 1
      n__a_A() = 1
      n__e_A() = 1
      n__i_A() = 1
      n__o_A() = 1
      n__u_A() = 1
      nil_A() = 1
      isList_A(x1) = 1
      isNeList_A(x1) = 1
      n__nil_A() = 1
      n__isList_A(x1) = 0
      n__isNeList_A(x1) = 0
      isPal_A(x1) = x1 + 5
      a_A() = 1
      e_A() = 1
      i_A() = 1
      o_A() = 1
      u_A() = 1

The next rules are strictly ordered:

  p1, p2, p3

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: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      __#_A(x1,x2) = x1
      ___A(x1,x2) = x1 + x2 + 1
      nil_A() = 0
      n_____A(x1,x2) = 0

The next rules are strictly ordered:

  p1, p2

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