YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  U11(tt()) -> tt()
  U21(tt(),V2) -> U22(isList(activate(V2)))
  U22(tt()) -> tt()
  U31(tt()) -> tt()
  U41(tt(),V2) -> U42(isNeList(activate(V2)))
  U42(tt()) -> tt()
  U51(tt(),V2) -> U52(isList(activate(V2)))
  U52(tt()) -> tt()
  U61(tt()) -> tt()
  U71(tt(),P) -> U72(isPal(activate(P)))
  U72(tt()) -> tt()
  U81(tt()) -> tt()
  isList(V) -> U11(isNeList(activate(V)))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
  isNeList(V) -> U31(isQid(activate(V)))
  isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
  isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
  isNePal(V) -> U61(isQid(activate(V)))
  isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
  isPal(V) -> U81(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)
  a() -> n__a()
  e() -> n__e()
  i() -> n__i()
  o() -> n__o()
  u() -> n__u()
  activate(n__nil()) -> nil()
  activate(n____(X1,X2)) -> __(activate(X1),activate(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: U21#(tt(),V2) -> U22#(isList(activate(V2)))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: U21#(tt(),V2) -> activate#(V2)
p6: U41#(tt(),V2) -> U42#(isNeList(activate(V2)))
p7: U41#(tt(),V2) -> isNeList#(activate(V2))
p8: U41#(tt(),V2) -> activate#(V2)
p9: U51#(tt(),V2) -> U52#(isList(activate(V2)))
p10: U51#(tt(),V2) -> isList#(activate(V2))
p11: U51#(tt(),V2) -> activate#(V2)
p12: U71#(tt(),P) -> U72#(isPal(activate(P)))
p13: U71#(tt(),P) -> isPal#(activate(P))
p14: U71#(tt(),P) -> activate#(P)
p15: isList#(V) -> U11#(isNeList(activate(V)))
p16: isList#(V) -> isNeList#(activate(V))
p17: isList#(V) -> activate#(V)
p18: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p19: isList#(n____(V1,V2)) -> isList#(activate(V1))
p20: isList#(n____(V1,V2)) -> activate#(V1)
p21: isList#(n____(V1,V2)) -> activate#(V2)
p22: isNeList#(V) -> U31#(isQid(activate(V)))
p23: isNeList#(V) -> isQid#(activate(V))
p24: isNeList#(V) -> activate#(V)
p25: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p26: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p27: isNeList#(n____(V1,V2)) -> activate#(V1)
p28: isNeList#(n____(V1,V2)) -> activate#(V2)
p29: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p30: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p31: isNeList#(n____(V1,V2)) -> activate#(V1)
p32: isNeList#(n____(V1,V2)) -> activate#(V2)
p33: isNePal#(V) -> U61#(isQid(activate(V)))
p34: isNePal#(V) -> isQid#(activate(V))
p35: isNePal#(V) -> activate#(V)
p36: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P))
p37: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I))
p38: isNePal#(n____(I,n____(P,I))) -> activate#(I)
p39: isNePal#(n____(I,n____(P,I))) -> activate#(P)
p40: isPal#(V) -> U81#(isNePal(activate(V)))
p41: isPal#(V) -> isNePal#(activate(V))
p42: isPal#(V) -> activate#(V)
p43: activate#(n__nil()) -> nil#()
p44: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
p45: activate#(n____(X1,X2)) -> activate#(X1)
p46: activate#(n____(X1,X2)) -> activate#(X2)
p47: activate#(n__a()) -> a#()
p48: activate#(n__e()) -> e#()
p49: activate#(n__i()) -> i#()
p50: activate#(n__o()) -> o#()
p51: 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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p13, p36, p41}
  {p4, p7, p10, p16, p18, p19, p25, p26, p29, p30}
  {p45, p46}
  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((0,1),(0,1)) x1 + (7,9)
          isNePal#_A(x1) = ((0,1),(0,1)) x1 + (6,2)
          activate_A(x1) = ((1,1),(0,1)) x1 + (8,0)
          n_____A(x1,x2) = x1 + x2 + (1,10)
          U71#_A(x1,x2) = ((1,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (1,1)
          isQid_A(x1) = ((0,1),(0,1)) x1 + (3,21)
          tt_A() = (0,8)
          ___A(x1,x2) = x1 + x2 + (2,10)
          nil_A() = (1,1)
          n__nil_A() = (0,1)
          a_A() = (1,1)
          n__a_A() = (0,1)
          e_A() = (1,8)
          n__e_A() = (0,8)
          i_A() = (1,1)
          n__i_A() = (0,1)
          o_A() = (1,8)
          n__o_A() = (0,8)
          u_A() = (1,8)
          n__u_A() = (1,8)
  
    precedence:
    
      activate = n____ = __ = nil = n__e > isQid = e > n__nil > tt = n__o > n__a = n__i > U71# = o = u > i = n__u > isPal# = isNePal# = a
    
    partial status:
  
      pi(isPal#) = []
      pi(isNePal#) = []
      pi(activate) = []
      pi(n____) = []
      pi(U71#) = [1]
      pi(isQid) = []
      pi(tt) = []
      pi(__) = []
      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) = []

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: isPal#(V) -> isNePal#(activate(V))
p2: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p5: U21#(tt(),V2) -> isList#(activate(V2))
p6: isList#(V) -> isNeList#(activate(V))
p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p9: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p10: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

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 + (6,4)
          n_____A(x1,x2) = x1 + x2 + (5,3)
          U51#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (4,4)
          isNeList_A(x1) = ((0,0),(1,0)) x1 + (7,5)
          activate_A(x1) = x1
          tt_A() = (4,2)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (7,4)
          U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (12,4)
          isList_A(x1) = (9,2)
          U41#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,4)
          U22_A(x1) = (5,2)
          U42_A(x1) = (6,3)
          U52_A(x1) = (5,3)
          ___A(x1,x2) = x1 + x2 + (5,3)
          nil_A() = (5,0)
          U11_A(x1) = ((1,0),(0,0)) x1 + (1,2)
          U21_A(x1,x2) = ((0,1),(0,0)) x1 + (4,2)
          U31_A(x1) = (5,2)
          U41_A(x1,x2) = ((0,1),(0,0)) x1 + (4,3)
          U51_A(x1,x2) = (6,3)
          isQid_A(x1) = ((0,1),(0,1)) x1 + (8,6)
          n__a_A() = (5,0)
          n__e_A() = (5,0)
          n__i_A() = (5,1)
          n__o_A() = (5,1)
          n__u_A() = (5,0)
          n__nil_A() = (5,0)
          a_A() = (5,0)
          e_A() = (5,0)
          i_A() = (5,1)
          o_A() = (5,1)
          u_A() = (5,0)
  
    precedence:
    
      U22 > n__o = o > n____ = isNeList = activate = U42 = U52 = __ = U41 = U51 = a > isNeList# = U51# = isList# = U21# = U41# = i > isList > nil = n__nil = u > n__a > U31 > e > U11 > n__e > n__i > n__u > tt = U21 = isQid
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(U51#) = []
      pi(isNeList) = []
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(U21#) = []
      pi(isList) = []
      pi(U41#) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__nil) = []
      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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: isList#(V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p9: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p5: U41#(tt(),V2) -> isNeList#(activate(V2))
p6: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p7: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p8: U21#(tt(),V2) -> isList#(activate(V2))
p9: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

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 + (15,18)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (6,17)
          U51#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (8,18)
          isNeList_A(x1) = ((1,0),(1,0)) x1 + (12,18)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,1)
          tt_A() = (14,16)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (21,18)
          U41#_A(x1,x2) = ((1,0),(0,0)) x2 + (16,18)
          isList_A(x1) = ((0,1),(1,1)) x1 + (27,24)
          U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (21,18)
          U22_A(x1) = (14,16)
          U42_A(x1) = (15,16)
          U52_A(x1) = (15,17)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (6,17)
          nil_A() = (0,0)
          U11_A(x1) = (26,24)
          U21_A(x1,x2) = x1 + (15,0)
          U31_A(x1) = ((0,1),(0,0)) x1 + (1,16)
          U41_A(x1,x2) = (18,17)
          U51_A(x1,x2) = ((0,1),(0,0)) x1 + (0,17)
          isQid_A(x1) = ((1,0),(1,0)) x1 + (0,10)
          n__a_A() = (15,16)
          n__e_A() = (15,16)
          n__i_A() = (15,16)
          n__o_A() = (15,16)
          n__u_A() = (15,16)
          n__nil_A() = (0,0)
          a_A() = (15,17)
          e_A() = (15,17)
          i_A() = (15,17)
          o_A() = (15,17)
          u_A() = (15,17)
  
    precedence:
    
      isNeList = activate = U42 = __ = U41 > isNeList# = U51# = isList# = U21# > U41# > U52 = U51 > isList > U21 > tt = U22 = isQid > u > e > n__e > o > nil = n__nil > i > n__u > a > n__a > n__i > n__o > n____ > U11 = U31
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = [1]
      pi(U51#) = []
      pi(isNeList) = []
      pi(activate) = []
      pi(tt) = []
      pi(isList#) = []
      pi(U41#) = []
      pi(isList) = []
      pi(U21#) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = []
      pi(nil) = []
      pi(U11) = []
      pi(U21) = [1]
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: U41#(tt(),V2) -> isNeList#(activate(V2))
p5: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p6: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p7: U21#(tt(),V2) -> isList#(activate(V2))
p8: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p5, p6, p7, p8}


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: isList#(V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNeList#_A(x1) = ((0,1),(0,0)) x1 + (4,10)
          n_____A(x1,x2) = x1 + x2 + (3,9)
          U51#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,0)) x2 + (6,10)
          isNeList_A(x1) = ((0,1),(0,1)) x1 + (6,6)
          activate_A(x1) = ((1,1),(0,1)) x1 + (7,0)
          tt_A() = (0,0)
          isList#_A(x1) = ((0,1),(0,0)) x1 + (5,10)
          U21#_A(x1,x2) = ((0,1),(0,0)) x2 + (6,10)
          isList_A(x1) = ((1,0),(1,0)) x1 + (9,4)
          U22_A(x1) = (0,0)
          U42_A(x1) = (0,1)
          U52_A(x1) = (1,1)
          ___A(x1,x2) = x1 + x2 + (4,9)
          nil_A() = (2,1)
          U11_A(x1) = (8,1)
          U21_A(x1,x2) = (0,0)
          U31_A(x1) = (0,0)
          U41_A(x1,x2) = (0,6)
          U51_A(x1,x2) = (2,10)
          isQid_A(x1) = ((0,1),(0,1)) x1 + (7,7)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (0,1)
          n__u_A() = (1,1)
          n__nil_A() = (1,1)
          a_A() = (2,1)
          e_A() = (2,1)
          i_A() = (2,1)
          o_A() = (1,1)
          u_A() = (2,1)
  
    precedence:
    
      n____ = __ > U41 > U42 > isList > U22 = U21 > a > isNeList# = U51# = isNeList = activate = isList# = U52 = U51 = n__a > u > n__e > o > e > U21# > i > n__i > n__nil > nil > tt = U11 = U31 = isQid = n__o = n__u
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(U51#) = []
      pi(isNeList) = []
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(U21#) = []
      pi(isList) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = []
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__nil) = []
      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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: U21#(tt(),V2) -> isList#(activate(V2))
p4: isList#(V) -> isNeList#(activate(V))
p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p6: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p4, p5, p6}


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p5: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

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,2)
          n_____A(x1,x2) = x1 + x2 + (8,2)
          U51#_A(x1,x2) = ((1,0),(0,0)) x2 + (6,2)
          isNeList_A(x1) = ((1,1),(0,1)) x1 + (4,0)
          activate_A(x1) = ((1,0),(1,1)) x1 + (0,7)
          tt_A() = (0,0)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (4,2)
          U22_A(x1) = (1,1)
          U11_A(x1) = (1,1)
          U21_A(x1,x2) = ((0,1),(0,0)) x2 + (2,3)
          isList_A(x1) = ((1,1),(0,0)) x1 + (9,3)
          U42_A(x1) = (0,0)
          U52_A(x1) = (0,0)
          ___A(x1,x2) = x1 + x2 + (8,2)
          nil_A() = (1,2)
          U31_A(x1) = (0,0)
          U41_A(x1,x2) = (0,0)
          U51_A(x1,x2) = (0,0)
          n__nil_A() = (1,1)
          isQid_A(x1) = ((0,0),(0,1)) x1 + (5,0)
          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)
          a_A() = (1,2)
          e_A() = (1,2)
          i_A() = (1,2)
          o_A() = (1,2)
          u_A() = (1,2)
  
    precedence:
    
      isNeList = activate = U11 = U21 = isList = __ = u > nil > o > U22 > a > n__a > i > n__nil > n__o > U31 > n__u > e > n__e = n__i > isNeList# = n____ = U51# = tt = isList# = U42 = U52 = U41 = U51 = isQid
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(U51#) = []
      pi(isNeList) = []
      pi(activate) = []
      pi(tt) = []
      pi(isList#) = []
      pi(U22) = []
      pi(U11) = []
      pi(U21) = []
      pi(isList) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = []
      pi(nil) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(n__nil) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p5

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#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNeList#_A(x1) = ((0,1),(0,0)) x1 + (8,7)
          n_____A(x1,x2) = x1 + x2 + (11,6)
          U51#_A(x1,x2) = ((0,1),(0,0)) x2 + (13,7)
          isNeList_A(x1) = ((1,1),(1,0)) x1 + (5,5)
          activate_A(x1) = ((1,1),(0,1)) x1 + (4,0)
          tt_A() = (0,0)
          isList#_A(x1) = ((0,1),(0,0)) x1 + (12,7)
          U22_A(x1) = (1,1)
          U11_A(x1) = (0,0)
          U21_A(x1,x2) = (2,7)
          isList_A(x1) = ((0,0),(0,1)) x1 + (3,8)
          U42_A(x1) = (1,1)
          U52_A(x1) = (0,0)
          ___A(x1,x2) = x1 + x2 + (12,6)
          nil_A() = (1,1)
          U31_A(x1) = (0,0)
          U41_A(x1,x2) = ((0,1),(0,0)) x1 + (2,9)
          U51_A(x1,x2) = (0,0)
          n__nil_A() = (1,1)
          isQid_A(x1) = ((0,0),(0,1)) x1 + (1,6)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,0)
          n__u_A() = (1,1)
          a_A() = (2,1)
          e_A() = (2,1)
          i_A() = (2,1)
          o_A() = (2,0)
          u_A() = (2,1)
  
    precedence:
    
      activate = U11 = __ = u > U22 > i > U21 = isList > o > a > n__i > e > U51# > isNeList# = isList# > nil = n__nil > isQid = n__a > n__e > U42 > n__u > n__o > n____ = isNeList = tt = U52 = U31 = U41 = U51
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(U51#) = []
      pi(isNeList) = []
      pi(activate) = []
      pi(tt) = []
      pi(isList#) = []
      pi(U22) = []
      pi(U11) = []
      pi(U21) = []
      pi(isList) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = []
      pi(nil) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(n__nil) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: isList#(V) -> isNeList#(activate(V))
p3: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3}


-- Reduction pair.

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

p1: isList#(V) -> isNeList#(activate(V))
p2: isNeList#(n____(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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isList#_A(x1) = x1 + (2,1)
          isNeList#_A(x1) = x1 + (1,1)
          activate_A(x1) = x1
          n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (3,1)
          ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (3,1)
          nil_A() = (1,1)
          n__nil_A() = (1,1)
          a_A() = (1,1)
          n__a_A() = (1,1)
          e_A() = (1,1)
          n__e_A() = (1,1)
          i_A() = (1,1)
          n__i_A() = (1,1)
          o_A() = (1,1)
          n__o_A() = (1,1)
          u_A() = (1,1)
          n__u_A() = (1,1)
  
    precedence:
    
      isList# > activate = n____ = __ = nil > n__nil > isNeList# > a = n__a = e = n__e > i > u > n__i > n__u > o > n__o
    
    partial status:
  
      pi(isList#) = [1]
      pi(isNeList#) = [1]
      pi(activate) = [1]
      pi(n____) = []
      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) = []

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#(V) -> isNeList#(activate(V))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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: activate#(n____(X1,X2)) -> activate#(X2)
p2: activate#(n____(X1,X2)) -> activate#(X1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

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: activate#(n____(X1,X2)) -> activate#(X1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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: activate#(n____(X1,X2)) -> activate#(X1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r32

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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r32

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.