YES

We show the termination of the TRS R:

  active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
  active(__(X,nil())) -> mark(X)
  active(__(nil(),X)) -> mark(X)
  active(and(tt(),X)) -> mark(X)
  active(isList(V)) -> mark(isNeList(V))
  active(isList(nil())) -> mark(tt())
  active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
  active(isNeList(V)) -> mark(isQid(V))
  active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
  active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
  active(isNePal(V)) -> mark(isQid(V))
  active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
  active(isPal(V)) -> mark(isNePal(V))
  active(isPal(nil())) -> mark(tt())
  active(isQid(a())) -> mark(tt())
  active(isQid(e())) -> mark(tt())
  active(isQid(i())) -> mark(tt())
  active(isQid(o())) -> mark(tt())
  active(isQid(u())) -> mark(tt())
  active(__(X1,X2)) -> __(active(X1),X2)
  active(__(X1,X2)) -> __(X1,active(X2))
  active(and(X1,X2)) -> and(active(X1),X2)
  __(mark(X1),X2) -> mark(__(X1,X2))
  __(X1,mark(X2)) -> mark(__(X1,X2))
  and(mark(X1),X2) -> mark(and(X1,X2))
  proper(__(X1,X2)) -> __(proper(X1),proper(X2))
  proper(nil()) -> ok(nil())
  proper(and(X1,X2)) -> and(proper(X1),proper(X2))
  proper(tt()) -> ok(tt())
  proper(isList(X)) -> isList(proper(X))
  proper(isNeList(X)) -> isNeList(proper(X))
  proper(isQid(X)) -> isQid(proper(X))
  proper(isNePal(X)) -> isNePal(proper(X))
  proper(isPal(X)) -> isPal(proper(X))
  proper(a()) -> ok(a())
  proper(e()) -> ok(e())
  proper(i()) -> ok(i())
  proper(o()) -> ok(o())
  proper(u()) -> ok(u())
  __(ok(X1),ok(X2)) -> ok(__(X1,X2))
  and(ok(X1),ok(X2)) -> ok(and(X1,X2))
  isList(ok(X)) -> ok(isList(X))
  isNeList(ok(X)) -> ok(isNeList(X))
  isQid(ok(X)) -> ok(isQid(X))
  isNePal(ok(X)) -> ok(isNePal(X))
  isPal(ok(X)) -> ok(isPal(X))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

-- SCC decomposition.

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

p1: active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
p2: active#(__(__(X,Y),Z)) -> __#(Y,Z)
p3: active#(isList(V)) -> isNeList#(V)
p4: active#(isList(__(V1,V2))) -> and#(isList(V1),isList(V2))
p5: active#(isList(__(V1,V2))) -> isList#(V1)
p6: active#(isList(__(V1,V2))) -> isList#(V2)
p7: active#(isNeList(V)) -> isQid#(V)
p8: active#(isNeList(__(V1,V2))) -> and#(isList(V1),isNeList(V2))
p9: active#(isNeList(__(V1,V2))) -> isList#(V1)
p10: active#(isNeList(__(V1,V2))) -> isNeList#(V2)
p11: active#(isNeList(__(V1,V2))) -> and#(isNeList(V1),isList(V2))
p12: active#(isNeList(__(V1,V2))) -> isNeList#(V1)
p13: active#(isNeList(__(V1,V2))) -> isList#(V2)
p14: active#(isNePal(V)) -> isQid#(V)
p15: active#(isNePal(__(I,__(P,I)))) -> and#(isQid(I),isPal(P))
p16: active#(isNePal(__(I,__(P,I)))) -> isQid#(I)
p17: active#(isNePal(__(I,__(P,I)))) -> isPal#(P)
p18: active#(isPal(V)) -> isNePal#(V)
p19: active#(__(X1,X2)) -> __#(active(X1),X2)
p20: active#(__(X1,X2)) -> active#(X1)
p21: active#(__(X1,X2)) -> __#(X1,active(X2))
p22: active#(__(X1,X2)) -> active#(X2)
p23: active#(and(X1,X2)) -> and#(active(X1),X2)
p24: active#(and(X1,X2)) -> active#(X1)
p25: __#(mark(X1),X2) -> __#(X1,X2)
p26: __#(X1,mark(X2)) -> __#(X1,X2)
p27: and#(mark(X1),X2) -> and#(X1,X2)
p28: proper#(__(X1,X2)) -> __#(proper(X1),proper(X2))
p29: proper#(__(X1,X2)) -> proper#(X1)
p30: proper#(__(X1,X2)) -> proper#(X2)
p31: proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
p32: proper#(and(X1,X2)) -> proper#(X1)
p33: proper#(and(X1,X2)) -> proper#(X2)
p34: proper#(isList(X)) -> isList#(proper(X))
p35: proper#(isList(X)) -> proper#(X)
p36: proper#(isNeList(X)) -> isNeList#(proper(X))
p37: proper#(isNeList(X)) -> proper#(X)
p38: proper#(isQid(X)) -> isQid#(proper(X))
p39: proper#(isQid(X)) -> proper#(X)
p40: proper#(isNePal(X)) -> isNePal#(proper(X))
p41: proper#(isNePal(X)) -> proper#(X)
p42: proper#(isPal(X)) -> isPal#(proper(X))
p43: proper#(isPal(X)) -> proper#(X)
p44: __#(ok(X1),ok(X2)) -> __#(X1,X2)
p45: and#(ok(X1),ok(X2)) -> and#(X1,X2)
p46: isList#(ok(X)) -> isList#(X)
p47: isNeList#(ok(X)) -> isNeList#(X)
p48: isQid#(ok(X)) -> isQid#(X)
p49: isNePal#(ok(X)) -> isNePal#(X)
p50: isPal#(ok(X)) -> isPal#(X)
p51: top#(mark(X)) -> top#(proper(X))
p52: top#(mark(X)) -> proper#(X)
p53: top#(ok(X)) -> top#(active(X))
p54: top#(ok(X)) -> active#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p51, p53}
  {p20, p22, p24}
  {p29, p30, p32, p33, p35, p37, p39, p41, p43}
  {p25, p26, p44}
  {p47}
  {p27, p45}
  {p46}
  {p48}
  {p50}
  {p49}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(X))

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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, r41, r42, r43, r44, r45, r46

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          top#_A(x1) = x1 + (0,1)
          ok_A(x1) = x1
          active_A(x1) = x1
          mark_A(x1) = x1 + (0,2)
          proper_A(x1) = x1
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (12,15)
          and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,3)
          isList_A(x1) = ((1,0),(1,0)) x1 + (6,9)
          isNeList_A(x1) = ((1,0),(0,0)) x1 + (4,6)
          isQid_A(x1) = ((1,0),(0,0)) x1 + (3,4)
          isNePal_A(x1) = ((1,0),(1,1)) x1 + (4,7)
          isPal_A(x1) = ((1,0),(0,0)) x1 + (5,9)
          nil_A() = (3,4)
          tt_A() = (2,1)
          a_A() = (3,4)
          e_A() = (0,3)
          i_A() = (3,4)
          o_A() = (1,3)
          u_A() = (3,4)
  
    precedence:
    
      isNeList = isQid = a > nil > e = i = o > ok = active = __ = and = isList = isNePal = isPal = tt = u > mark > top# = proper
    
    partial status:
  
      pi(top#) = [1]
      pi(ok) = []
      pi(active) = []
      pi(mark) = []
      pi(proper) = [1]
      pi(__) = []
      pi(and) = []
      pi(isList) = []
      pi(isNeList) = []
      pi(isQid) = []
      pi(isNePal) = []
      pi(isPal) = []
      pi(nil) = []
      pi(tt) = []
      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: top#(ok(X)) -> top#(active(X))

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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, r40, r41, r42, r43, r44, r45, r46

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: lexicographic order
        interpretations:
          top#_A(x1) = x1 + (0,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (7,2)
          active_A(x1) = ((1,0),(0,0)) x1 + (1,4)
          ___A(x1,x2) = ((1,0),(0,0)) x1 + (6,2)
          mark_A(x1) = (0,4)
          and_A(x1,x2) = ((1,0),(0,0)) x2 + (2,4)
          isList_A(x1) = x1 + (1,12)
          isNeList_A(x1) = ((1,0),(1,1)) x1 + (3,3)
          isQid_A(x1) = ((1,0),(0,0)) x1 + (0,2)
          isNePal_A(x1) = ((1,0),(1,0)) x1 + (8,0)
          isPal_A(x1) = ((1,0),(0,0)) x1 + (0,7)
          nil_A() = (0,5)
          tt_A() = (0,1)
          a_A() = (0,5)
          e_A() = (1,5)
          i_A() = (1,5)
          o_A() = (1,5)
          u_A() = (0,5)
  
    precedence:
    
      isNePal = isPal = a > ok = __ = isQid > top# = active = and = tt = e = i > mark = isList = isNeList = nil = o = u
    
    partial status:
  
      pi(top#) = [1]
      pi(ok) = []
      pi(active) = []
      pi(__) = []
      pi(mark) = []
      pi(and) = []
      pi(isList) = []
      pi(isNeList) = [1]
      pi(isQid) = []
      pi(isNePal) = []
      pi(isPal) = []
      pi(nil) = []
      pi(tt) = []
      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: active#(and(X1,X2)) -> active#(X1)
p2: active#(__(X1,X2)) -> active#(X2)
p3: active#(__(X1,X2)) -> active#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          active#_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          and_A(x1,x2) = x1 + x2 + (2,2)
          ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (1,2)
  
    precedence:
    
      active# = and = __
    
    partial status:
  
      pi(active#) = []
      pi(and) = [2]
      pi(__) = [2]

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: active#(and(X1,X2)) -> active#(X1)
p2: active#(__(X1,X2)) -> active#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: active#(and(X1,X2)) -> active#(X1)
p2: active#(__(X1,X2)) -> active#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          active#_A(x1) = ((1,0),(0,0)) x1
          and_A(x1,x2) = ((1,0),(0,0)) x1 + x2
          ___A(x1,x2) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      and = __ > active#
    
    partial status:
  
      pi(active#) = []
      pi(and) = [2]
      pi(__) = []

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: active#(and(X1,X2)) -> active#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: active#(and(X1,X2)) -> active#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          active#_A(x1) = ((1,0),(1,1)) x1
          and_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (1,1)
  
    precedence:
    
      active# > and
    
    partial status:
  
      pi(active#) = [1]
      pi(and) = [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: proper#(isPal(X)) -> proper#(X)
p2: proper#(isNePal(X)) -> proper#(X)
p3: proper#(isQid(X)) -> proper#(X)
p4: proper#(isNeList(X)) -> proper#(X)
p5: proper#(isList(X)) -> proper#(X)
p6: proper#(and(X1,X2)) -> proper#(X2)
p7: proper#(and(X1,X2)) -> proper#(X1)
p8: proper#(__(X1,X2)) -> proper#(X2)
p9: proper#(__(X1,X2)) -> proper#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(1,1)) x1 + (1,2)
          isPal_A(x1) = x1 + (2,1)
          isNePal_A(x1) = x1 + (2,3)
          isQid_A(x1) = x1 + (2,1)
          isNeList_A(x1) = x1 + (2,3)
          isList_A(x1) = x1 + (2,3)
          and_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (2,3)
          ___A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (2,1)
  
    precedence:
    
      isNePal > isPal = isQid > isNeList = __ > proper# = and > isList
    
    partial status:
  
      pi(proper#) = [1]
      pi(isPal) = [1]
      pi(isNePal) = [1]
      pi(isQid) = []
      pi(isNeList) = [1]
      pi(isList) = [1]
      pi(and) = [2]
      pi(__) = [2]

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: proper#(isPal(X)) -> proper#(X)
p2: proper#(isNePal(X)) -> proper#(X)
p3: proper#(isNeList(X)) -> proper#(X)
p4: proper#(isList(X)) -> proper#(X)
p5: proper#(and(X1,X2)) -> proper#(X2)
p6: proper#(and(X1,X2)) -> proper#(X1)
p7: proper#(__(X1,X2)) -> proper#(X2)
p8: proper#(__(X1,X2)) -> proper#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: proper#(isPal(X)) -> proper#(X)
p2: proper#(__(X1,X2)) -> proper#(X1)
p3: proper#(__(X1,X2)) -> proper#(X2)
p4: proper#(and(X1,X2)) -> proper#(X1)
p5: proper#(and(X1,X2)) -> proper#(X2)
p6: proper#(isList(X)) -> proper#(X)
p7: proper#(isNeList(X)) -> proper#(X)
p8: proper#(isNePal(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(1,0)) x1
          isPal_A(x1) = x1 + (1,1)
          ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (1,1)
          and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,1)
          isList_A(x1) = x1 + (1,1)
          isNeList_A(x1) = x1 + (1,1)
          isNePal_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isPal = __ = and = isNePal > proper# = isList = isNeList
    
    partial status:
  
      pi(proper#) = []
      pi(isPal) = [1]
      pi(__) = [2]
      pi(and) = [2]
      pi(isList) = [1]
      pi(isNeList) = [1]
      pi(isNePal) = []

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: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(__(X1,X2)) -> proper#(X2)
p3: proper#(and(X1,X2)) -> proper#(X1)
p4: proper#(and(X1,X2)) -> proper#(X2)
p5: proper#(isList(X)) -> proper#(X)
p6: proper#(isNeList(X)) -> proper#(X)
p7: proper#(isNePal(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(isNePal(X)) -> proper#(X)
p3: proper#(isNeList(X)) -> proper#(X)
p4: proper#(isList(X)) -> proper#(X)
p5: proper#(and(X1,X2)) -> proper#(X2)
p6: proper#(and(X1,X2)) -> proper#(X1)
p7: proper#(__(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(1,1)) x1 + (1,1)
          ___A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (2,2)
          isNePal_A(x1) = x1 + (2,2)
          isNeList_A(x1) = x1 + (2,2)
          isList_A(x1) = ((1,0),(1,1)) x1 + (2,2)
          and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (2,2)
  
    precedence:
    
      proper# = __ = isNePal = isNeList = isList = and
    
    partial status:
  
      pi(proper#) = [1]
      pi(__) = [1]
      pi(isNePal) = [1]
      pi(isNeList) = [1]
      pi(isList) = []
      pi(and) = [2]

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: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(isNePal(X)) -> proper#(X)
p3: proper#(isNeList(X)) -> proper#(X)
p4: proper#(isList(X)) -> proper#(X)
p5: proper#(and(X1,X2)) -> proper#(X2)
p6: proper#(and(X1,X2)) -> proper#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(and(X1,X2)) -> proper#(X1)
p3: proper#(and(X1,X2)) -> proper#(X2)
p4: proper#(isList(X)) -> proper#(X)
p5: proper#(isNeList(X)) -> proper#(X)
p6: proper#(isNePal(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          ___A(x1,x2) = x1 + (2,2)
          and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (2,2)
          isList_A(x1) = x1 + (2,2)
          isNeList_A(x1) = ((1,0),(0,0)) x1 + (2,2)
          isNePal_A(x1) = ((1,0),(0,0)) x1 + (2,2)
  
    precedence:
    
      proper# = isNePal > __ > and = isList = isNeList
    
    partial status:
  
      pi(proper#) = []
      pi(__) = []
      pi(and) = [2]
      pi(isList) = [1]
      pi(isNeList) = []
      pi(isNePal) = []

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: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(and(X1,X2)) -> proper#(X1)
p3: proper#(and(X1,X2)) -> proper#(X2)
p4: proper#(isNeList(X)) -> proper#(X)
p5: proper#(isNePal(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

p1: proper#(__(X1,X2)) -> proper#(X1)
p2: proper#(isNePal(X)) -> proper#(X)
p3: proper#(isNeList(X)) -> proper#(X)
p4: proper#(and(X1,X2)) -> proper#(X2)
p5: proper#(and(X1,X2)) -> proper#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(0,0)) x1 + (2,1)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (3,2)
          isNePal_A(x1) = ((1,0),(0,0)) x1 + (1,2)
          isNeList_A(x1) = x1 + (3,2)
          and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (3,2)
  
    precedence:
    
      proper# > __ = isNePal = isNeList = and
    
    partial status:
  
      pi(proper#) = []
      pi(__) = [2]
      pi(isNePal) = []
      pi(isNeList) = [1]
      pi(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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(isNeList(X)) -> proper#(X)
p3: proper#(and(X1,X2)) -> proper#(X2)
p4: proper#(and(X1,X2)) -> proper#(X1)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(and(X1,X2)) -> proper#(X1)
p3: proper#(and(X1,X2)) -> proper#(X2)
p4: proper#(isNeList(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(0,0)) x1
          isNePal_A(x1) = ((1,0),(1,0)) x1 + (1,1)
          and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,1)
          isNeList_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isNePal = isNeList > proper# = and
    
    partial status:
  
      pi(proper#) = []
      pi(isNePal) = []
      pi(and) = [2]
      pi(isNeList) = []

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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(and(X1,X2)) -> proper#(X2)
p3: proper#(isNeList(X)) -> proper#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(isNeList(X)) -> proper#(X)
p3: proper#(and(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = x1 + (1,2)
          isNePal_A(x1) = ((1,0),(1,1)) x1 + (2,3)
          isNeList_A(x1) = x1 + (2,1)
          and_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (2,3)
  
    precedence:
    
      isNePal > isNeList > proper# = and
    
    partial status:
  
      pi(proper#) = [1]
      pi(isNePal) = []
      pi(isNeList) = [1]
      pi(and) = [1]

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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(and(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: proper#(isNePal(X)) -> proper#(X)
p2: proper#(and(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(1,0)) x1 + (1,2)
          isNePal_A(x1) = ((1,0),(0,0)) x1 + (2,1)
          and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,1)
  
    precedence:
    
      proper# = isNePal = and
    
    partial status:
  
      pi(proper#) = []
      pi(isNePal) = []
      pi(and) = [1]

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: proper#(and(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: proper#(and(X1,X2)) -> proper#(X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          proper#_A(x1) = ((1,0),(1,1)) x1
          and_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,1)
  
    precedence:
    
      proper# = and
    
    partial status:
  
      pi(proper#) = [1]
      pi(and) = [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: __#(mark(X1),X2) -> __#(X1,X2)
p2: __#(ok(X1),ok(X2)) -> __#(X1,X2)
p3: __#(X1,mark(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          __#_A(x1,x2) = x2 + (1,1)
          mark_A(x1) = ((1,0),(1,1)) x1 + (2,2)
          ok_A(x1) = ((1,0),(1,1)) x1 + (2,2)
  
    precedence:
    
      __# = mark = ok
    
    partial status:
  
      pi(__#) = [2]
      pi(mark) = [1]
      pi(ok) = [1]

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: __#(mark(X1),X2) -> __#(X1,X2)
p2: __#(ok(X1),ok(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: __#(mark(X1),X2) -> __#(X1,X2)
p2: __#(ok(X1),ok(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          __#_A(x1,x2) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (2,2)
          mark_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,3)
  
    precedence:
    
      __# = mark = ok
    
    partial status:
  
      pi(__#) = []
      pi(mark) = []
      pi(ok) = []

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: __#(ok(X1),ok(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: __#(ok(X1),ok(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          __#_A(x1,x2) = x1
          ok_A(x1) = x1 + (1,1)
  
    precedence:
    
      ok > __#
    
    partial status:
  
      pi(__#) = []
      pi(ok) = [1]

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: isNeList#(ok(X)) -> isNeList#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          isNeList#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isNeList# = ok
    
    partial status:
  
      pi(isNeList#) = []
      pi(ok) = []

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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(ok(X1),ok(X2)) -> and#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          and#_A(x1,x2) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (2,2)
          mark_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,3)
  
    precedence:
    
      and# = mark = ok
    
    partial status:
  
      pi(and#) = []
      pi(mark) = []
      pi(ok) = []

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: and#(ok(X1),ok(X2)) -> and#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: and#(ok(X1),ok(X2)) -> and#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          and#_A(x1,x2) = x1
          ok_A(x1) = x1 + (1,1)
  
    precedence:
    
      ok > and#
    
    partial status:
  
      pi(and#) = []
      pi(ok) = [1]

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: isList#(ok(X)) -> isList#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          isList#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isList# = ok
    
    partial status:
  
      pi(isList#) = []
      pi(ok) = []

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: isQid#(ok(X)) -> isQid#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          isQid#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isQid# = ok
    
    partial status:
  
      pi(isQid#) = []
      pi(ok) = []

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: isPal#(ok(X)) -> isPal#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          isPal#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isPal# = ok
    
    partial status:
  
      pi(isPal#) = []
      pi(ok) = []

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: isNePal#(ok(X)) -> isNePal#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: active(__(X1,X2)) -> __(active(X1),X2)
r21: active(__(X1,X2)) -> __(X1,active(X2))
r22: active(and(X1,X2)) -> and(active(X1),X2)
r23: __(mark(X1),X2) -> mark(__(X1,X2))
r24: __(X1,mark(X2)) -> mark(__(X1,X2))
r25: and(mark(X1),X2) -> mark(and(X1,X2))
r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
r27: proper(nil()) -> ok(nil())
r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r29: proper(tt()) -> ok(tt())
r30: proper(isList(X)) -> isList(proper(X))
r31: proper(isNeList(X)) -> isNeList(proper(X))
r32: proper(isQid(X)) -> isQid(proper(X))
r33: proper(isNePal(X)) -> isNePal(proper(X))
r34: proper(isPal(X)) -> isPal(proper(X))
r35: proper(a()) -> ok(a())
r36: proper(e()) -> ok(e())
r37: proper(i()) -> ok(i())
r38: proper(o()) -> ok(o())
r39: proper(u()) -> ok(u())
r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r42: isList(ok(X)) -> ok(isList(X))
r43: isNeList(ok(X)) -> ok(isNeList(X))
r44: isQid(ok(X)) -> ok(isQid(X))
r45: isNePal(ok(X)) -> ok(isNePal(X))
r46: isPal(ok(X)) -> ok(isPal(X))
r47: top(mark(X)) -> top(proper(X))
r48: top(ok(X)) -> top(active(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: lexicographic order
        interpretations:
          isNePal#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          ok_A(x1) = ((1,0),(0,0)) x1 + (1,1)
  
    precedence:
    
      isNePal# = ok
    
    partial status:
  
      pi(isNePal#) = []
      pi(ok) = []

The next rules are strictly ordered:

  p1

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