YES

We show the termination of the TRS R:

  active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
  active(oddNs()) -> mark(incr(pairNs()))
  active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
  active(take(|0|(),XS)) -> mark(nil())
  active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
  active(zip(nil(),XS)) -> mark(nil())
  active(zip(X,nil())) -> mark(nil())
  active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
  active(tail(cons(X,XS))) -> mark(XS)
  active(repItems(nil())) -> mark(nil())
  active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
  mark(pairNs()) -> active(pairNs())
  mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
  mark(|0|()) -> active(|0|())
  mark(incr(X)) -> active(incr(mark(X)))
  mark(oddNs()) -> active(oddNs())
  mark(s(X)) -> active(s(mark(X)))
  mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
  mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
  mark(tail(X)) -> active(tail(mark(X)))
  mark(repItems(X)) -> active(repItems(mark(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)
  incr(mark(X)) -> incr(X)
  incr(active(X)) -> incr(X)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  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)
  zip(mark(X1),X2) -> zip(X1,X2)
  zip(X1,mark(X2)) -> zip(X1,X2)
  zip(active(X1),X2) -> zip(X1,X2)
  zip(X1,active(X2)) -> zip(X1,X2)
  pair(mark(X1),X2) -> pair(X1,X2)
  pair(X1,mark(X2)) -> pair(X1,X2)
  pair(active(X1),X2) -> pair(X1,X2)
  pair(X1,active(X2)) -> pair(X1,X2)
  tail(mark(X)) -> tail(X)
  tail(active(X)) -> tail(X)
  repItems(mark(X)) -> repItems(X)
  repItems(active(X)) -> repItems(X)

-- SCC decomposition.

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

p1: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: active#(pairNs()) -> cons#(|0|(),incr(oddNs()))
p3: active#(pairNs()) -> incr#(oddNs())
p4: active#(oddNs()) -> mark#(incr(pairNs()))
p5: active#(oddNs()) -> incr#(pairNs())
p6: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p7: active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
p8: active#(incr(cons(X,XS))) -> s#(X)
p9: active#(incr(cons(X,XS))) -> incr#(XS)
p10: active#(take(|0|(),XS)) -> mark#(nil())
p11: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p12: active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
p13: active#(take(s(N),cons(X,XS))) -> take#(N,XS)
p14: active#(zip(nil(),XS)) -> mark#(nil())
p15: active#(zip(X,nil())) -> mark#(nil())
p16: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p17: active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
p18: active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
p19: active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
p20: active#(tail(cons(X,XS))) -> mark#(XS)
p21: active#(repItems(nil())) -> mark#(nil())
p22: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p23: active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
p24: active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
p25: active#(repItems(cons(X,XS))) -> repItems#(XS)
p26: mark#(pairNs()) -> active#(pairNs())
p27: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p28: mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
p29: mark#(cons(X1,X2)) -> mark#(X1)
p30: mark#(|0|()) -> active#(|0|())
p31: mark#(incr(X)) -> active#(incr(mark(X)))
p32: mark#(incr(X)) -> incr#(mark(X))
p33: mark#(incr(X)) -> mark#(X)
p34: mark#(oddNs()) -> active#(oddNs())
p35: mark#(s(X)) -> active#(s(mark(X)))
p36: mark#(s(X)) -> s#(mark(X))
p37: mark#(s(X)) -> mark#(X)
p38: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p39: mark#(take(X1,X2)) -> take#(mark(X1),mark(X2))
p40: mark#(take(X1,X2)) -> mark#(X1)
p41: mark#(take(X1,X2)) -> mark#(X2)
p42: mark#(nil()) -> active#(nil())
p43: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p44: mark#(zip(X1,X2)) -> zip#(mark(X1),mark(X2))
p45: mark#(zip(X1,X2)) -> mark#(X1)
p46: mark#(zip(X1,X2)) -> mark#(X2)
p47: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p48: mark#(pair(X1,X2)) -> pair#(mark(X1),mark(X2))
p49: mark#(pair(X1,X2)) -> mark#(X1)
p50: mark#(pair(X1,X2)) -> mark#(X2)
p51: mark#(tail(X)) -> active#(tail(mark(X)))
p52: mark#(tail(X)) -> tail#(mark(X))
p53: mark#(tail(X)) -> mark#(X)
p54: mark#(repItems(X)) -> active#(repItems(mark(X)))
p55: mark#(repItems(X)) -> repItems#(mark(X))
p56: mark#(repItems(X)) -> mark#(X)
p57: cons#(mark(X1),X2) -> cons#(X1,X2)
p58: cons#(X1,mark(X2)) -> cons#(X1,X2)
p59: cons#(active(X1),X2) -> cons#(X1,X2)
p60: cons#(X1,active(X2)) -> cons#(X1,X2)
p61: incr#(mark(X)) -> incr#(X)
p62: incr#(active(X)) -> incr#(X)
p63: s#(mark(X)) -> s#(X)
p64: s#(active(X)) -> s#(X)
p65: take#(mark(X1),X2) -> take#(X1,X2)
p66: take#(X1,mark(X2)) -> take#(X1,X2)
p67: take#(active(X1),X2) -> take#(X1,X2)
p68: take#(X1,active(X2)) -> take#(X1,X2)
p69: zip#(mark(X1),X2) -> zip#(X1,X2)
p70: zip#(X1,mark(X2)) -> zip#(X1,X2)
p71: zip#(active(X1),X2) -> zip#(X1,X2)
p72: zip#(X1,active(X2)) -> zip#(X1,X2)
p73: pair#(mark(X1),X2) -> pair#(X1,X2)
p74: pair#(X1,mark(X2)) -> pair#(X1,X2)
p75: pair#(active(X1),X2) -> pair#(X1,X2)
p76: pair#(X1,active(X2)) -> pair#(X1,X2)
p77: tail#(mark(X)) -> tail#(X)
p78: tail#(active(X)) -> tail#(X)
p79: repItems#(mark(X)) -> repItems#(X)
p80: repItems#(active(X)) -> repItems#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p4, p6, p11, p16, p20, p22, p26, p27, p29, p31, p33, p34, p35, p37, p38, p40, p41, p43, p45, p46, p47, p49, p50, p51, p53, p54, p56}
  {p57, p58, p59, p60}
  {p63, p64}
  {p61, p62}
  {p65, p66, p67, p68}
  {p73, p74, p75, p76}
  {p69, p70, p71, p72}
  {p79, p80}
  {p77, p78}


-- Reduction pair.

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

p1: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: mark#(cons(X1,X2)) -> mark#(X1)
p3: mark#(repItems(X)) -> mark#(X)
p4: mark#(repItems(X)) -> active#(repItems(mark(X)))
p5: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(tail(X)) -> active#(tail(mark(X)))
p8: active#(tail(cons(X,XS))) -> mark#(XS)
p9: mark#(pair(X1,X2)) -> mark#(X2)
p10: mark#(pair(X1,X2)) -> mark#(X1)
p11: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p12: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(zip(X1,X2)) -> mark#(X1)
p15: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p16: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p17: mark#(take(X1,X2)) -> mark#(X2)
p18: mark#(take(X1,X2)) -> mark#(X1)
p19: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p20: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p21: mark#(s(X)) -> mark#(X)
p22: mark#(s(X)) -> active#(s(mark(X)))
p23: active#(oddNs()) -> mark#(incr(pairNs()))
p24: mark#(incr(X)) -> mark#(X)
p25: mark#(oddNs()) -> active#(oddNs())
p26: mark#(incr(X)) -> active#(incr(mark(X)))
p27: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p28: mark#(pairNs()) -> active#(pairNs())

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47

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{2, x1 - 5}
          pairNs_A = 85
          mark#_A(x1) = max{1, x1 - 5}
          cons_A(x1,x2) = max{x1 + 16, x2 - 48}
          |0|_A = 63
          incr_A(x1) = x1 + 21
          oddNs_A = 111
          repItems_A(x1) = x1 + 55
          mark_A(x1) = x1
          tail_A(x1) = max{59, x1 + 55}
          pair_A(x1,x2) = max{x1 + 18, x2 + 14}
          zip_A(x1,x2) = max{x1 + 84, x2 + 90}
          take_A(x1,x2) = max{x1 + 58, x2 + 62}
          s_A(x1) = x1 + 17
          active_A(x1) = max{15, x1}
          nil_A = 63
    
      precedence:
      
        active# = pairNs = mark# = cons = |0| = incr = oddNs = repItems = mark = tail = pair = zip = take = s = active = nil
      
      partial status:
    
        pi(active#) = []
        pi(pairNs) = []
        pi(mark#) = []
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(repItems) = []
        pi(mark) = []
        pi(tail) = []
        pi(pair) = []
        pi(zip) = []
        pi(take) = []
        pi(s) = []
        pi(active) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 37
          pairNs_A = 284
          mark#_A(x1) = 37
          cons_A(x1,x2) = 132
          |0|_A = 503
          incr_A(x1) = 132
          oddNs_A = 133
          repItems_A(x1) = 593
          mark_A(x1) = 130
          tail_A(x1) = 135
          pair_A(x1,x2) = 14
          zip_A(x1,x2) = 0
          take_A(x1,x2) = 132
          s_A(x1) = 207
          active_A(x1) = 130
          nil_A = 598
    
      precedence:
      
        pairNs > oddNs = nil > take > active# = mark# = cons = |0| = incr = repItems = mark = tail = pair = zip = s = active
      
      partial status:
    
        pi(active#) = []
        pi(pairNs) = []
        pi(mark#) = []
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(repItems) = []
        pi(mark) = []
        pi(tail) = []
        pi(pair) = []
        pi(zip) = []
        pi(take) = []
        pi(s) = []
        pi(active) = []
        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: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: mark#(cons(X1,X2)) -> mark#(X1)
p3: mark#(repItems(X)) -> mark#(X)
p4: mark#(repItems(X)) -> active#(repItems(mark(X)))
p5: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(tail(X)) -> active#(tail(mark(X)))
p8: mark#(pair(X1,X2)) -> mark#(X2)
p9: mark#(pair(X1,X2)) -> mark#(X1)
p10: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p11: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p12: mark#(zip(X1,X2)) -> mark#(X2)
p13: mark#(zip(X1,X2)) -> mark#(X1)
p14: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p15: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p16: mark#(take(X1,X2)) -> mark#(X2)
p17: mark#(take(X1,X2)) -> mark#(X1)
p18: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p19: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p20: mark#(s(X)) -> mark#(X)
p21: mark#(s(X)) -> active#(s(mark(X)))
p22: active#(oddNs()) -> mark#(incr(pairNs()))
p23: mark#(incr(X)) -> mark#(X)
p24: mark#(oddNs()) -> active#(oddNs())
p25: mark#(incr(X)) -> active#(incr(mark(X)))
p26: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p27: mark#(pairNs()) -> active#(pairNs())

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27}


-- Reduction pair.

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

p1: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p3: active#(oddNs()) -> mark#(incr(pairNs()))
p4: mark#(incr(X)) -> active#(incr(mark(X)))
p5: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p6: mark#(pairNs()) -> active#(pairNs())
p7: mark#(oddNs()) -> active#(oddNs())
p8: mark#(incr(X)) -> mark#(X)
p9: mark#(s(X)) -> active#(s(mark(X)))
p10: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p13: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p14: mark#(take(X1,X2)) -> mark#(X1)
p15: mark#(take(X1,X2)) -> mark#(X2)
p16: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p17: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p18: mark#(zip(X1,X2)) -> mark#(X1)
p19: mark#(zip(X1,X2)) -> mark#(X2)
p20: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p21: mark#(pair(X1,X2)) -> mark#(X1)
p22: mark#(pair(X1,X2)) -> mark#(X2)
p23: mark#(tail(X)) -> active#(tail(mark(X)))
p24: mark#(tail(X)) -> mark#(X)
p25: mark#(repItems(X)) -> active#(repItems(mark(X)))
p26: mark#(repItems(X)) -> mark#(X)
p27: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47

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{8, x1 + 7}
          pairNs_A = 29
          mark#_A(x1) = max{9, x1 + 7}
          cons_A(x1,x2) = max{19, x1 + 7, x2 - 43}
          |0|_A = 15
          incr_A(x1) = x1 + 13
          oddNs_A = 42
          mark_A(x1) = x1
          s_A(x1) = x1 + 13
          take_A(x1,x2) = max{x1 + 84, x2 + 70}
          zip_A(x1,x2) = max{x1 + 61, x2 + 46}
          pair_A(x1,x2) = max{13, x1 + 7, x2 + 7}
          repItems_A(x1) = x1 + 70
          tail_A(x1) = max{51, x1 + 44}
          active_A(x1) = max{13, x1}
          nil_A = 14
    
      precedence:
      
        pairNs = oddNs = take = pair > incr = zip > cons = repItems = nil > active# = mark# = |0| = mark = s = tail = active
      
      partial status:
    
        pi(active#) = [1]
        pi(pairNs) = []
        pi(mark#) = [1]
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(mark) = []
        pi(s) = []
        pi(take) = []
        pi(zip) = []
        pi(pair) = []
        pi(repItems) = []
        pi(tail) = []
        pi(active) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 849
          pairNs_A = 740
          mark#_A(x1) = 849
          cons_A(x1,x2) = 715
          |0|_A = 789
          incr_A(x1) = 780
          oddNs_A = 703
          mark_A(x1) = 727
          s_A(x1) = 782
          take_A(x1,x2) = 319
          zip_A(x1,x2) = 0
          pair_A(x1,x2) = 722
          repItems_A(x1) = 780
          tail_A(x1) = 782
          active_A(x1) = 727
          nil_A = 857
    
      precedence:
      
        active# = mark# = |0| = oddNs > pairNs = incr = mark = s = repItems = tail = active = nil > pair > cons = take = zip
      
      partial status:
    
        pi(active#) = []
        pi(pairNs) = []
        pi(mark#) = []
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(mark) = []
        pi(s) = []
        pi(take) = []
        pi(zip) = []
        pi(pair) = []
        pi(repItems) = []
        pi(tail) = []
        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: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p3: active#(oddNs()) -> mark#(incr(pairNs()))
p4: mark#(incr(X)) -> active#(incr(mark(X)))
p5: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p6: mark#(pairNs()) -> active#(pairNs())
p7: mark#(oddNs()) -> active#(oddNs())
p8: mark#(incr(X)) -> mark#(X)
p9: mark#(s(X)) -> active#(s(mark(X)))
p10: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p13: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p14: mark#(take(X1,X2)) -> mark#(X1)
p15: mark#(take(X1,X2)) -> mark#(X2)
p16: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p17: mark#(zip(X1,X2)) -> mark#(X1)
p18: mark#(zip(X1,X2)) -> mark#(X2)
p19: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p20: mark#(pair(X1,X2)) -> mark#(X1)
p21: mark#(pair(X1,X2)) -> mark#(X2)
p22: mark#(tail(X)) -> active#(tail(mark(X)))
p23: mark#(tail(X)) -> mark#(X)
p24: mark#(repItems(X)) -> active#(repItems(mark(X)))
p25: mark#(repItems(X)) -> mark#(X)
p26: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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, p18, p19, p20, p21, p22, p23, p24, p25, p26}


-- Reduction pair.

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

p1: active#(pairNs()) -> mark#(cons(|0|(),incr(oddNs())))
p2: mark#(cons(X1,X2)) -> mark#(X1)
p3: mark#(repItems(X)) -> mark#(X)
p4: mark#(repItems(X)) -> active#(repItems(mark(X)))
p5: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(tail(X)) -> active#(tail(mark(X)))
p8: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p9: mark#(pair(X1,X2)) -> mark#(X2)
p10: mark#(pair(X1,X2)) -> mark#(X1)
p11: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p12: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(zip(X1,X2)) -> mark#(X1)
p15: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p16: active#(oddNs()) -> mark#(incr(pairNs()))
p17: mark#(incr(X)) -> mark#(X)
p18: mark#(take(X1,X2)) -> mark#(X2)
p19: mark#(take(X1,X2)) -> mark#(X1)
p20: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p21: mark#(s(X)) -> mark#(X)
p22: mark#(s(X)) -> active#(s(mark(X)))
p23: mark#(oddNs()) -> active#(oddNs())
p24: mark#(pairNs()) -> active#(pairNs())
p25: mark#(incr(X)) -> active#(incr(mark(X)))
p26: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47

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{2, x1}
          pairNs_A = 46
          mark#_A(x1) = max{46, x1}
          cons_A(x1,x2) = max{8, x1 + 4, x2 - 32}
          |0|_A = 41
          incr_A(x1) = max{51, x1 + 15}
          oddNs_A = 62
          repItems_A(x1) = x1 + 47
          mark_A(x1) = x1
          zip_A(x1,x2) = max{x1 + 81, x2 + 82}
          pair_A(x1,x2) = max{x1 + 80, x2 + 45}
          tail_A(x1) = x1 + 46
          take_A(x1,x2) = max{48, x1 + 40, x2 + 41}
          s_A(x1) = max{46, x1 + 7}
          active_A(x1) = x1
          nil_A = 0
    
      precedence:
      
        zip = take > incr > mark = nil > cons = oddNs > |0| > pairNs = tail = s = active > mark# = pair > active# = repItems
      
      partial status:
    
        pi(active#) = [1]
        pi(pairNs) = []
        pi(mark#) = [1]
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(repItems) = []
        pi(mark) = [1]
        pi(zip) = []
        pi(pair) = [2]
        pi(tail) = []
        pi(take) = []
        pi(s) = []
        pi(active) = [1]
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = x1 + 170
          pairNs_A = 248
          mark#_A(x1) = 231
          cons_A(x1,x2) = 59
          |0|_A = 414
          incr_A(x1) = 61
          oddNs_A = 61
          repItems_A(x1) = 0
          mark_A(x1) = 312
          zip_A(x1,x2) = 61
          pair_A(x1,x2) = 55
          tail_A(x1) = 41
          take_A(x1,x2) = 61
          s_A(x1) = 60
          active_A(x1) = 312
          nil_A = 450
    
      precedence:
      
        s > pairNs = cons = |0| = incr = nil > pair = take > tail > active# = mark# = oddNs > mark = zip > active > repItems
      
      partial status:
    
        pi(active#) = [1]
        pi(pairNs) = []
        pi(mark#) = []
        pi(cons) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(repItems) = []
        pi(mark) = []
        pi(zip) = []
        pi(pair) = []
        pi(tail) = []
        pi(take) = []
        pi(s) = []
        pi(active) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p1, p4, p8, p10, p12, p13, p15, p16, p17, p18, p19, p20, p23, p24, p25

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(cons(X1,X2)) -> mark#(X1)
p2: mark#(repItems(X)) -> mark#(X)
p3: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p4: mark#(tail(X)) -> mark#(X)
p5: mark#(tail(X)) -> active#(tail(mark(X)))
p6: mark#(pair(X1,X2)) -> mark#(X2)
p7: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p8: mark#(zip(X1,X2)) -> mark#(X1)
p9: mark#(s(X)) -> mark#(X)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> mark#(X1)
p2: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p3: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p4: mark#(s(X)) -> active#(s(mark(X)))
p5: mark#(s(X)) -> mark#(X)
p6: mark#(zip(X1,X2)) -> mark#(X1)
p7: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p8: mark#(pair(X1,X2)) -> mark#(X2)
p9: mark#(tail(X)) -> active#(tail(mark(X)))
p10: mark#(tail(X)) -> mark#(X)
p11: mark#(repItems(X)) -> mark#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47

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{4, x1 - 7}
          cons_A(x1,x2) = max{17, x1 + 1, x2 - 26}
          active#_A(x1) = max{2, x1 - 7}
          mark_A(x1) = max{8, x1}
          zip_A(x1,x2) = max{59, x1 + 51, x2 + 51}
          pair_A(x1,x2) = max{10, x2}
          s_A(x1) = max{5, x1}
          tail_A(x1) = max{50, x1 + 35}
          repItems_A(x1) = max{52, x1 + 44}
          active_A(x1) = max{7, x1}
          pairNs_A = 26
          |0|_A = 9
          incr_A(x1) = max{26, x1}
          oddNs_A = 32
          take_A(x1,x2) = max{59, x1 + 51, x2 + 44}
          nil_A = 6
    
      precedence:
      
        zip = |0| = take > incr > mark > repItems > active > cons = pair > mark# = active# = s = tail = pairNs = oddNs = nil
      
      partial status:
    
        pi(mark#) = []
        pi(cons) = []
        pi(active#) = []
        pi(mark) = [1]
        pi(zip) = []
        pi(pair) = []
        pi(s) = []
        pi(tail) = []
        pi(repItems) = []
        pi(active) = [1]
        pi(pairNs) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(take) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 257
          cons_A(x1,x2) = 276
          active#_A(x1) = 257
          mark_A(x1) = max{258, x1 + 130}
          zip_A(x1,x2) = 422
          pair_A(x1,x2) = 385
          s_A(x1) = 274
          tail_A(x1) = 58
          repItems_A(x1) = 125
          active_A(x1) = max{257, x1 - 15}
          pairNs_A = 421
          |0|_A = 603
          incr_A(x1) = 422
          oddNs_A = 567
          take_A(x1,x2) = 421
          nil_A = 126
    
      precedence:
      
        |0| = oddNs = take > mark# = cons = active# = nil > zip = pair = s = tail = repItems = active = incr > mark = pairNs
      
      partial status:
    
        pi(mark#) = []
        pi(cons) = []
        pi(active#) = []
        pi(mark) = []
        pi(zip) = []
        pi(pair) = []
        pi(s) = []
        pi(tail) = []
        pi(repItems) = []
        pi(active) = []
        pi(pairNs) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(take) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p10

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(cons(X1,X2)) -> mark#(X1)
p2: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p3: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p4: mark#(s(X)) -> active#(s(mark(X)))
p5: mark#(s(X)) -> mark#(X)
p6: mark#(zip(X1,X2)) -> mark#(X1)
p7: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p8: mark#(pair(X1,X2)) -> mark#(X2)
p9: mark#(tail(X)) -> active#(tail(mark(X)))
p10: mark#(repItems(X)) -> mark#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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#(cons(X1,X2)) -> mark#(X1)
p2: mark#(repItems(X)) -> mark#(X)
p3: mark#(tail(X)) -> active#(tail(mark(X)))
p4: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p5: mark#(pair(X1,X2)) -> mark#(X2)
p6: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p7: mark#(zip(X1,X2)) -> mark#(X1)
p8: mark#(s(X)) -> mark#(X)
p9: mark#(s(X)) -> active#(s(mark(X)))
p10: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47

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}
          cons_A(x1,x2) = max{32, x1 + 3, x2 - 21}
          repItems_A(x1) = max{75, x1 + 74}
          tail_A(x1) = max{41, x1 + 21}
          active#_A(x1) = max{2, x1}
          mark_A(x1) = x1
          zip_A(x1,x2) = max{x1 + 28, x2 + 54}
          pair_A(x1,x2) = x2 + 20
          s_A(x1) = max{23, x1 + 3}
          active_A(x1) = max{20, x1}
          pairNs_A = 33
          |0|_A = 30
          incr_A(x1) = max{37, x1 + 3}
          oddNs_A = 37
          take_A(x1,x2) = max{x1 + 52, x2 + 52}
          nil_A = 21
    
      precedence:
      
        zip = oddNs > mark# > tail = active# > cons = incr > pair > repItems = mark = s = active = pairNs = |0| = take = nil
      
      partial status:
    
        pi(mark#) = [1]
        pi(cons) = []
        pi(repItems) = []
        pi(tail) = []
        pi(active#) = [1]
        pi(mark) = []
        pi(zip) = []
        pi(pair) = []
        pi(s) = []
        pi(active) = []
        pi(pairNs) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(take) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 107
          cons_A(x1,x2) = 57
          repItems_A(x1) = 362
          tail_A(x1) = 546
          active#_A(x1) = 58
          mark_A(x1) = 302
          zip_A(x1,x2) = 116
          pair_A(x1,x2) = 55
          s_A(x1) = 394
          active_A(x1) = 302
          pairNs_A = 430
          |0|_A = 456
          incr_A(x1) = 393
          oddNs_A = 363
          take_A(x1,x2) = 27
          nil_A = 151
    
      precedence:
      
        incr > oddNs = nil > cons = repItems = |0| > mark# = tail = mark = zip = pair = s = active = pairNs = take > active#
      
      partial status:
    
        pi(mark#) = []
        pi(cons) = []
        pi(repItems) = []
        pi(tail) = []
        pi(active#) = []
        pi(mark) = []
        pi(zip) = []
        pi(pair) = []
        pi(s) = []
        pi(active) = []
        pi(pairNs) = []
        pi(|0|) = []
        pi(incr) = []
        pi(oddNs) = []
        pi(take) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p1, p3, p4, p5, p9

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(repItems(X)) -> mark#(X)
p2: mark#(pair(X1,X2)) -> active#(pair(mark(X1),mark(X2)))
p3: mark#(zip(X1,X2)) -> mark#(X1)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p3, p4}


-- Reduction pair.

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

p1: mark#(repItems(X)) -> mark#(X)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(zip(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          mark#_A(x1) = max{2, x1 + 1}
          repItems_A(x1) = max{1, x1}
          s_A(x1) = max{1, x1}
          zip_A(x1,x2) = max{1, x1, x2}
    
      precedence:
      
        mark# = repItems = s = zip
      
      partial status:
    
        pi(mark#) = [1]
        pi(repItems) = [1]
        pi(s) = [1]
        pi(zip) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          repItems_A(x1) = x1 + 1
          s_A(x1) = x1 + 1
          zip_A(x1,x2) = max{x1 + 1, x2}
    
      precedence:
      
        mark# = repItems = s = zip
      
      partial status:
    
        pi(mark#) = []
        pi(repItems) = [1]
        pi(s) = [1]
        pi(zip) = [2]
    

The next rules are strictly ordered:

  p1, p2, p3

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

-- Reduction pair.

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

p1: 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(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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: incr#(mark(X)) -> incr#(X)
p2: incr#(active(X)) -> incr#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          incr#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > incr#
      
      partial status:
    
        pi(incr#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          incr#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        incr# = mark = active
      
      partial status:
    
        pi(incr#) = [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(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(X1,active(X2)) -> pair#(X1,X2)
p3: pair#(active(X1),X2) -> pair#(X1,X2)
p4: pair#(X1,mark(X2)) -> pair#(X1,X2)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          pair#_A(x1,x2) = max{4, x1 + 1, x2 + 3}
          mark_A(x1) = max{3, x1 + 2}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        pair# = mark = active
      
      partial status:
    
        pi(pair#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          pair#_A(x1,x2) = max{x1 + 1, x2 + 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        pair# = mark = active
      
      partial status:
    
        pi(pair#) = [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: zip#(mark(X1),X2) -> zip#(X1,X2)
p2: zip#(X1,active(X2)) -> zip#(X1,X2)
p3: zip#(active(X1),X2) -> zip#(X1,X2)
p4: zip#(X1,mark(X2)) -> zip#(X1,X2)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          zip#_A(x1,x2) = max{4, x1 + 1, x2 + 3}
          mark_A(x1) = max{3, x1 + 2}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        zip# = mark = active
      
      partial status:
    
        pi(zip#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          zip#_A(x1,x2) = max{x1 + 1, x2 + 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        zip# = mark = active
      
      partial status:
    
        pi(zip#) = [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: repItems#(mark(X)) -> repItems#(X)
p2: repItems#(active(X)) -> repItems#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          repItems#_A(x1) = max{6, x1 + 4}
          mark_A(x1) = max{4, x1 + 3}
          active_A(x1) = max{2, x1 + 1}
    
      precedence:
      
        repItems# = mark = active
      
      partial status:
    
        pi(repItems#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          repItems#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        repItems# = mark = active
      
      partial status:
    
        pi(repItems#) = [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: tail#(mark(X)) -> tail#(X)
p2: tail#(active(X)) -> tail#(X)

and R consists of:

r1: active(pairNs()) -> mark(cons(|0|(),incr(oddNs())))
r2: active(oddNs()) -> mark(incr(pairNs()))
r3: active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
r4: active(take(|0|(),XS)) -> mark(nil())
r5: active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS)))
r6: active(zip(nil(),XS)) -> mark(nil())
r7: active(zip(X,nil())) -> mark(nil())
r8: active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS)))
r9: active(tail(cons(X,XS))) -> mark(XS)
r10: active(repItems(nil())) -> mark(nil())
r11: active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS))))
r12: mark(pairNs()) -> active(pairNs())
r13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r14: mark(|0|()) -> active(|0|())
r15: mark(incr(X)) -> active(incr(mark(X)))
r16: mark(oddNs()) -> active(oddNs())
r17: mark(s(X)) -> active(s(mark(X)))
r18: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2)))
r21: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2)))
r22: mark(tail(X)) -> active(tail(mark(X)))
r23: mark(repItems(X)) -> active(repItems(mark(X)))
r24: cons(mark(X1),X2) -> cons(X1,X2)
r25: cons(X1,mark(X2)) -> cons(X1,X2)
r26: cons(active(X1),X2) -> cons(X1,X2)
r27: cons(X1,active(X2)) -> cons(X1,X2)
r28: incr(mark(X)) -> incr(X)
r29: incr(active(X)) -> incr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: take(mark(X1),X2) -> take(X1,X2)
r33: take(X1,mark(X2)) -> take(X1,X2)
r34: take(active(X1),X2) -> take(X1,X2)
r35: take(X1,active(X2)) -> take(X1,X2)
r36: zip(mark(X1),X2) -> zip(X1,X2)
r37: zip(X1,mark(X2)) -> zip(X1,X2)
r38: zip(active(X1),X2) -> zip(X1,X2)
r39: zip(X1,active(X2)) -> zip(X1,X2)
r40: pair(mark(X1),X2) -> pair(X1,X2)
r41: pair(X1,mark(X2)) -> pair(X1,X2)
r42: pair(active(X1),X2) -> pair(X1,X2)
r43: pair(X1,active(X2)) -> pair(X1,X2)
r44: tail(mark(X)) -> tail(X)
r45: tail(active(X)) -> tail(X)
r46: repItems(mark(X)) -> repItems(X)
r47: repItems(active(X)) -> repItems(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:
        
          tail#_A(x1) = max{6, x1 + 4}
          mark_A(x1) = max{4, x1 + 3}
          active_A(x1) = max{2, x1 + 1}
    
      precedence:
      
        tail# = mark = active
      
      partial status:
    
        pi(tail#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          tail#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        tail# = mark = active
      
      partial status:
    
        pi(tail#) = [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.