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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((1,1),(0,0)) x1
        pairNs_A() = (1,1)
        mark#_A(x1) = ((1,1),(0,0)) x1
        cons_A(x1,x2) = ((1,1),(1,0)) x1 + ((0,1),(1,0)) x2
        |0|_A() = (0,0)
        incr_A(x1) = x1
        oddNs_A() = (1,1)
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,0)
        mark_A(x1) = x1
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,0)
        pair_A(x1,x2) = x1 + x2
        zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        take_A(x1,x2) = ((0,1),(1,1)) x1 + x2
        s_A(x1) = ((0,0),(1,1)) x1
        active_A(x1) = x1
        nil_A() = (0,0)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (3,2)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (2,1)
        |0|_A() = (2,1)
        incr_A(x1) = ((1,1),(1,1)) x1 + (4,2)
        oddNs_A() = (16,16)
        repItems_A(x1) = (3,3)
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        tail_A(x1) = (2,1)
        pair_A(x1,x2) = ((1,1),(1,1)) x1 + (3,2)
        zip_A(x1,x2) = (3,3)
        take_A(x1,x2) = ((1,1),(1,1)) x2 + (4,2)
        s_A(x1) = (2,1)
        active_A(x1) = ((0,1),(1,0)) x1 + (2,1)
        nil_A() = (1,0)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (3,1)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (0,1)
        |0|_A() = (3,1)
        incr_A(x1) = (1,1)
        oddNs_A() = (3,1)
        repItems_A(x1) = (3,1)
        mark_A(x1) = x1 + (1,1)
        tail_A(x1) = (1,1)
        pair_A(x1,x2) = (3,1)
        zip_A(x1,x2) = (1,1)
        take_A(x1,x2) = ((1,1),(0,0)) x2 + (3,1)
        s_A(x1) = (3,1)
        active_A(x1) = (3,1)
        nil_A() = (3,1)
    

The next rules are strictly ordered:

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


-- 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#(repItems(X)) -> active#(repItems(mark(X)))
p25: 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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,0)) x1
        pairNs_A() = (1,2)
        mark#_A(x1) = (2,0)
        cons_A(x1,x2) = (1,1)
        |0|_A() = (1,1)
        incr_A(x1) = (0,2)
        oddNs_A() = (1,2)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        take_A(x1,x2) = (1,2)
        zip_A(x1,x2) = (1,2)
        pair_A(x1,x2) = (1,1)
        repItems_A(x1) = (1,2)
        tail_A(x1) = (1,1)
        active_A(x1) = (1,1)
        nil_A() = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (1,0)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (0,1)
        |0|_A() = (1,1)
        incr_A(x1) = (1,1)
        oddNs_A() = (1,0)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        take_A(x1,x2) = (1,1)
        zip_A(x1,x2) = (1,1)
        pair_A(x1,x2) = (1,1)
        repItems_A(x1) = (1,0)
        tail_A(x1) = (1,1)
        active_A(x1) = (1,1)
        nil_A() = (1,0)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (1,1)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (1,1)
        |0|_A() = (1,1)
        incr_A(x1) = (1,0)
        oddNs_A() = (1,1)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        take_A(x1,x2) = (1,0)
        zip_A(x1,x2) = (1,0)
        pair_A(x1,x2) = (1,1)
        repItems_A(x1) = (1,1)
        tail_A(x1) = (1,0)
        active_A(x1) = (1,1)
        nil_A() = (1,0)
    

The next rules are strictly ordered:

  p2, p9, p20, p23

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: active#(oddNs()) -> mark#(incr(pairNs()))
p3: mark#(incr(X)) -> active#(incr(mark(X)))
p4: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p5: mark#(pairNs()) -> active#(pairNs())
p6: mark#(oddNs()) -> active#(oddNs())
p7: mark#(incr(X)) -> mark#(X)
p8: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p11: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p12: mark#(take(X1,X2)) -> mark#(X1)
p13: mark#(take(X1,X2)) -> mark#(X2)
p14: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p15: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p16: mark#(zip(X1,X2)) -> mark#(X1)
p17: mark#(zip(X1,X2)) -> mark#(X2)
p18: mark#(pair(X1,X2)) -> mark#(X1)
p19: mark#(pair(X1,X2)) -> mark#(X2)
p20: mark#(repItems(X)) -> active#(repItems(mark(X)))
p21: 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}


-- 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)) -> active#(repItems(mark(X)))
p4: active#(repItems(cons(X,XS))) -> mark#(cons(X,cons(X,repItems(XS))))
p5: mark#(pair(X1,X2)) -> mark#(X2)
p6: mark#(pair(X1,X2)) -> mark#(X1)
p7: mark#(zip(X1,X2)) -> mark#(X2)
p8: mark#(zip(X1,X2)) -> mark#(X1)
p9: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p10: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p11: mark#(take(X1,X2)) -> mark#(X2)
p12: mark#(take(X1,X2)) -> mark#(X1)
p13: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p14: active#(take(s(N),cons(X,XS))) -> mark#(cons(X,take(N,XS)))
p15: mark#(s(X)) -> mark#(X)
p16: mark#(incr(X)) -> mark#(X)
p17: mark#(oddNs()) -> active#(oddNs())
p18: active#(oddNs()) -> mark#(incr(pairNs()))
p19: mark#(incr(X)) -> active#(incr(mark(X)))
p20: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p21: 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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = x1
        pairNs_A() = (1,1)
        mark#_A(x1) = x1
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2
        |0|_A() = (0,0)
        incr_A(x1) = ((1,1),(0,0)) x1
        oddNs_A() = (2,0)
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        mark_A(x1) = ((0,0),(1,1)) x1
        pair_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2
        zip_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (1,1)
        s_A(x1) = ((1,1),(0,0)) x1
        active_A(x1) = ((0,0),(1,1)) x1
        nil_A() = (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (1,0)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (0,0)
        |0|_A() = (0,1)
        incr_A(x1) = (1,1)
        oddNs_A() = (1,1)
        repItems_A(x1) = (1,1)
        mark_A(x1) = (1,1)
        pair_A(x1,x2) = (0,1)
        zip_A(x1,x2) = (1,1)
        take_A(x1,x2) = (1,1)
        s_A(x1) = (1,1)
        active_A(x1) = (1,1)
        nil_A() = (1,1)
        tail_A(x1) = (0,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        pairNs_A() = (1,1)
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (1,0)
        |0|_A() = (1,1)
        incr_A(x1) = (1,1)
        oddNs_A() = (1,1)
        repItems_A(x1) = (1,1)
        mark_A(x1) = (1,0)
        pair_A(x1,x2) = (1,1)
        zip_A(x1,x2) = (1,1)
        take_A(x1,x2) = (1,1)
        s_A(x1) = (1,1)
        active_A(x1) = (1,0)
        nil_A() = (1,1)
        tail_A(x1) = (1,1)
    

The next rules are strictly ordered:

  p1, p4, p7, p8, p10, p11, p12, p14

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)) -> active#(repItems(mark(X)))
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p6: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p7: mark#(s(X)) -> mark#(X)
p8: mark#(incr(X)) -> mark#(X)
p9: mark#(oddNs()) -> active#(oddNs())
p10: active#(oddNs()) -> mark#(incr(pairNs()))
p11: mark#(incr(X)) -> active#(incr(mark(X)))
p12: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p13: 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}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> mark#(X1)
p2: mark#(incr(X)) -> active#(incr(mark(X)))
p3: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p4: mark#(oddNs()) -> active#(oddNs())
p5: active#(oddNs()) -> mark#(incr(pairNs()))
p6: mark#(incr(X)) -> mark#(X)
p7: mark#(s(X)) -> mark#(X)
p8: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p9: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p10: mark#(pair(X1,X2)) -> mark#(X1)
p11: mark#(pair(X1,X2)) -> mark#(X2)
p12: mark#(repItems(X)) -> active#(repItems(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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = ((0,0),(1,1)) x2
        incr_A(x1) = ((0,0),(1,1)) x1
        active#_A(x1) = x1
        mark_A(x1) = ((0,0),(1,1)) x1
        s_A(x1) = ((0,0),(1,1)) x1 + (0,1)
        oddNs_A() = (0,1)
        pairNs_A() = (0,1)
        take_A(x1,x2) = (0,1)
        zip_A(x1,x2) = ((0,0),(1,1)) x2 + (0,1)
        pair_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (0,1)
        repItems_A(x1) = ((0,0),(1,1)) x1 + (0,1)
        active_A(x1) = x1
        |0|_A() = (0,1)
        nil_A() = (0,1)
        tail_A(x1) = ((0,0),(1,1)) x1 + (0,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = (2,0)
        cons_A(x1,x2) = (1,0)
        incr_A(x1) = (2,0)
        active#_A(x1) = x1
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        oddNs_A() = (2,1)
        pairNs_A() = (1,0)
        take_A(x1,x2) = (1,1)
        zip_A(x1,x2) = (2,1)
        pair_A(x1,x2) = (1,0)
        repItems_A(x1) = (1,1)
        active_A(x1) = (1,1)
        |0|_A() = (1,1)
        nil_A() = (1,1)
        tail_A(x1) = (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = (3,0)
        cons_A(x1,x2) = (0,0)
        incr_A(x1) = (1,2)
        active#_A(x1) = ((1,1),(0,0)) x1
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        oddNs_A() = (2,1)
        pairNs_A() = (1,1)
        take_A(x1,x2) = (1,1)
        zip_A(x1,x2) = (0,1)
        pair_A(x1,x2) = (1,1)
        repItems_A(x1) = (0,0)
        active_A(x1) = (1,1)
        |0|_A() = (0,1)
        nil_A() = (0,1)
        tail_A(x1) = (0,1)
    

The next rules are strictly ordered:

  p8, p9, p12

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#(incr(X)) -> active#(incr(mark(X)))
p3: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p4: mark#(oddNs()) -> active#(oddNs())
p5: active#(oddNs()) -> mark#(incr(pairNs()))
p6: mark#(incr(X)) -> mark#(X)
p7: mark#(s(X)) -> mark#(X)
p8: mark#(pair(X1,X2)) -> mark#(X1)
p9: mark#(pair(X1,X2)) -> mark#(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}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> mark#(X1)
p2: mark#(pair(X1,X2)) -> mark#(X2)
p3: mark#(pair(X1,X2)) -> mark#(X1)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(incr(X)) -> mark#(X)
p6: mark#(oddNs()) -> active#(oddNs())
p7: active#(oddNs()) -> mark#(incr(pairNs()))
p8: mark#(incr(X)) -> active#(incr(mark(X)))
p9: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))

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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = x1
        cons_A(x1,x2) = ((1,1),(0,0)) x1 + ((0,0),(1,1)) x2
        pair_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2
        s_A(x1) = ((1,1),(0,0)) x1
        incr_A(x1) = ((1,1),(0,0)) x1
        oddNs_A() = (2,0)
        active#_A(x1) = ((1,1),(0,0)) x1
        pairNs_A() = (1,1)
        mark_A(x1) = ((1,1),(0,0)) x1
        active_A(x1) = ((1,1),(0,0)) x1
        |0|_A() = (0,0)
        take_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,0)) x2 + (2,1)
        nil_A() = (1,1)
        zip_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = ((0,1),(0,1)) x1 + (3,0)
        cons_A(x1,x2) = x1 + (1,1)
        pair_A(x1,x2) = x1 + x2 + (1,1)
        s_A(x1) = ((0,1),(0,1)) x1 + (1,1)
        incr_A(x1) = ((0,1),(0,1)) x1 + (1,4)
        oddNs_A() = (6,17)
        active#_A(x1) = ((0,1),(1,0)) x1 + (0,3)
        pairNs_A() = (1,5)
        mark_A(x1) = ((1,1),(0,1)) x1 + (1,0)
        active_A(x1) = ((0,1),(0,1)) x1
        |0|_A() = (1,1)
        take_A(x1,x2) = ((0,1),(0,1)) x2 + (1,3)
        nil_A() = (3,4)
        zip_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (1,3)
        tail_A(x1) = ((0,1),(0,0)) x1 + (1,2)
        repItems_A(x1) = x1 + (1,3)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        mark#_A(x1) = (0,0)
        cons_A(x1,x2) = (1,2)
        pair_A(x1,x2) = (1,0)
        s_A(x1) = (1,4)
        incr_A(x1) = (1,1)
        oddNs_A() = (1,4)
        active#_A(x1) = (0,0)
        pairNs_A() = (0,0)
        mark_A(x1) = ((0,1),(0,1)) x1
        active_A(x1) = (3,2)
        |0|_A() = (0,4)
        take_A(x1,x2) = (1,0)
        nil_A() = (1,4)
        zip_A(x1,x2) = (0,4)
        tail_A(x1) = (1,0)
        repItems_A(x1) = (1,4)
    

The next rules are strictly ordered:

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

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))

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:

  (no SCCs)

-- 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 monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        cons#_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,0)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        cons#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        cons#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,0),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3, p4
  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

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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        s#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        s#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        s#_A(x1) = ((1,1),(0,1)) x1
        mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        incr#_A(x1) = ((1,1),(1,0)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        incr#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(0,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        incr#_A(x1) = ((0,1),(1,1)) x1
        mark_A(x1) = ((0,0),(1,0)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        take#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(1,0)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        take#_A(x1,x2) = x1 + ((0,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((0,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        take#_A(x1,x2) = (0,0)
        mark_A(x1) = x1 + (1,1)
        active_A(x1) = (1,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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        pair#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        pair#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        pair#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3, p4
  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

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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        zip#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        zip#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,0)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        zip#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,0),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(0,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3, p4
  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

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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        repItems#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        repItems#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        repItems#_A(x1) = ((0,1),(1,1)) x1
        mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,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. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        tail#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        tail#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,0)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    3. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        tail#_A(x1) = ((1,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2
  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

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