YES

We show the termination of the TRS R:

  a__pairNs() -> cons(|0|(),incr(oddNs()))
  a__oddNs() -> a__incr(a__pairNs())
  a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
  a__take(|0|(),XS) -> nil()
  a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
  a__zip(nil(),XS) -> nil()
  a__zip(X,nil()) -> nil()
  a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
  a__tail(cons(X,XS)) -> mark(XS)
  a__repItems(nil()) -> nil()
  a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
  mark(pairNs()) -> a__pairNs()
  mark(incr(X)) -> a__incr(mark(X))
  mark(oddNs()) -> a__oddNs()
  mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
  mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
  mark(tail(X)) -> a__tail(mark(X))
  mark(repItems(X)) -> a__repItems(mark(X))
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(|0|()) -> |0|()
  mark(s(X)) -> s(mark(X))
  mark(nil()) -> nil()
  mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
  a__pairNs() -> pairNs()
  a__incr(X) -> incr(X)
  a__oddNs() -> oddNs()
  a__take(X1,X2) -> take(X1,X2)
  a__zip(X1,X2) -> zip(X1,X2)
  a__tail(X) -> tail(X)
  a__repItems(X) -> repItems(X)

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p3, p4, p5, p6, p7, p8, 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: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(repItems(X)) -> mark#(X)
p8: mark#(repItems(X)) -> a__repItems#(mark(X))
p9: a__repItems#(cons(X,XS)) -> mark#(X)
p10: mark#(tail(X)) -> mark#(X)
p11: mark#(tail(X)) -> a__tail#(mark(X))
p12: a__tail#(cons(X,XS)) -> mark#(XS)
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(zip(X1,X2)) -> mark#(X1)
p15: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p16: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(Y)
p17: mark#(take(X1,X2)) -> mark#(X2)
p18: mark#(take(X1,X2)) -> mark#(X1)
p19: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p20: a__take#(s(N),cons(X,XS)) -> mark#(X)
p21: mark#(oddNs()) -> a__oddNs#()
p22: mark#(incr(X)) -> mark#(X)
p23: mark#(incr(X)) -> a__incr#(mark(X))
p24: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          a__oddNs#_A() = (1,1)
          a__incr#_A(x1) = ((1,0),(1,0)) x1
          a__pairNs_A() = (1,1)
          cons_A(x1,x2) = ((1,0),(1,0)) x1 + x2
          mark#_A(x1) = ((1,0),(1,0)) x1
          pair_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2
          s_A(x1) = ((1,0),(1,1)) x1 + (0,1)
          repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          a__repItems#_A(x1) = x1 + (1,1)
          mark_A(x1) = x1
          tail_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          a__tail#_A(x1) = ((1,0),(1,0)) x1 + (1,1)
          zip_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (2,1)
          a__zip#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (1,2)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2 + (2,2)
          a__take#_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (1,0)
          oddNs_A() = (1,2)
          incr_A(x1) = ((1,0),(1,0)) x1
          a__oddNs_A() = (1,2)
          a__incr_A(x1) = ((1,0),(1,0)) x1
          a__take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2 + (2,2)
          |0|_A() = (0,0)
          nil_A() = (1,1)
          a__zip_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (2,1)
          a__tail_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          pairNs_A() = (1,1)
  
    precedence:
    
      |0| > oddNs = incr = a__oddNs = a__incr = nil > a__tail# = zip = a__zip > a__oddNs# = a__incr# = a__pairNs = cons = mark# = repItems = a__repItems# = a__zip# = take = a__take = a__repItems = pairNs > a__take# > mark = a__tail > s = tail > pair
    
    partial status:
  
      pi(a__oddNs#) = []
      pi(a__incr#) = []
      pi(a__pairNs) = []
      pi(cons) = []
      pi(mark#) = []
      pi(pair) = []
      pi(s) = []
      pi(repItems) = []
      pi(a__repItems#) = [1]
      pi(mark) = [1]
      pi(tail) = []
      pi(a__tail#) = []
      pi(zip) = []
      pi(a__zip#) = []
      pi(take) = []
      pi(a__take#) = [2]
      pi(oddNs) = []
      pi(incr) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = []
      pi(|0|) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p12

We remove them from the problem.

-- SCC decomposition.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(repItems(X)) -> mark#(X)
p8: mark#(repItems(X)) -> a__repItems#(mark(X))
p9: a__repItems#(cons(X,XS)) -> mark#(X)
p10: mark#(tail(X)) -> mark#(X)
p11: mark#(tail(X)) -> a__tail#(mark(X))
p12: mark#(zip(X1,X2)) -> mark#(X2)
p13: mark#(zip(X1,X2)) -> mark#(X1)
p14: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p15: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(Y)
p16: mark#(take(X1,X2)) -> mark#(X2)
p17: mark#(take(X1,X2)) -> mark#(X1)
p18: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p19: a__take#(s(N),cons(X,XS)) -> mark#(X)
p20: mark#(oddNs()) -> a__oddNs#()
p21: mark#(incr(X)) -> mark#(X)
p22: mark#(incr(X)) -> a__incr#(mark(X))
p23: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23}


-- Reduction pair.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(incr(X)) -> a__incr#(mark(X))
p4: mark#(incr(X)) -> mark#(X)
p5: mark#(oddNs()) -> a__oddNs#()
p6: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p7: a__take#(s(N),cons(X,XS)) -> mark#(X)
p8: mark#(take(X1,X2)) -> mark#(X1)
p9: mark#(take(X1,X2)) -> mark#(X2)
p10: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p11: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p12: mark#(zip(X1,X2)) -> mark#(X1)
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(tail(X)) -> mark#(X)
p15: mark#(repItems(X)) -> a__repItems#(mark(X))
p16: a__repItems#(cons(X,XS)) -> mark#(X)
p17: mark#(repItems(X)) -> mark#(X)
p18: mark#(cons(X1,X2)) -> mark#(X1)
p19: mark#(s(X)) -> mark#(X)
p20: mark#(pair(X1,X2)) -> mark#(X1)
p21: mark#(pair(X1,X2)) -> mark#(X2)
p22: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(Y)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          a__oddNs#_A() = (4,4)
          a__incr#_A(x1) = ((0,1),(0,1)) x1 + (3,3)
          a__pairNs_A() = (1,1)
          cons_A(x1,x2) = x1 + ((0,1),(1,0)) x2
          mark#_A(x1) = ((0,1),(0,1)) x1 + (3,3)
          incr_A(x1) = x1
          mark_A(x1) = x1
          oddNs_A() = (1,1)
          take_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (2,2)
          a__take#_A(x1,x2) = ((0,1),(0,1)) x2 + (5,3)
          s_A(x1) = ((0,0),(0,1)) x1
          zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2)
          a__zip#_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (4,5)
          tail_A(x1) = ((0,1),(1,1)) x1 + (0,1)
          repItems_A(x1) = ((1,1),(1,1)) x1 + (3,4)
          a__repItems#_A(x1) = ((0,1),(0,1)) x1 + (3,3)
          pair_A(x1,x2) = ((0,0),(0,1)) x1 + ((0,0),(0,1)) x2
          a__oddNs_A() = (1,1)
          a__incr_A(x1) = x1
          a__take_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (2,2)
          |0|_A() = (0,0)
          nil_A() = (1,1)
          a__zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2)
          a__tail_A(x1) = ((0,1),(1,1)) x1 + (0,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (3,4)
          pairNs_A() = (1,1)
  
    precedence:
    
      a__pairNs = cons = incr = mark = oddNs = take = repItems = a__oddNs = a__incr = a__take = a__zip = a__tail = a__repItems = pairNs > tail > a__oddNs# = a__incr# = mark# = a__take# = s = a__zip# = a__repItems# > zip > nil > |0| > pair
    
    partial status:
  
      pi(a__oddNs#) = []
      pi(a__incr#) = []
      pi(a__pairNs) = []
      pi(cons) = []
      pi(mark#) = []
      pi(incr) = []
      pi(mark) = []
      pi(oddNs) = []
      pi(take) = []
      pi(a__take#) = []
      pi(s) = []
      pi(zip) = []
      pi(a__zip#) = [2]
      pi(tail) = []
      pi(repItems) = []
      pi(a__repItems#) = []
      pi(pair) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = []
      pi(|0|) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p22

We remove them from the problem.

-- SCC decomposition.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(incr(X)) -> a__incr#(mark(X))
p4: mark#(incr(X)) -> mark#(X)
p5: mark#(oddNs()) -> a__oddNs#()
p6: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p7: a__take#(s(N),cons(X,XS)) -> mark#(X)
p8: mark#(take(X1,X2)) -> mark#(X1)
p9: mark#(take(X1,X2)) -> mark#(X2)
p10: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p11: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p12: mark#(zip(X1,X2)) -> mark#(X1)
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(tail(X)) -> mark#(X)
p15: mark#(repItems(X)) -> a__repItems#(mark(X))
p16: a__repItems#(cons(X,XS)) -> mark#(X)
p17: mark#(repItems(X)) -> mark#(X)
p18: mark#(cons(X1,X2)) -> mark#(X1)
p19: mark#(s(X)) -> mark#(X)
p20: mark#(pair(X1,X2)) -> mark#(X1)
p21: mark#(pair(X1,X2)) -> mark#(X2)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(repItems(X)) -> mark#(X)
p8: mark#(repItems(X)) -> a__repItems#(mark(X))
p9: a__repItems#(cons(X,XS)) -> mark#(X)
p10: mark#(tail(X)) -> mark#(X)
p11: mark#(zip(X1,X2)) -> mark#(X2)
p12: mark#(zip(X1,X2)) -> mark#(X1)
p13: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p14: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p15: mark#(take(X1,X2)) -> mark#(X2)
p16: mark#(take(X1,X2)) -> mark#(X1)
p17: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p18: a__take#(s(N),cons(X,XS)) -> mark#(X)
p19: mark#(oddNs()) -> a__oddNs#()
p20: mark#(incr(X)) -> mark#(X)
p21: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          a__oddNs#_A() = (4,1)
          a__incr#_A(x1) = ((0,1),(0,1)) x1 + (3,0)
          a__pairNs_A() = (7,1)
          cons_A(x1,x2) = ((1,1),(1,1)) x1 + x2
          mark#_A(x1) = ((0,1),(0,1)) x1 + (3,0)
          pair_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(0,1)) x2
          s_A(x1) = x1
          repItems_A(x1) = ((1,1),(1,1)) x1 + (1,2)
          a__repItems#_A(x1) = ((0,1),(1,0)) x1 + (4,1)
          mark_A(x1) = x1
          tail_A(x1) = ((1,1),(1,1)) x1 + (4,1)
          zip_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (4,3)
          a__zip#_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,0)) x2 + (5,0)
          take_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (2,2)
          a__take#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(1,0)) x2 + (4,0)
          oddNs_A() = (6,1)
          incr_A(x1) = ((0,1),(0,1)) x1 + (4,0)
          a__oddNs_A() = (6,1)
          a__incr_A(x1) = ((0,1),(0,1)) x1 + (4,0)
          a__take_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (2,2)
          |0|_A() = (0,0)
          nil_A() = (1,0)
          a__zip_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,1)) x2 + (4,3)
          a__tail_A(x1) = ((1,1),(1,1)) x1 + (4,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (1,2)
          pairNs_A() = (7,1)
  
    precedence:
    
      a__oddNs# = a__incr# = mark# = a__repItems# = a__zip# = a__take# > pair = s = mark = tail = a__tail > a__oddNs > repItems = a__repItems > a__pairNs = cons = zip = incr = a__incr = a__take = nil = a__zip = pairNs > take > oddNs = |0|
    
    partial status:
  
      pi(a__oddNs#) = []
      pi(a__incr#) = []
      pi(a__pairNs) = []
      pi(cons) = []
      pi(mark#) = []
      pi(pair) = []
      pi(s) = [1]
      pi(repItems) = []
      pi(a__repItems#) = []
      pi(mark) = [1]
      pi(tail) = []
      pi(zip) = []
      pi(a__zip#) = []
      pi(take) = []
      pi(a__take#) = []
      pi(oddNs) = []
      pi(incr) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = []
      pi(|0|) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

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: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(repItems(X)) -> mark#(X)
p8: a__repItems#(cons(X,XS)) -> mark#(X)
p9: mark#(tail(X)) -> mark#(X)
p10: mark#(zip(X1,X2)) -> mark#(X2)
p11: mark#(zip(X1,X2)) -> mark#(X1)
p12: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p13: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p14: mark#(take(X1,X2)) -> mark#(X2)
p15: mark#(take(X1,X2)) -> mark#(X1)
p16: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p17: a__take#(s(N),cons(X,XS)) -> mark#(X)
p18: mark#(oddNs()) -> a__oddNs#()
p19: mark#(incr(X)) -> mark#(X)
p20: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(incr(X)) -> a__incr#(mark(X))
p4: mark#(incr(X)) -> mark#(X)
p5: mark#(oddNs()) -> a__oddNs#()
p6: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p7: a__take#(s(N),cons(X,XS)) -> mark#(X)
p8: mark#(take(X1,X2)) -> mark#(X1)
p9: mark#(take(X1,X2)) -> mark#(X2)
p10: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p11: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p12: mark#(zip(X1,X2)) -> mark#(X1)
p13: mark#(zip(X1,X2)) -> mark#(X2)
p14: mark#(tail(X)) -> mark#(X)
p15: mark#(repItems(X)) -> mark#(X)
p16: mark#(cons(X1,X2)) -> mark#(X1)
p17: mark#(s(X)) -> mark#(X)
p18: mark#(pair(X1,X2)) -> mark#(X1)
p19: mark#(pair(X1,X2)) -> mark#(X2)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          a__oddNs#_A() = (3,0)
          a__incr#_A(x1) = ((1,0),(1,0)) x1 + (3,0)
          a__pairNs_A() = (0,0)
          cons_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(1,0)) x2
          mark#_A(x1) = ((0,1),(0,1)) x1 + (3,0)
          incr_A(x1) = ((1,1),(1,1)) x1
          mark_A(x1) = x1
          oddNs_A() = (0,0)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)
          a__take#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (2,0)
          s_A(x1) = x1 + (2,0)
          zip_A(x1,x2) = x1 + x2
          a__zip#_A(x1,x2) = ((0,1),(0,1)) x1 + (3,0)
          tail_A(x1) = ((0,1),(1,1)) x1 + (1,1)
          repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          pair_A(x1,x2) = ((0,0),(0,1)) x1 + ((0,1),(0,1)) x2 + (1,0)
          a__oddNs_A() = (0,0)
          a__incr_A(x1) = ((1,1),(1,1)) x1
          a__take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)
          |0|_A() = (1,0)
          nil_A() = (1,1)
          a__zip_A(x1,x2) = x1 + x2
          a__tail_A(x1) = ((0,1),(1,1)) x1 + (1,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          pairNs_A() = (0,0)
  
    precedence:
    
      a__oddNs# = a__incr# = mark# = a__zip# > a__take# > zip = repItems = |0| = a__zip = a__repItems > tail = a__tail > a__pairNs = cons = mark = take = s = a__oddNs = a__incr = a__take = nil > oddNs = pairNs > incr > pair
    
    partial status:
  
      pi(a__oddNs#) = []
      pi(a__incr#) = []
      pi(a__pairNs) = []
      pi(cons) = []
      pi(mark#) = []
      pi(incr) = []
      pi(mark) = [1]
      pi(oddNs) = []
      pi(take) = []
      pi(a__take#) = []
      pi(s) = [1]
      pi(zip) = []
      pi(a__zip#) = []
      pi(tail) = []
      pi(repItems) = []
      pi(pair) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = [2]
      pi(|0|) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(incr(X)) -> a__incr#(mark(X))
p4: mark#(incr(X)) -> mark#(X)
p5: mark#(oddNs()) -> a__oddNs#()
p6: a__take#(s(N),cons(X,XS)) -> mark#(X)
p7: mark#(take(X1,X2)) -> mark#(X1)
p8: mark#(take(X1,X2)) -> mark#(X2)
p9: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p10: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p11: mark#(zip(X1,X2)) -> mark#(X1)
p12: mark#(zip(X1,X2)) -> mark#(X2)
p13: mark#(tail(X)) -> mark#(X)
p14: mark#(repItems(X)) -> mark#(X)
p15: mark#(cons(X1,X2)) -> mark#(X1)
p16: mark#(s(X)) -> mark#(X)
p17: mark#(pair(X1,X2)) -> mark#(X1)
p18: mark#(pair(X1,X2)) -> mark#(X2)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: a__incr#(cons(X,XS)) -> mark#(X)
p3: mark#(pair(X1,X2)) -> mark#(X2)
p4: mark#(pair(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(repItems(X)) -> mark#(X)
p8: mark#(tail(X)) -> mark#(X)
p9: mark#(zip(X1,X2)) -> mark#(X2)
p10: mark#(zip(X1,X2)) -> mark#(X1)
p11: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p12: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p13: mark#(take(X1,X2)) -> mark#(X2)
p14: mark#(take(X1,X2)) -> mark#(X1)
p15: mark#(oddNs()) -> a__oddNs#()
p16: mark#(incr(X)) -> mark#(X)
p17: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          a__oddNs#_A() = (1,1)
          a__incr#_A(x1) = x1
          a__pairNs_A() = (1,1)
          cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,0)) x2
          mark#_A(x1) = x1
          pair_A(x1,x2) = ((1,1),(0,1)) x1 + x2
          s_A(x1) = x1
          repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2)
          a__zip#_A(x1,x2) = ((1,1),(1,1)) x1 + (1,1)
          mark_A(x1) = x1
          take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
          oddNs_A() = (1,1)
          incr_A(x1) = x1
          a__oddNs_A() = (1,1)
          a__incr_A(x1) = x1
          a__take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
          |0|_A() = (0,0)
          nil_A() = (1,1)
          a__zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (2,2)
          a__tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          pairNs_A() = (1,1)
  
    precedence:
    
      oddNs = a__oddNs > a__oddNs# > a__pairNs = pairNs > take = a__take > pair = mark = incr = a__incr > s > zip = a__zip = a__repItems > cons > a__incr# = mark# = a__zip# > a__tail > repItems > tail = |0| = nil
    
    partial status:
  
      pi(a__oddNs#) = []
      pi(a__incr#) = [1]
      pi(a__pairNs) = []
      pi(cons) = [1]
      pi(mark#) = [1]
      pi(pair) = [1, 2]
      pi(s) = [1]
      pi(repItems) = []
      pi(tail) = []
      pi(zip) = []
      pi(a__zip#) = [1]
      pi(mark) = [1]
      pi(take) = []
      pi(oddNs) = []
      pi(incr) = [1]
      pi(a__oddNs) = []
      pi(a__incr) = [1]
      pi(a__take) = []
      pi(|0|) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = [1]
      pi(a__repItems) = [1]
      pi(pairNs) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: a__oddNs#() -> a__incr#(a__pairNs())
p2: mark#(pair(X1,X2)) -> mark#(X2)
p3: mark#(pair(X1,X2)) -> mark#(X1)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> mark#(X1)
p6: mark#(repItems(X)) -> mark#(X)
p7: mark#(tail(X)) -> mark#(X)
p8: mark#(zip(X1,X2)) -> mark#(X2)
p9: mark#(zip(X1,X2)) -> mark#(X1)
p10: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p11: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p12: mark#(take(X1,X2)) -> mark#(X2)
p13: mark#(take(X1,X2)) -> mark#(X1)
p14: mark#(oddNs()) -> a__oddNs#()
p15: mark#(incr(X)) -> mark#(X)
p16: mark#(incr(X)) -> a__incr#(mark(X))

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((1,1),(1,1)) x1 + (1,2)
          pair_A(x1,x2) = ((0,1),(1,0)) x1 + ((0,1),(1,0)) x2
          incr_A(x1) = ((0,1),(1,0)) x1
          take_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,1),(1,0)) x2 + (2,1)
          zip_A(x1,x2) = ((0,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (2,1)
          a__zip#_A(x1,x2) = ((1,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (3,2)
          mark_A(x1) = x1
          cons_A(x1,x2) = ((1,1),(1,1)) x1 + x2
          tail_A(x1) = ((1,0),(1,1)) x1 + (2,1)
          repItems_A(x1) = ((1,1),(1,1)) x1 + (2,2)
          s_A(x1) = ((0,1),(1,0)) x1
          a__pairNs_A() = (1,2)
          |0|_A() = (0,0)
          oddNs_A() = (2,1)
          a__oddNs_A() = (2,1)
          a__incr_A(x1) = ((0,1),(1,0)) x1
          a__take_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,1),(1,0)) x2 + (2,1)
          nil_A() = (1,1)
          a__zip_A(x1,x2) = ((0,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (2,1)
          a__tail_A(x1) = ((1,0),(1,1)) x1 + (2,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (2,2)
          pairNs_A() = (1,2)
  
    precedence:
    
      mark# = pair = incr = take = zip = a__zip# = mark = cons = tail = repItems = s = a__pairNs = |0| = oddNs = a__oddNs = a__incr = a__take = nil = a__zip = a__tail = a__repItems = pairNs
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = []
      pi(incr) = []
      pi(take) = []
      pi(zip) = []
      pi(a__zip#) = []
      pi(mark) = []
      pi(cons) = []
      pi(tail) = []
      pi(repItems) = []
      pi(s) = []
      pi(a__pairNs) = []
      pi(|0|) = []
      pi(oddNs) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p8

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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#(pair(X1,X2)) -> mark#(X2)
p2: mark#(pair(X1,X2)) -> mark#(X1)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(repItems(X)) -> mark#(X)
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(zip(X1,X2)) -> mark#(X1)
p8: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p9: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p10: mark#(take(X1,X2)) -> mark#(X2)
p11: mark#(take(X1,X2)) -> mark#(X1)
p12: mark#(incr(X)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((1,1),(0,0)) x1 + (3,6)
          pair_A(x1,x2) = x1 + x2
          s_A(x1) = ((0,1),(1,0)) x1
          cons_A(x1,x2) = ((0,1),(1,0)) x1 + ((0,1),(1,0)) x2
          repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          tail_A(x1) = ((1,1),(1,0)) x1 + (4,6)
          zip_A(x1,x2) = x1 + x2 + (5,5)
          a__zip#_A(x1,x2) = ((1,1),(0,0)) x1 + ((0,1),(0,0)) x2 + (4,6)
          mark_A(x1) = x1
          take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (6,6)
          incr_A(x1) = ((0,1),(1,0)) x1
          a__pairNs_A() = (1,1)
          |0|_A() = (0,0)
          oddNs_A() = (1,1)
          a__oddNs_A() = (1,1)
          a__incr_A(x1) = ((0,1),(1,0)) x1
          a__take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (6,6)
          nil_A() = (0,0)
          a__zip_A(x1,x2) = x1 + x2 + (5,5)
          a__tail_A(x1) = ((1,1),(1,0)) x1 + (4,6)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (2,1)
          pairNs_A() = (1,1)
  
    precedence:
    
      oddNs = a__oddNs > a__pairNs = pairNs > incr = a__incr > mark# = s = cons = repItems = zip = a__zip# = take = a__take = nil = a__zip = a__repItems > pair = mark > tail = a__tail > |0|
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = []
      pi(s) = []
      pi(cons) = []
      pi(repItems) = []
      pi(tail) = []
      pi(zip) = []
      pi(a__zip#) = []
      pi(mark) = [1]
      pi(take) = []
      pi(incr) = []
      pi(a__pairNs) = []
      pi(|0|) = []
      pi(oddNs) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = []
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = []
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p11

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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#(pair(X1,X2)) -> mark#(X2)
p2: mark#(incr(X)) -> mark#(X)
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p5: a__zip#(cons(X,XS),cons(Y,YS)) -> mark#(X)
p6: mark#(zip(X1,X2)) -> mark#(X1)
p7: mark#(tail(X)) -> mark#(X)
p8: mark#(repItems(X)) -> mark#(X)
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(s(X)) -> mark#(X)
p11: mark#(pair(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,0)) x1
          pair_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (1,0)
          incr_A(x1) = ((0,1),(0,1)) x1 + (1,0)
          take_A(x1,x2) = x2
          zip_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (2,2)
          a__zip#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,0)) x2 + (1,0)
          mark_A(x1) = x1
          cons_A(x1,x2) = ((0,1),(0,1)) x1 + x2
          tail_A(x1) = x1 + (1,1)
          repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          s_A(x1) = ((0,0),(0,1)) x1
          a__pairNs_A() = (4,1)
          |0|_A() = (4,0)
          oddNs_A() = (3,1)
          a__oddNs_A() = (3,1)
          a__incr_A(x1) = ((0,1),(0,1)) x1 + (1,0)
          a__take_A(x1,x2) = x2
          nil_A() = (0,0)
          a__zip_A(x1,x2) = ((1,1),(0,1)) x1 + ((1,1),(0,1)) x2 + (2,2)
          a__tail_A(x1) = x1 + (1,1)
          a__repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
          pairNs_A() = (4,1)
  
    precedence:
    
      zip = a__zip > incr = cons = repItems = a__pairNs = |0| = a__incr = a__repItems = pairNs > mark# = pair > a__zip# > mark = s > tail = a__tail > a__take > take > a__oddNs > oddNs > nil
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = []
      pi(incr) = []
      pi(take) = [2]
      pi(zip) = []
      pi(a__zip#) = []
      pi(mark) = [1]
      pi(cons) = []
      pi(tail) = [1]
      pi(repItems) = []
      pi(s) = []
      pi(a__pairNs) = []
      pi(|0|) = []
      pi(oddNs) = []
      pi(a__oddNs) = []
      pi(a__incr) = []
      pi(a__take) = [2]
      pi(nil) = []
      pi(a__zip) = []
      pi(a__tail) = [1]
      pi(a__repItems) = []
      pi(pairNs) = []

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(pair(X1,X2)) -> mark#(X2)
p2: mark#(incr(X)) -> mark#(X)
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(zip(X1,X2)) -> a__zip#(mark(X1),mark(X2))
p5: mark#(zip(X1,X2)) -> mark#(X1)
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(repItems(X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> mark#(X1)
p9: mark#(s(X)) -> mark#(X)
p10: mark#(pair(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(pair(X1,X2)) -> mark#(X2)
p2: mark#(pair(X1,X2)) -> mark#(X1)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(repItems(X)) -> mark#(X)
p6: mark#(tail(X)) -> mark#(X)
p7: mark#(zip(X1,X2)) -> mark#(X1)
p8: mark#(take(X1,X2)) -> mark#(X2)
p9: mark#(incr(X)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2)
          pair_A(x1,x2) = ((0,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,2)
          s_A(x1) = ((0,0),(0,1)) x1 + (1,1)
          cons_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (1,1)
          repItems_A(x1) = x1 + (1,1)
          tail_A(x1) = x1 + (0,1)
          zip_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
          incr_A(x1) = ((0,0),(0,1)) x1 + (3,1)
  
    precedence:
    
      pair > mark# = repItems = tail = zip = take > s = cons = incr
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = [2]
      pi(s) = []
      pi(cons) = []
      pi(repItems) = [1]
      pi(tail) = [1]
      pi(zip) = []
      pi(take) = [2]
      pi(incr) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(pair(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(cons(X1,X2)) -> mark#(X1)
p4: mark#(repItems(X)) -> mark#(X)
p5: mark#(tail(X)) -> mark#(X)
p6: mark#(zip(X1,X2)) -> mark#(X1)
p7: mark#(take(X1,X2)) -> mark#(X2)
p8: mark#(incr(X)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(pair(X1,X2)) -> mark#(X1)
p2: mark#(incr(X)) -> mark#(X)
p3: mark#(take(X1,X2)) -> mark#(X2)
p4: mark#(zip(X1,X2)) -> mark#(X1)
p5: mark#(tail(X)) -> mark#(X)
p6: mark#(repItems(X)) -> mark#(X)
p7: mark#(cons(X1,X2)) -> mark#(X1)
p8: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((1,1),(0,0)) x1 + (2,2)
          pair_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (1,1)
          incr_A(x1) = x1 + (1,1)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,0)) x2 + (0,1)
          zip_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(1,1)) x2 + (0,1)
          tail_A(x1) = x1 + (0,1)
          repItems_A(x1) = ((0,0),(1,1)) x1 + (1,1)
          cons_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (0,1)
          s_A(x1) = ((0,0),(1,1)) x1 + (1,1)
  
    precedence:
    
      take = tail > pair = repItems > mark# = zip = cons > incr = s
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = [2]
      pi(incr) = []
      pi(take) = []
      pi(zip) = []
      pi(tail) = [1]
      pi(repItems) = []
      pi(cons) = [2]
      pi(s) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,1)) x1 + (2,2)
          pair_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
          s_A(x1) = ((1,1),(1,1)) x1 + (3,2)
          cons_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
          repItems_A(x1) = ((0,0),(0,1)) x1 + (1,1)
          tail_A(x1) = x1 + (1,1)
          zip_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (3,1)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(0,1)) x2 + (3,1)
  
    precedence:
    
      zip > pair = take > cons > tail > mark# = s > repItems
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = [2]
      pi(s) = []
      pi(cons) = [2]
      pi(repItems) = []
      pi(tail) = []
      pi(zip) = []
      pi(take) = []

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,1)) x1 + (2,2)
          pair_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,2)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
          zip_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
          tail_A(x1) = x1 + (1,1)
          repItems_A(x1) = x1 + (1,1)
          s_A(x1) = ((0,0),(0,1)) x1 + (1,1)
  
    precedence:
    
      take = zip > mark# = pair = s > tail = repItems
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = []
      pi(take) = [2]
      pi(zip) = [2]
      pi(tail) = [1]
      pi(repItems) = [1]
      pi(s) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((1,1),(0,0)) x1 + (2,1)
          pair_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (1,0)
          s_A(x1) = ((1,1),(1,1)) x1 + (3,1)
          repItems_A(x1) = ((0,1),(1,0)) x1 + (1,0)
          zip_A(x1,x2) = ((0,1),(1,0)) x1 + ((1,1),(1,1)) x2 + (1,0)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 + (1,0)
  
    precedence:
    
      repItems = zip = take > mark# = pair > s
    
    partial status:
  
      pi(mark#) = []
      pi(pair) = [1, 2]
      pi(s) = []
      pi(repItems) = []
      pi(zip) = [2]
      pi(take) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,1)) x1 + (2,2)
          s_A(x1) = x1 + (3,1)
          take_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
          zip_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (3,1)
          repItems_A(x1) = ((0,0),(0,1)) x1 + (1,1)
  
    precedence:
    
      zip > mark# > s = take = repItems
    
    partial status:
  
      pi(mark#) = []
      pi(s) = [1]
      pi(take) = [2]
      pi(zip) = [2]
      pi(repItems) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((0,1),(0,0)) x1 + (2,2)
          s_A(x1) = ((0,0),(0,1)) x1 + (1,1)
          repItems_A(x1) = ((0,0),(0,1)) x1 + (3,1)
          zip_A(x1,x2) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + (3,1)
  
    precedence:
    
      s = repItems > mark# = zip
    
    partial status:
  
      pi(mark#) = []
      pi(s) = []
      pi(repItems) = []
      pi(zip) = [2]

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = ((1,0),(1,0)) x1 + (2,2)
          s_A(x1) = ((1,0),(0,0)) x1 + (1,1)
          zip_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,1),(1,1)) x2 + (1,1)
  
    precedence:
    
      mark# = s = zip
    
    partial status:
  
      pi(mark#) = []
      pi(s) = []
      pi(zip) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(zip(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: mark#(zip(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__pairNs() -> cons(|0|(),incr(oddNs()))
r2: a__oddNs() -> a__incr(a__pairNs())
r3: a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
r4: a__take(|0|(),XS) -> nil()
r5: a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
r6: a__zip(nil(),XS) -> nil()
r7: a__zip(X,nil()) -> nil()
r8: a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
r9: a__tail(cons(X,XS)) -> mark(XS)
r10: a__repItems(nil()) -> nil()
r11: a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
r12: mark(pairNs()) -> a__pairNs()
r13: mark(incr(X)) -> a__incr(mark(X))
r14: mark(oddNs()) -> a__oddNs()
r15: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r16: mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
r17: mark(tail(X)) -> a__tail(mark(X))
r18: mark(repItems(X)) -> a__repItems(mark(X))
r19: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r20: mark(|0|()) -> |0|()
r21: mark(s(X)) -> s(mark(X))
r22: mark(nil()) -> nil()
r23: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r24: a__pairNs() -> pairNs()
r25: a__incr(X) -> incr(X)
r26: a__oddNs() -> oddNs()
r27: a__take(X1,X2) -> take(X1,X2)
r28: a__zip(X1,X2) -> zip(X1,X2)
r29: a__tail(X) -> tail(X)
r30: a__repItems(X) -> repItems(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          mark#_A(x1) = x1 + (1,1)
          zip_A(x1,x2) = x1 + ((1,1),(1,1)) x2 + (2,1)
  
    precedence:
    
      zip > mark#
    
    partial status:
  
      pi(mark#) = [1]
      pi(zip) = [1, 2]

The next rules are strictly ordered:

  p1

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