YES

We show the termination of the TRS R:

  active(fst(|0|(),Z)) -> mark(nil())
  active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
  active(from(X)) -> mark(cons(X,from(s(X))))
  active(add(|0|(),X)) -> mark(X)
  active(add(s(X),Y)) -> mark(s(add(X,Y)))
  active(len(nil())) -> mark(|0|())
  active(len(cons(X,Z))) -> mark(s(len(Z)))
  mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
  mark(|0|()) -> active(|0|())
  mark(nil()) -> active(nil())
  mark(s(X)) -> active(s(X))
  mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
  mark(from(X)) -> active(from(mark(X)))
  mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
  mark(len(X)) -> active(len(mark(X)))
  fst(mark(X1),X2) -> fst(X1,X2)
  fst(X1,mark(X2)) -> fst(X1,X2)
  fst(active(X1),X2) -> fst(X1,X2)
  fst(X1,active(X2)) -> fst(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(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)
  from(mark(X)) -> from(X)
  from(active(X)) -> from(X)
  add(mark(X1),X2) -> add(X1,X2)
  add(X1,mark(X2)) -> add(X1,X2)
  add(active(X1),X2) -> add(X1,X2)
  add(X1,active(X2)) -> add(X1,X2)
  len(mark(X)) -> len(X)
  len(active(X)) -> len(X)

-- SCC decomposition.

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

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

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(X)

The estimated dependency graph contains the following SCCs:

  {p2, p5, p9, p10, p14, p17, p19, p20, p23, p24, p26, p27, p29, p30, p32, p33, p34, p36}
  {p43, p44, p45, p46}
  {p37, p38, p39, p40}
  {p47, p48}
  {p41, p42}
  {p49, p50, p51, p52}
  {p53, p54}


-- Reduction pair.

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

p1: mark#(len(X)) -> active#(len(mark(X)))
p2: active#(len(cons(X,Z))) -> mark#(s(len(Z)))
p3: mark#(len(X)) -> mark#(X)
p4: mark#(add(X1,X2)) -> mark#(X2)
p5: mark#(add(X1,X2)) -> mark#(X1)
p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p8: mark#(from(X)) -> mark#(X)
p9: mark#(from(X)) -> active#(from(mark(X)))
p10: active#(add(|0|(),X)) -> mark#(X)
p11: mark#(cons(X1,X2)) -> mark#(X1)
p12: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p13: active#(from(X)) -> mark#(cons(X,from(s(X))))
p14: mark#(s(X)) -> active#(s(X))
p15: active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
p16: mark#(fst(X1,X2)) -> mark#(X2)
p17: mark#(fst(X1,X2)) -> mark#(X1)
p18: mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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

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 + 19
          len_A(x1) = max{10, x1}
          active#_A(x1) = x1 + 19
          mark_A(x1) = x1
          cons_A(x1,x2) = max{9, x1 + 7, x2 - 3}
          s_A(x1) = max{0, x1 - 3}
          add_A(x1,x2) = max{x1 + 40, x2 + 40}
          from_A(x1) = max{9, x1 + 7}
          |0|_A = 9
          fst_A(x1,x2) = max{x1 + 34, x2 + 14}
          active_A(x1) = x1
          nil_A = 1
    
      precedence:
      
        mark# = active# = mark = active = nil > cons = from = fst > len = add = |0| > s
      
      partial status:
    
        pi(mark#) = []
        pi(len) = []
        pi(active#) = []
        pi(mark) = []
        pi(cons) = []
        pi(s) = []
        pi(add) = []
        pi(from) = []
        pi(|0|) = []
        pi(fst) = []
        pi(active) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 48
          len_A(x1) = 124
          active#_A(x1) = 48
          mark_A(x1) = 122
          cons_A(x1,x2) = 114
          s_A(x1) = 155
          add_A(x1,x2) = 51
          from_A(x1) = 145
          |0|_A = 134
          fst_A(x1,x2) = 42
          active_A(x1) = 122
          nil_A = 123
    
      precedence:
      
        mark# = len = active# = mark = cons = s = add = from = |0| = fst = active = nil
      
      partial status:
    
        pi(mark#) = []
        pi(len) = []
        pi(active#) = []
        pi(mark) = []
        pi(cons) = []
        pi(s) = []
        pi(add) = []
        pi(from) = []
        pi(|0|) = []
        pi(fst) = []
        pi(active) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p17

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(len(X)) -> active#(len(mark(X)))
p2: active#(len(cons(X,Z))) -> mark#(s(len(Z)))
p3: mark#(len(X)) -> mark#(X)
p4: mark#(add(X1,X2)) -> mark#(X2)
p5: mark#(add(X1,X2)) -> mark#(X1)
p6: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p7: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p8: mark#(from(X)) -> mark#(X)
p9: mark#(from(X)) -> active#(from(mark(X)))
p10: active#(add(|0|(),X)) -> mark#(X)
p11: mark#(cons(X1,X2)) -> mark#(X1)
p12: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p13: active#(from(X)) -> mark#(cons(X,from(s(X))))
p14: mark#(s(X)) -> active#(s(X))
p15: active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
p16: mark#(fst(X1,X2)) -> mark#(X2)
p17: mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(len(X)) -> active#(len(mark(X)))
p2: active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
p3: mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
p4: active#(from(X)) -> mark#(cons(X,from(s(X))))
p5: mark#(fst(X1,X2)) -> mark#(X2)
p6: mark#(s(X)) -> active#(s(X))
p7: active#(add(|0|(),X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p10: mark#(cons(X1,X2)) -> mark#(X1)
p11: mark#(from(X)) -> active#(from(mark(X)))
p12: active#(len(cons(X,Z))) -> mark#(s(len(Z)))
p13: mark#(from(X)) -> mark#(X)
p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p15: mark#(add(X1,X2)) -> mark#(X1)
p16: mark#(add(X1,X2)) -> mark#(X2)
p17: mark#(len(X)) -> mark#(X)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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

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 + 10
          len_A(x1) = x1 + 11
          active#_A(x1) = x1 + 10
          mark_A(x1) = x1
          fst_A(x1,x2) = x2 + 9
          s_A(x1) = 0
          cons_A(x1,x2) = max{10, x1, x2}
          from_A(x1) = max{10, x1}
          add_A(x1,x2) = max{x1 + 1, x2 + 1}
          |0|_A = 7
          active_A(x1) = x1
          nil_A = 0
    
      precedence:
      
        mark# = len = active# = mark = fst = s = cons = from = add = |0| = active = nil
      
      partial status:
    
        pi(mark#) = []
        pi(len) = []
        pi(active#) = []
        pi(mark) = []
        pi(fst) = []
        pi(s) = []
        pi(cons) = []
        pi(from) = []
        pi(add) = []
        pi(|0|) = []
        pi(active) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 321
          len_A(x1) = 319
          active#_A(x1) = 321
          mark_A(x1) = max{256, x1 + 60}
          fst_A(x1,x2) = 362
          s_A(x1) = 257
          cons_A(x1,x2) = 264
          from_A(x1) = 493
          add_A(x1,x2) = 257
          |0|_A = 258
          active_A(x1) = max{317, x1}
          nil_A = 257
    
      precedence:
      
        mark# = len = active# = mark > fst = s = cons = from = add = active > |0| = nil
      
      partial status:
    
        pi(mark#) = []
        pi(len) = []
        pi(active#) = []
        pi(mark) = [1]
        pi(fst) = []
        pi(s) = []
        pi(cons) = []
        pi(from) = []
        pi(add) = []
        pi(|0|) = []
        pi(active) = [1]
        pi(nil) = []
    

The next rules are strictly ordered:

  p7, p12, p16

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(len(X)) -> active#(len(mark(X)))
p2: active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
p3: mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
p4: active#(from(X)) -> mark#(cons(X,from(s(X))))
p5: mark#(fst(X1,X2)) -> mark#(X2)
p6: mark#(s(X)) -> active#(s(X))
p7: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(from(X)) -> active#(from(mark(X)))
p11: mark#(from(X)) -> mark#(X)
p12: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p13: mark#(add(X1,X2)) -> mark#(X1)
p14: mark#(len(X)) -> mark#(X)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(len(X)) -> active#(len(mark(X)))
p2: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p3: mark#(len(X)) -> mark#(X)
p4: mark#(add(X1,X2)) -> mark#(X1)
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p6: active#(from(X)) -> mark#(cons(X,from(s(X))))
p7: mark#(from(X)) -> mark#(X)
p8: mark#(from(X)) -> active#(from(mark(X)))
p9: active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
p10: mark#(cons(X1,X2)) -> mark#(X1)
p11: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p12: mark#(s(X)) -> active#(s(X))
p13: mark#(fst(X1,X2)) -> mark#(X2)
p14: mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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

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{103, x1 + 34}
          len_A(x1) = x1 + 70
          active#_A(x1) = max{26, x1}
          mark_A(x1) = x1 + 34
          add_A(x1,x2) = max{x1 + 115, x2 + 125}
          s_A(x1) = 24
          from_A(x1) = x1 + 142
          cons_A(x1,x2) = x1 + 25
          fst_A(x1,x2) = max{98, x1 + 80, x2 + 77}
          active_A(x1) = max{58, x1}
          |0|_A = 134
          nil_A = 99
    
      precedence:
      
        nil > mark# = mark > from = |0| > len = s = cons = fst > active# = add = active
      
      partial status:
    
        pi(mark#) = [1]
        pi(len) = [1]
        pi(active#) = [1]
        pi(mark) = []
        pi(add) = [1, 2]
        pi(s) = []
        pi(from) = [1]
        pi(cons) = [1]
        pi(fst) = [1, 2]
        pi(active) = [1]
        pi(|0|) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 44
          len_A(x1) = max{190, x1 + 150}
          active#_A(x1) = max{86, x1 - 6}
          mark_A(x1) = 21
          add_A(x1,x2) = x1 + 48
          s_A(x1) = 294
          from_A(x1) = max{337, x1 + 299}
          cons_A(x1,x2) = max{85, x1 + 45}
          fst_A(x1,x2) = x2 + 48
          active_A(x1) = 21
          |0|_A = 294
          nil_A = 152
    
      precedence:
      
        mark# = len = active# = mark = add = s = from = cons = fst = active = nil > |0|
      
      partial status:
    
        pi(mark#) = [1]
        pi(len) = []
        pi(active#) = []
        pi(mark) = []
        pi(add) = [1]
        pi(s) = []
        pi(from) = [1]
        pi(cons) = [1]
        pi(fst) = [2]
        pi(active) = []
        pi(|0|) = []
        pi(nil) = []
    

The next rules are strictly ordered:

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

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(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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: fst#(mark(X1),X2) -> fst#(X1,X2)
p2: fst#(X1,active(X2)) -> fst#(X1,X2)
p3: fst#(active(X1),X2) -> fst#(X1,X2)
p4: fst#(X1,mark(X2)) -> fst#(X1,X2)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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:
        
          fst#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        fst# = mark = active
      
      partial status:
    
        pi(fst#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          fst#_A(x1,x2) = max{x1 + 1, x2 - 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        fst# = mark = active
      
      partial status:
    
        pi(fst#) = [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: from#(mark(X)) -> from#(X)
p2: from#(active(X)) -> from#(X)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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:
        
          from#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > from#
      
      partial status:
    
        pi(from#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          from#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        from# = mark = active
      
      partial status:
    
        pi(from#) = [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(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(X1,active(X2)) -> add#(X1,X2)
p3: add#(active(X1),X2) -> add#(X1,X2)
p4: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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:
        
          add#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        add# = mark = active
      
      partial status:
    
        pi(add#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          add#_A(x1,x2) = max{x1 + 1, x2 - 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        add# = mark = active
      
      partial status:
    
        pi(add#) = [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: len#(mark(X)) -> len#(X)
p2: len#(active(X)) -> len#(X)

and R consists of:

r1: active(fst(|0|(),Z)) -> mark(nil())
r2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
r3: active(from(X)) -> mark(cons(X,from(s(X))))
r4: active(add(|0|(),X)) -> mark(X)
r5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r6: active(len(nil())) -> mark(|0|())
r7: active(len(cons(X,Z))) -> mark(s(len(Z)))
r8: mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
r9: mark(|0|()) -> active(|0|())
r10: mark(nil()) -> active(nil())
r11: mark(s(X)) -> active(s(X))
r12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r13: mark(from(X)) -> active(from(mark(X)))
r14: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r15: mark(len(X)) -> active(len(mark(X)))
r16: fst(mark(X1),X2) -> fst(X1,X2)
r17: fst(X1,mark(X2)) -> fst(X1,X2)
r18: fst(active(X1),X2) -> fst(X1,X2)
r19: fst(X1,active(X2)) -> fst(X1,X2)
r20: s(mark(X)) -> s(X)
r21: s(active(X)) -> s(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: from(mark(X)) -> from(X)
r27: from(active(X)) -> from(X)
r28: add(mark(X1),X2) -> add(X1,X2)
r29: add(X1,mark(X2)) -> add(X1,X2)
r30: add(active(X1),X2) -> add(X1,X2)
r31: add(X1,active(X2)) -> add(X1,X2)
r32: len(mark(X)) -> len(X)
r33: len(active(X)) -> len(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:
        
          len#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > len#
      
      partial status:
    
        pi(len#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          len#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        len# = mark = active
      
      partial status:
    
        pi(len#) = [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.