YES

We show the termination of the TRS R:

  active(eq(|0|(),|0|())) -> mark(true())
  active(eq(s(X),s(Y))) -> mark(eq(X,Y))
  active(eq(X,Y)) -> mark(false())
  active(inf(X)) -> mark(cons(X,inf(s(X))))
  active(take(|0|(),X)) -> mark(nil())
  active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
  active(length(nil())) -> mark(|0|())
  active(length(cons(X,L))) -> mark(s(length(L)))
  mark(eq(X1,X2)) -> active(eq(X1,X2))
  mark(|0|()) -> active(|0|())
  mark(true()) -> active(true())
  mark(s(X)) -> active(s(X))
  mark(false()) -> active(false())
  mark(inf(X)) -> active(inf(mark(X)))
  mark(cons(X1,X2)) -> active(cons(X1,X2))
  mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  mark(length(X)) -> active(length(mark(X)))
  eq(mark(X1),X2) -> eq(X1,X2)
  eq(X1,mark(X2)) -> eq(X1,X2)
  eq(active(X1),X2) -> eq(X1,X2)
  eq(X1,active(X2)) -> eq(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  inf(mark(X)) -> inf(X)
  inf(active(X)) -> inf(X)
  cons(mark(X1),X2) -> cons(X1,X2)
  cons(X1,mark(X2)) -> cons(X1,X2)
  cons(active(X1),X2) -> cons(X1,X2)
  cons(X1,active(X2)) -> cons(X1,X2)
  take(mark(X1),X2) -> take(X1,X2)
  take(X1,mark(X2)) -> take(X1,X2)
  take(active(X1),X2) -> take(X1,X2)
  take(X1,active(X2)) -> take(X1,X2)
  length(mark(X)) -> length(X)
  length(active(X)) -> length(X)

-- SCC decomposition.

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

p1: active#(eq(|0|(),|0|())) -> mark#(true())
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: active#(eq(s(X),s(Y))) -> eq#(X,Y)
p4: active#(eq(X,Y)) -> mark#(false())
p5: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p6: active#(inf(X)) -> cons#(X,inf(s(X)))
p7: active#(inf(X)) -> inf#(s(X))
p8: active#(inf(X)) -> s#(X)
p9: active#(take(|0|(),X)) -> mark#(nil())
p10: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p11: active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
p12: active#(take(s(X),cons(Y,L))) -> take#(X,L)
p13: active#(length(nil())) -> mark#(|0|())
p14: active#(length(cons(X,L))) -> mark#(s(length(L)))
p15: active#(length(cons(X,L))) -> s#(length(L))
p16: active#(length(cons(X,L))) -> length#(L)
p17: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p18: mark#(|0|()) -> active#(|0|())
p19: mark#(true()) -> active#(true())
p20: mark#(s(X)) -> active#(s(X))
p21: mark#(false()) -> active#(false())
p22: mark#(inf(X)) -> active#(inf(mark(X)))
p23: mark#(inf(X)) -> inf#(mark(X))
p24: mark#(inf(X)) -> mark#(X)
p25: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p26: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p27: mark#(take(X1,X2)) -> take#(mark(X1),mark(X2))
p28: mark#(take(X1,X2)) -> mark#(X1)
p29: mark#(take(X1,X2)) -> mark#(X2)
p30: mark#(nil()) -> active#(nil())
p31: mark#(length(X)) -> active#(length(mark(X)))
p32: mark#(length(X)) -> length#(mark(X))
p33: mark#(length(X)) -> mark#(X)
p34: eq#(mark(X1),X2) -> eq#(X1,X2)
p35: eq#(X1,mark(X2)) -> eq#(X1,X2)
p36: eq#(active(X1),X2) -> eq#(X1,X2)
p37: eq#(X1,active(X2)) -> eq#(X1,X2)
p38: s#(mark(X)) -> s#(X)
p39: s#(active(X)) -> s#(X)
p40: inf#(mark(X)) -> inf#(X)
p41: inf#(active(X)) -> inf#(X)
p42: cons#(mark(X1),X2) -> cons#(X1,X2)
p43: cons#(X1,mark(X2)) -> cons#(X1,X2)
p44: cons#(active(X1),X2) -> cons#(X1,X2)
p45: cons#(X1,active(X2)) -> cons#(X1,X2)
p46: take#(mark(X1),X2) -> take#(X1,X2)
p47: take#(X1,mark(X2)) -> take#(X1,X2)
p48: take#(active(X1),X2) -> take#(X1,X2)
p49: take#(X1,active(X2)) -> take#(X1,X2)
p50: length#(mark(X)) -> length#(X)
p51: length#(active(X)) -> length#(X)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The estimated dependency graph contains the following SCCs:

  {p2, p5, p10, p14, p17, p20, p22, p24, p25, p26, p28, p29, p31, p33}
  {p34, p35, p36, p37}
  {p42, p43, p44, p45}
  {p40, p41}
  {p38, p39}
  {p46, p47, p48, p49}
  {p50, p51}


-- Reduction pair.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(length(cons(X,L))) -> mark#(s(length(L)))
p3: mark#(length(X)) -> mark#(X)
p4: mark#(take(X1,X2)) -> mark#(X2)
p5: mark#(take(X1,X2)) -> mark#(X1)
p6: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p7: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p8: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p9: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p10: mark#(inf(X)) -> mark#(X)
p11: mark#(inf(X)) -> active#(inf(mark(X)))
p12: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p13: mark#(s(X)) -> active#(s(X))
p14: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{1, x1 - 7}
          length_A(x1) = x1 + 20
          active#_A(x1) = max{0, x1 - 7}
          mark_A(x1) = x1
          cons_A(x1,x2) = max{x1 + 9, x2 - 3}
          s_A(x1) = max{0, x1 - 3}
          take_A(x1,x2) = max{x1 + 21, x2 + 20}
          inf_A(x1) = max{28, x1 + 17}
          eq_A(x1,x2) = 8
          active_A(x1) = x1
          |0|_A = 9
          true_A = 8
          false_A = 7
          nil_A = 8
    
      precedence:
      
        take > true > |0| > false = nil > cons > mark# = length = active# = mark = s = inf = eq = active
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(cons) = []
        pi(s) = []
        pi(take) = []
        pi(inf) = []
        pi(eq) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 24
          length_A(x1) = 115
          active#_A(x1) = 24
          mark_A(x1) = 115
          cons_A(x1,x2) = 107
          s_A(x1) = 103
          take_A(x1,x2) = 111
          inf_A(x1) = 594
          eq_A(x1,x2) = 124
          active_A(x1) = 115
          |0|_A = 40
          true_A = 120
          false_A = 122
          nil_A = 41
    
      precedence:
      
        eq > length = mark = inf = active > cons > mark# = active# = s = take = |0| = true = false = nil
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(cons) = []
        pi(s) = []
        pi(take) = []
        pi(inf) = []
        pi(eq) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    

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#(length(X)) -> active#(length(mark(X)))
p2: active#(length(cons(X,L))) -> mark#(s(length(L)))
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(take(X1,X2)) -> mark#(X1)
p5: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p6: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p7: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p8: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p9: mark#(inf(X)) -> mark#(X)
p10: mark#(inf(X)) -> active#(inf(mark(X)))
p11: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p12: mark#(s(X)) -> active#(s(X))
p13: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(s(X)) -> active#(s(X))
p6: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p7: mark#(inf(X)) -> active#(inf(mark(X)))
p8: active#(length(cons(X,L))) -> mark#(s(length(L)))
p9: mark#(inf(X)) -> mark#(X)
p10: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p11: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p12: mark#(take(X1,X2)) -> mark#(X1)
p13: mark#(take(X1,X2)) -> mark#(X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1
          length_A(x1) = x1 + 10
          active#_A(x1) = max{1, x1}
          mark_A(x1) = x1
          eq_A(x1,x2) = 7
          s_A(x1) = max{4, x1}
          inf_A(x1) = max{8, x1 + 3}
          cons_A(x1,x2) = max{8, x1 + 2, x2}
          take_A(x1,x2) = max{x1 + 9, x2 + 9}
          active_A(x1) = max{4, x1}
          |0|_A = 14
          true_A = 4
          false_A = 5
          nil_A = 4
    
      precedence:
      
        length > s = |0| > inf > take > mark = eq = active > true = false = nil > mark# = active# = cons
      
      partial status:
    
        pi(mark#) = [1]
        pi(length) = []
        pi(active#) = [1]
        pi(mark) = [1]
        pi(eq) = []
        pi(s) = []
        pi(inf) = []
        pi(cons) = []
        pi(take) = []
        pi(active) = [1]
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 78
          length_A(x1) = 136
          active#_A(x1) = 78
          mark_A(x1) = max{143, x1 + 7}
          eq_A(x1,x2) = 136
          s_A(x1) = 136
          inf_A(x1) = 162
          cons_A(x1,x2) = 163
          take_A(x1,x2) = 173
          active_A(x1) = max{143, x1 - 2}
          |0|_A = 171
          true_A = 136
          false_A = 136
          nil_A = 174
    
      precedence:
      
        false > eq = |0| = nil > inf = take > mark# = active# = cons > mark = active = true > length > s
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(eq) = []
        pi(s) = []
        pi(inf) = []
        pi(cons) = []
        pi(take) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p8

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(s(X)) -> active#(s(X))
p6: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p7: mark#(inf(X)) -> active#(inf(mark(X)))
p8: mark#(inf(X)) -> mark#(X)
p9: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p10: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p11: mark#(take(X1,X2)) -> mark#(X1)
p12: mark#(take(X1,X2)) -> mark#(X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(take(X1,X2)) -> mark#(X1)
p5: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p6: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p7: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p8: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p9: mark#(inf(X)) -> mark#(X)
p10: mark#(inf(X)) -> active#(inf(mark(X)))
p11: mark#(s(X)) -> active#(s(X))
p12: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{244, x1 + 93}
          length_A(x1) = 81
          active#_A(x1) = max{223, x1 + 34}
          mark_A(x1) = max{220, x1 + 7}
          take_A(x1,x2) = max{346, x1 + 93, x2 + 127}
          s_A(x1) = x1 + 131
          cons_A(x1,x2) = max{345, x1 + 118}
          inf_A(x1) = max{466, x1 + 212}
          eq_A(x1,x2) = x2 + 222
          active_A(x1) = max{220, x1}
          |0|_A = 73
          true_A = 214
          false_A = 214
          nil_A = 74
    
      precedence:
      
        mark = inf = active = nil > length > active# = take = s > cons = false > true > eq = |0| > mark#
      
      partial status:
    
        pi(mark#) = [1]
        pi(length) = []
        pi(active#) = [1]
        pi(mark) = []
        pi(take) = [2]
        pi(s) = [1]
        pi(cons) = []
        pi(inf) = []
        pi(eq) = [2]
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 10
          length_A(x1) = 109
          active#_A(x1) = 10
          mark_A(x1) = 108
          take_A(x1,x2) = 20
          s_A(x1) = 145
          cons_A(x1,x2) = 93
          inf_A(x1) = 108
          eq_A(x1,x2) = 1
          active_A(x1) = 108
          |0|_A = 134
          true_A = 143
          false_A = 117
          nil_A = 97
    
      precedence:
      
        length > cons > eq > take = false > mark = s = active = nil > inf = |0| > mark# = active# = true
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(take) = []
        pi(s) = []
        pi(cons) = []
        pi(inf) = []
        pi(eq) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p5, p11

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(take(X1,X2)) -> mark#(X1)
p5: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p6: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p7: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p8: mark#(inf(X)) -> mark#(X)
p9: mark#(inf(X)) -> active#(inf(mark(X)))
p10: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(inf(X)) -> active#(inf(mark(X)))
p6: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p7: mark#(inf(X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p9: mark#(take(X1,X2)) -> mark#(X1)
p10: mark#(take(X1,X2)) -> mark#(X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{29, x1 + 11}
          length_A(x1) = 0
          active#_A(x1) = max{10, x1 + 7}
          mark_A(x1) = max{13, x1 + 2}
          eq_A(x1,x2) = max{x1 + 30, x2 + 30}
          s_A(x1) = x1 + 11
          inf_A(x1) = max{29, x1}
          cons_A(x1,x2) = 18
          take_A(x1,x2) = max{44, x1 + 21, x2 + 33}
          active_A(x1) = max{13, x1}
          |0|_A = 11
          true_A = 11
          false_A = 11
          nil_A = 28
    
      precedence:
      
        mark = inf = take = active = true = false > mark# = eq > active# = nil > |0| > length = s = cons
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = [1]
        pi(mark) = []
        pi(eq) = [2]
        pi(s) = [1]
        pi(inf) = []
        pi(cons) = []
        pi(take) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 2
          length_A(x1) = 125
          active#_A(x1) = 2
          mark_A(x1) = 78
          eq_A(x1,x2) = 12
          s_A(x1) = 43
          inf_A(x1) = 93
          cons_A(x1,x2) = 103
          take_A(x1,x2) = 93
          active_A(x1) = 78
          |0|_A = 21
          true_A = 21
          false_A = 21
          nil_A = 13
    
      precedence:
      
        length > cons > mark# = active# = mark = eq = inf = take = active = true = false = nil > s = |0|
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(eq) = []
        pi(s) = []
        pi(inf) = []
        pi(cons) = []
        pi(take) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p9, p10

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(inf(X)) -> active#(inf(mark(X)))
p6: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p7: mark#(inf(X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> active#(cons(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(take(s(X),cons(Y,L))) -> mark#(cons(Y,take(X,L)))
p3: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(inf(X)) -> mark#(X)
p6: mark#(inf(X)) -> active#(inf(mark(X)))
p7: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p8: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 48
          length_A(x1) = 4
          active#_A(x1) = max{45, x1 + 44}
          mark_A(x1) = x1 + 24
          take_A(x1,x2) = 20
          s_A(x1) = max{4, x1}
          cons_A(x1,x2) = 4
          inf_A(x1) = 4
          eq_A(x1,x2) = 4
          active_A(x1) = max{28, x1 + 10}
          |0|_A = 4
          true_A = 4
          false_A = 4
          nil_A = 5
    
      precedence:
      
        cons > inf = true > length = mark = active > s > mark# = active# = take = nil > eq = |0| = false
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(take) = []
        pi(s) = [1]
        pi(cons) = []
        pi(inf) = []
        pi(eq) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 106
          length_A(x1) = 83
          active#_A(x1) = 106
          mark_A(x1) = 82
          take_A(x1,x2) = 63
          s_A(x1) = max{176, x1 + 174}
          cons_A(x1,x2) = 71
          inf_A(x1) = 89
          eq_A(x1,x2) = 82
          active_A(x1) = 82
          |0|_A = 158
          true_A = 86
          false_A = 86
          nil_A = 144
    
      precedence:
      
        |0| > mark# = length = active# = true = false = nil > mark = active > take = s = cons = inf = eq
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(take) = []
        pi(s) = [1]
        pi(cons) = []
        pi(inf) = []
        pi(eq) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(nil) = []
    

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: mark#(length(X)) -> active#(length(mark(X)))
p2: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p3: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p4: mark#(inf(X)) -> mark#(X)
p5: mark#(inf(X)) -> active#(inf(mark(X)))
p6: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p7: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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: mark#(length(X)) -> active#(length(mark(X)))
p2: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p3: mark#(eq(X1,X2)) -> active#(eq(X1,X2))
p4: active#(inf(X)) -> mark#(cons(X,inf(s(X))))
p5: mark#(inf(X)) -> active#(inf(mark(X)))
p6: mark#(inf(X)) -> mark#(X)
p7: mark#(cons(X1,X2)) -> active#(cons(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{61, x1 + 43}
          length_A(x1) = 62
          active#_A(x1) = max{61, x1 + 7}
          mark_A(x1) = max{4, x1}
          eq_A(x1,x2) = 17
          s_A(x1) = max{27, x1}
          inf_A(x1) = max{134, x1 + 62}
          cons_A(x1,x2) = x1 + 19
          active_A(x1) = max{15, x1}
          |0|_A = 15
          true_A = 15
          false_A = 16
          take_A(x1,x2) = max{21, x2 + 17}
          nil_A = 16
    
      precedence:
      
        length = mark = eq = active = false > inf = cons = |0| = true > mark# = active# = s = take = nil
      
      partial status:
    
        pi(mark#) = [1]
        pi(length) = []
        pi(active#) = [1]
        pi(mark) = []
        pi(eq) = []
        pi(s) = []
        pi(inf) = [1]
        pi(cons) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(take) = [2]
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{148, x1 + 66}
          length_A(x1) = 140
          active#_A(x1) = max{237, x1 + 22}
          mark_A(x1) = 67
          eq_A(x1,x2) = 171
          s_A(x1) = 238
          inf_A(x1) = 147
          cons_A(x1,x2) = 127
          active_A(x1) = 67
          |0|_A = 292
          true_A = 370
          false_A = 249
          take_A(x1,x2) = 214
          nil_A = 214
    
      precedence:
      
        true = take > mark# = active# = false = nil > length = eq = s = inf = cons > mark = active = |0|
      
      partial status:
    
        pi(mark#) = []
        pi(length) = []
        pi(active#) = []
        pi(mark) = []
        pi(eq) = []
        pi(s) = []
        pi(inf) = []
        pi(cons) = []
        pi(active) = []
        pi(|0|) = []
        pi(true) = []
        pi(false) = []
        pi(take) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p1, p4, p5, p6, p7

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p2: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(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#(eq(s(X),s(Y))) -> mark#(eq(X,Y))
p2: mark#(eq(X1,X2)) -> active#(eq(X1,X2))

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  r19, r20, r21, r22

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{10, x1 + 3}
          eq_A(x1,x2) = max{x1 + 6, x2 + 9}
          s_A(x1) = max{4, x1 + 3}
          mark#_A(x1) = max{7, x1 + 6}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        active# = eq = s = mark# = mark = active
      
      partial status:
    
        pi(active#) = [1]
        pi(eq) = [1, 2]
        pi(s) = [1]
        pi(mark#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{16, x1 + 6}
          eq_A(x1,x2) = max{9, x1 + 1, x2 - 10}
          s_A(x1) = max{14, x1 + 3}
          mark#_A(x1) = x1 + 7
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        active# = eq = s = mark# = mark = active
      
      partial status:
    
        pi(active#) = []
        pi(eq) = []
        pi(s) = [1]
        pi(mark#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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: eq#(mark(X1),X2) -> eq#(X1,X2)
p2: eq#(X1,active(X2)) -> eq#(X1,X2)
p3: eq#(active(X1),X2) -> eq#(X1,X2)
p4: eq#(X1,mark(X2)) -> eq#(X1,X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        eq# = mark = active
      
      partial status:
    
        pi(eq#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{x1 + 1, x2 - 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        eq# = mark = active
      
      partial status:
    
        pi(eq#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(X1,mark(X2)) -> cons#(X1,X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          cons#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        cons# = mark = active
      
      partial status:
    
        pi(cons#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          cons#_A(x1,x2) = max{x1 + 1, x2 - 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        cons# = mark = active
      
      partial status:
    
        pi(cons#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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: inf#(mark(X)) -> inf#(X)
p2: inf#(active(X)) -> inf#(X)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inf#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > inf#
      
      partial status:
    
        pi(inf#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inf#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        inf# = mark = active
      
      partial status:
    
        pi(inf#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          s#_A(x1) = max{6, x1 + 4}
          mark_A(x1) = max{4, x1 + 3}
          active_A(x1) = max{2, x1 + 1}
    
      precedence:
      
        s# = mark = active
      
      partial status:
    
        pi(s#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          s#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        s# = mark = active
      
      partial status:
    
        pi(s#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(X1,active(X2)) -> take#(X1,X2)
p3: take#(active(X1),X2) -> take#(X1,X2)
p4: take#(X1,mark(X2)) -> take#(X1,X2)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          take#_A(x1,x2) = max{4, x1 + 1, x2 + 3}
          mark_A(x1) = max{3, x1 + 2}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        take# = mark = active
      
      partial status:
    
        pi(take#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          take#_A(x1,x2) = max{x1 + 1, x2 + 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        take# = mark = active
      
      partial status:
    
        pi(take#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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: length#(mark(X)) -> length#(X)
p2: length#(active(X)) -> length#(X)

and R consists of:

r1: active(eq(|0|(),|0|())) -> mark(true())
r2: active(eq(s(X),s(Y))) -> mark(eq(X,Y))
r3: active(eq(X,Y)) -> mark(false())
r4: active(inf(X)) -> mark(cons(X,inf(s(X))))
r5: active(take(|0|(),X)) -> mark(nil())
r6: active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
r7: active(length(nil())) -> mark(|0|())
r8: active(length(cons(X,L))) -> mark(s(length(L)))
r9: mark(eq(X1,X2)) -> active(eq(X1,X2))
r10: mark(|0|()) -> active(|0|())
r11: mark(true()) -> active(true())
r12: mark(s(X)) -> active(s(X))
r13: mark(false()) -> active(false())
r14: mark(inf(X)) -> active(inf(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(X1,X2))
r16: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r17: mark(nil()) -> active(nil())
r18: mark(length(X)) -> active(length(mark(X)))
r19: eq(mark(X1),X2) -> eq(X1,X2)
r20: eq(X1,mark(X2)) -> eq(X1,X2)
r21: eq(active(X1),X2) -> eq(X1,X2)
r22: eq(X1,active(X2)) -> eq(X1,X2)
r23: s(mark(X)) -> s(X)
r24: s(active(X)) -> s(X)
r25: inf(mark(X)) -> inf(X)
r26: inf(active(X)) -> inf(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: take(mark(X1),X2) -> take(X1,X2)
r32: take(X1,mark(X2)) -> take(X1,X2)
r33: take(active(X1),X2) -> take(X1,X2)
r34: take(X1,active(X2)) -> take(X1,X2)
r35: length(mark(X)) -> length(X)
r36: length(active(X)) -> length(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          length#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > length#
      
      partial status:
    
        pi(length#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          length#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        length# = mark = active
      
      partial status:
    
        pi(length#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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