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

-- SCC decomposition.

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

p1: active#(pairNs()) -> cons#(|0|(),incr(oddNs()))
p2: active#(pairNs()) -> incr#(oddNs())
p3: active#(oddNs()) -> incr#(pairNs())
p4: active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
p5: active#(incr(cons(X,XS))) -> s#(X)
p6: active#(incr(cons(X,XS))) -> incr#(XS)
p7: active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
p8: active#(take(s(N),cons(X,XS))) -> take#(N,XS)
p9: active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
p10: active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
p11: active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
p12: active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
p13: active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
p14: active#(repItems(cons(X,XS))) -> repItems#(XS)
p15: active#(cons(X1,X2)) -> cons#(active(X1),X2)
p16: active#(cons(X1,X2)) -> active#(X1)
p17: active#(incr(X)) -> incr#(active(X))
p18: active#(incr(X)) -> active#(X)
p19: active#(s(X)) -> s#(active(X))
p20: active#(s(X)) -> active#(X)
p21: active#(take(X1,X2)) -> take#(active(X1),X2)
p22: active#(take(X1,X2)) -> active#(X1)
p23: active#(take(X1,X2)) -> take#(X1,active(X2))
p24: active#(take(X1,X2)) -> active#(X2)
p25: active#(zip(X1,X2)) -> zip#(active(X1),X2)
p26: active#(zip(X1,X2)) -> active#(X1)
p27: active#(zip(X1,X2)) -> zip#(X1,active(X2))
p28: active#(zip(X1,X2)) -> active#(X2)
p29: active#(pair(X1,X2)) -> pair#(active(X1),X2)
p30: active#(pair(X1,X2)) -> active#(X1)
p31: active#(pair(X1,X2)) -> pair#(X1,active(X2))
p32: active#(pair(X1,X2)) -> active#(X2)
p33: active#(tail(X)) -> tail#(active(X))
p34: active#(tail(X)) -> active#(X)
p35: active#(repItems(X)) -> repItems#(active(X))
p36: active#(repItems(X)) -> active#(X)
p37: cons#(mark(X1),X2) -> cons#(X1,X2)
p38: incr#(mark(X)) -> incr#(X)
p39: s#(mark(X)) -> s#(X)
p40: take#(mark(X1),X2) -> take#(X1,X2)
p41: take#(X1,mark(X2)) -> take#(X1,X2)
p42: zip#(mark(X1),X2) -> zip#(X1,X2)
p43: zip#(X1,mark(X2)) -> zip#(X1,X2)
p44: pair#(mark(X1),X2) -> pair#(X1,X2)
p45: pair#(X1,mark(X2)) -> pair#(X1,X2)
p46: tail#(mark(X)) -> tail#(X)
p47: repItems#(mark(X)) -> repItems#(X)
p48: proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
p49: proper#(cons(X1,X2)) -> proper#(X1)
p50: proper#(cons(X1,X2)) -> proper#(X2)
p51: proper#(incr(X)) -> incr#(proper(X))
p52: proper#(incr(X)) -> proper#(X)
p53: proper#(s(X)) -> s#(proper(X))
p54: proper#(s(X)) -> proper#(X)
p55: proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
p56: proper#(take(X1,X2)) -> proper#(X1)
p57: proper#(take(X1,X2)) -> proper#(X2)
p58: proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
p59: proper#(zip(X1,X2)) -> proper#(X1)
p60: proper#(zip(X1,X2)) -> proper#(X2)
p61: proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
p62: proper#(pair(X1,X2)) -> proper#(X1)
p63: proper#(pair(X1,X2)) -> proper#(X2)
p64: proper#(tail(X)) -> tail#(proper(X))
p65: proper#(tail(X)) -> proper#(X)
p66: proper#(repItems(X)) -> repItems#(proper(X))
p67: proper#(repItems(X)) -> proper#(X)
p68: cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
p69: incr#(ok(X)) -> incr#(X)
p70: s#(ok(X)) -> s#(X)
p71: take#(ok(X1),ok(X2)) -> take#(X1,X2)
p72: zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
p73: pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
p74: tail#(ok(X)) -> tail#(X)
p75: repItems#(ok(X)) -> repItems#(X)
p76: top#(mark(X)) -> top#(proper(X))
p77: top#(mark(X)) -> proper#(X)
p78: top#(ok(X)) -> top#(active(X))
p79: top#(ok(X)) -> active#(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p76, p78}
  {p16, p18, p20, p22, p24, p26, p28, p30, p32, p34, p36}
  {p49, p50, p52, p54, p56, p57, p59, p60, p62, p63, p65, p67}
  {p37, p68}
  {p39, p70}
  {p38, p69}
  {p40, p41, p71}
  {p44, p45, p73}
  {p42, p43, p72}
  {p47, p75}
  {p46, p74}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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, r48, r49, r50, r51, r52, r53

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        top#_A(x1) = ((1,0),(1,0)) x1
        ok_A(x1) = x1
        active_A(x1) = x1
        mark_A(x1) = x1
        proper_A(x1) = x1
        cons_A(x1,x2) = ((1,0),(1,0)) x1 + x2
        incr_A(x1) = ((1,0),(1,0)) x1 + (0,1)
        s_A(x1) = x1 + (0,1)
        take_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (2,1)
        zip_A(x1,x2) = x1 + x2 + (1,1)
        pair_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (0,1)
        tail_A(x1) = x1 + (1,1)
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        pairNs_A() = (1,2)
        |0|_A() = (0,1)
        oddNs_A() = (1,2)
        nil_A() = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        top#_A(x1) = ((0,1),(0,0)) x1
        ok_A(x1) = x1
        active_A(x1) = x1
        mark_A(x1) = ((0,0),(1,1)) x1 + (0,3)
        proper_A(x1) = ((0,1),(0,1)) x1 + (1,0)
        cons_A(x1,x2) = x1 + (0,1)
        incr_A(x1) = x1 + (0,3)
        s_A(x1) = x1
        take_A(x1,x2) = x1 + x2 + (0,3)
        zip_A(x1,x2) = x1 + x2 + (0,3)
        pair_A(x1,x2) = x1 + x2 + (0,1)
        tail_A(x1) = x1 + (0,1)
        repItems_A(x1) = x1 + (0,3)
        pairNs_A() = (1,5)
        |0|_A() = (0,1)
        oddNs_A() = (1,12)
        nil_A() = (1,1)
    

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: top#(ok(X)) -> top#(active(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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, r46, r47, r48, r49, r50, r51, r52, r53

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        top#_A(x1) = ((1,1),(0,0)) x1
        ok_A(x1) = ((0,1),(1,0)) x1 + (1,2)
        active_A(x1) = x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x2 + (0,1)
        mark_A(x1) = (0,1)
        incr_A(x1) = x1 + (1,1)
        s_A(x1) = x1 + (1,1)
        take_A(x1,x2) = x1 + (1,1)
        zip_A(x1,x2) = x1 + ((0,1),(1,0)) x2 + (0,1)
        pair_A(x1,x2) = ((0,1),(1,0)) x2 + (1,2)
        tail_A(x1) = x1 + (1,1)
        repItems_A(x1) = ((0,1),(1,0)) x1 + (1,2)
        pairNs_A() = (1,1)
        |0|_A() = (1,1)
        oddNs_A() = (1,1)
        nil_A() = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        top#_A(x1) = ((1,0),(1,1)) x1
        ok_A(x1) = (3,5)
        active_A(x1) = (5,7)
        cons_A(x1,x2) = ((0,0),(1,0)) x2 + (2,1)
        mark_A(x1) = (1,1)
        incr_A(x1) = (4,5)
        s_A(x1) = x1 + (0,5)
        take_A(x1,x2) = ((0,0),(1,0)) x1 + (4,2)
        zip_A(x1,x2) = (4,4)
        pair_A(x1,x2) = (4,7)
        tail_A(x1) = x1 + (4,0)
        repItems_A(x1) = (3,7)
        pairNs_A() = (1,1)
        |0|_A() = (1,1)
        oddNs_A() = (1,1)
        nil_A() = (1,1)
    

The next rules are strictly ordered:

  p1

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: active#(repItems(X)) -> active#(X)
p2: active#(tail(X)) -> active#(X)
p3: active#(pair(X1,X2)) -> active#(X2)
p4: active#(pair(X1,X2)) -> active#(X1)
p5: active#(zip(X1,X2)) -> active#(X2)
p6: active#(zip(X1,X2)) -> active#(X1)
p7: active#(take(X1,X2)) -> active#(X2)
p8: active#(take(X1,X2)) -> active#(X1)
p9: active#(s(X)) -> active#(X)
p10: active#(incr(X)) -> active#(X)
p11: active#(cons(X1,X2)) -> active#(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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:
        active#_A(x1) = ((1,1),(1,1)) x1
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        pair_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        s_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        incr_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((1,1),(1,0)) x1
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        pair_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        zip_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        s_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        incr_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11
  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, r48, r49, r50, r51, r52, r53, r54, r55

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: proper#(repItems(X)) -> proper#(X)
p2: proper#(tail(X)) -> proper#(X)
p3: proper#(pair(X1,X2)) -> proper#(X2)
p4: proper#(pair(X1,X2)) -> proper#(X1)
p5: proper#(zip(X1,X2)) -> proper#(X2)
p6: proper#(zip(X1,X2)) -> proper#(X1)
p7: proper#(take(X1,X2)) -> proper#(X2)
p8: proper#(take(X1,X2)) -> proper#(X1)
p9: proper#(s(X)) -> proper#(X)
p10: proper#(incr(X)) -> proper#(X)
p11: proper#(cons(X1,X2)) -> proper#(X2)
p12: proper#(cons(X1,X2)) -> proper#(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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:
        proper#_A(x1) = ((1,1),(0,0)) x1
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        pair_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        zip_A(x1,x2) = ((0,1),(1,0)) x1 + ((1,1),(1,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        s_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        incr_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        proper#_A(x1) = ((1,1),(1,1)) x1
        repItems_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        tail_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        pair_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
        zip_A(x1,x2) = ((1,1),(1,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
        s_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        incr_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(ok(X1),ok(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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:
        cons#_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(0,0)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        cons#_A(x1,x2) = ((0,1),(0,0)) x1 + ((1,0),(1,1)) x2
        mark_A(x1) = x1 + (1,1)
        ok_A(x1) = ((0,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: s#(mark(X)) -> s#(X)
p2: s#(ok(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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,0)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        s#_A(x1) = ((0,1),(1,0)) x1
        mark_A(x1) = ((1,0),(1,0)) x1 + (1,1)
        ok_A(x1) = ((0,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#(ok(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        incr#_A(x1) = ((1,1),(0,1)) x1
        mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
        ok_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#(ok(X1),ok(X2)) -> take#(X1,X2)
p3: 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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        take#_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3

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

-- Reduction pair.

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

p1: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
p3: 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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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),(0,0)) x1 + ((1,1),(1,0)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        pair#_A(x1,x2) = x1 + ((1,1),(1,0)) x2
        mark_A(x1) = ((1,1),(1,0)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,0)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3
  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, r48, r49, r50, r51, r52, r53, r54, r55

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#(ok(X1),ok(X2)) -> zip#(X1,X2)
p3: 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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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:
        zip#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        zip#_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3

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

-- Reduction pair.

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

p1: repItems#(mark(X)) -> repItems#(X)
p2: repItems#(ok(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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,0),(1,0)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        repItems#_A(x1) = x1
        mark_A(x1) = ((0,0),(1,0)) x1 + (1,1)
        ok_A(x1) = ((0,0),(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#(ok(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: active(cons(X1,X2)) -> cons(active(X1),X2)
r13: active(incr(X)) -> incr(active(X))
r14: active(s(X)) -> s(active(X))
r15: active(take(X1,X2)) -> take(active(X1),X2)
r16: active(take(X1,X2)) -> take(X1,active(X2))
r17: active(zip(X1,X2)) -> zip(active(X1),X2)
r18: active(zip(X1,X2)) -> zip(X1,active(X2))
r19: active(pair(X1,X2)) -> pair(active(X1),X2)
r20: active(pair(X1,X2)) -> pair(X1,active(X2))
r21: active(tail(X)) -> tail(active(X))
r22: active(repItems(X)) -> repItems(active(X))
r23: cons(mark(X1),X2) -> mark(cons(X1,X2))
r24: incr(mark(X)) -> mark(incr(X))
r25: s(mark(X)) -> mark(s(X))
r26: take(mark(X1),X2) -> mark(take(X1,X2))
r27: take(X1,mark(X2)) -> mark(take(X1,X2))
r28: zip(mark(X1),X2) -> mark(zip(X1,X2))
r29: zip(X1,mark(X2)) -> mark(zip(X1,X2))
r30: pair(mark(X1),X2) -> mark(pair(X1,X2))
r31: pair(X1,mark(X2)) -> mark(pair(X1,X2))
r32: tail(mark(X)) -> mark(tail(X))
r33: repItems(mark(X)) -> mark(repItems(X))
r34: proper(pairNs()) -> ok(pairNs())
r35: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r36: proper(|0|()) -> ok(|0|())
r37: proper(incr(X)) -> incr(proper(X))
r38: proper(oddNs()) -> ok(oddNs())
r39: proper(s(X)) -> s(proper(X))
r40: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
r41: proper(nil()) -> ok(nil())
r42: proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
r43: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
r44: proper(tail(X)) -> tail(proper(X))
r45: proper(repItems(X)) -> repItems(proper(X))
r46: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r47: incr(ok(X)) -> ok(incr(X))
r48: s(ok(X)) -> ok(s(X))
r49: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
r50: zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
r51: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
r52: tail(ok(X)) -> ok(tail(X))
r53: repItems(ok(X)) -> ok(repItems(X))
r54: top(mark(X)) -> top(proper(X))
r55: top(ok(X)) -> top(active(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:
        tail#_A(x1) = ((1,1),(1,0)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,1),(1,1)) x1 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        tail#_A(x1) = ((0,1),(1,1)) x1
        mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        ok_A(x1) = ((1,0),(1,1)) x1 + (1,1)
    

The next rules are strictly ordered:

  p1, p2

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