YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = max{0, x1 - 10}
    pairNs_A = 5
    mark#_A(x1) = max{0, x1 - 10}
    cons_A(x1,x2) = max{5, x1 + 2, x2 - 12}
    |0|_A = 2
    incr_A(x1) = max{10, x1 + 5}
    oddNs_A = 10
    repItems_A(x1) = max{11, x1}
    mark_A(x1) = max{1, x1}
    tail_A(x1) = max{14, x1 + 12}
    pair_A(x1,x2) = max{12, x1 + 11, x2}
    zip_A(x1,x2) = max{30, x1 + 29, x2 + 27}
    take_A(x1,x2) = max{24, x1 + 23, x2 + 23}
    s_A(x1) = max{3, x1 + 2}
    active_A(x1) = max{2, x1}
    nil_A = 3

The next rules are strictly ordered:

  p6, p10, p13, p14, p17, p18

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = x1 + 20
    pairNs_A = 108
    mark#_A(x1) = 128
    cons_A(x1,x2) = 108
    |0|_A = 89
    incr_A(x1) = 108
    oddNs_A = 108
    mark_A(x1) = 103
    s_A(x1) = 108
    take_A(x1,x2) = 108
    zip_A(x1,x2) = 108
    pair_A(x1,x2) = 105
    tail_A(x1) = 108
    repItems_A(x1) = 108
    active_A(x1) = 103
    nil_A = 106

The next rules are strictly ordered:

  p16

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = x1 + 9
    pairNs_A = 12
    mark#_A(x1) = x1 + 9
    cons_A(x1,x2) = max{11, x1 + 1, x2 - 8}
    |0|_A = 2
    incr_A(x1) = x1 + 4
    oddNs_A = 16
    repItems_A(x1) = x1 + 20
    mark_A(x1) = x1
    tail_A(x1) = x1 + 9
    pair_A(x1,x2) = max{21, x1 + 20, x2 + 20}
    zip_A(x1,x2) = max{x1 + 20, x2 + 20}
    take_A(x1,x2) = max{x1 + 19, x2 + 20}
    s_A(x1) = x1 + 2
    active_A(x1) = max{2, x1}
    nil_A = 3

The next rules are strictly ordered:

  p2, p3, p5, p7, p8, p13, p16

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = 0
    pairNs_A = 147
    mark#_A(x1) = max{0, x1 - 148}
    cons_A(x1,x2) = 146
    |0|_A = 146
    incr_A(x1) = 148
    oddNs_A = 146
    mark_A(x1) = 117
    s_A(x1) = 148
    take_A(x1,x2) = 148
    zip_A(x1,x2) = 148
    pair_A(x1,x2) = 156
    tail_A(x1) = 146
    repItems_A(x1) = 149
    active_A(x1) = 117
    nil_A = 156

The next rules are strictly ordered:

  p14

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = x1 + 6
    pairNs_A = 10
    mark#_A(x1) = max{15, x1 + 6}
    cons_A(x1,x2) = max{7, x1 - 5, x2 - 5}
    |0|_A = 7
    incr_A(x1) = x1 + 2
    oddNs_A = 12
    mark_A(x1) = x1
    zip_A(x1,x2) = max{x1 + 13, x2 + 13}
    pair_A(x1,x2) = max{x1 + 12, x2 + 12}
    tail_A(x1) = x1 + 10
    take_A(x1,x2) = max{x1 + 14, x2 + 15}
    s_A(x1) = x1 + 2
    active_A(x1) = max{1, x1}
    nil_A = 2
    repItems_A(x1) = x1 + 12

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{0, x1 - 2}
    cons_A(x1,x2) = max{6, x2 - 8}
    active#_A(x1) = max{4, x1 - 2}
    mark_A(x1) = x1
    oddNs_A = 6
    incr_A(x1) = 6
    pairNs_A = 6
    s_A(x1) = x1 + 8
    take_A(x1,x2) = x1 + 23
    zip_A(x1,x2) = max{12, x1 + 11, x2 - 1}
    pair_A(x1,x2) = max{x1 + 2, x2 + 2}
    tail_A(x1) = x1 + 8
    active_A(x1) = max{2, x1}
    |0|_A = 25
    nil_A = 12
    repItems_A(x1) = x1 + 19

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{26, x1 + 10}
    cons_A(x1,x2) = max{x1 + 12, x2 - 9}
    active#_A(x1) = x1 + 10
    mark_A(x1) = x1
    zip_A(x1,x2) = max{x1 + 24, x2 + 24}
    pair_A(x1,x2) = max{x1 + 2, x2 + 2}
    tail_A(x1) = x1 + 17
    incr_A(x1) = x1 + 4
    s_A(x1) = x1 + 4
    oddNs_A = 19
    pairNs_A = 14
    take_A(x1,x2) = max{x1 + 20, x2 + 21}
    active_A(x1) = max{2, x1}
    |0|_A = 2
    nil_A = 3
    repItems_A(x1) = x1 + 21

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: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(tail(X)) -> active#(tail(mark(X)))
p4: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p5: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p6: mark#(incr(X)) -> active#(incr(mark(X)))
p7: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p8: mark#(s(X)) -> active#(s(mark(X)))
p9: mark#(oddNs()) -> active#(oddNs())

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{32, x1 - 3}
    cons_A(x1,x2) = max{29, x2 - 12}
    active#_A(x1) = max{0, x1 - 3}
    mark_A(x1) = x1
    incr_A(x1) = x1 + 6
    s_A(x1) = x1 + 4
    zip_A(x1,x2) = max{36, x1 + 17, x2 + 17}
    pair_A(x1,x2) = max{x1 + 3, x2 + 3}
    take_A(x1,x2) = 29
    tail_A(x1) = x1 + 36
    active_A(x1) = max{2, x1}
    pairNs_A = 29
    |0|_A = 2
    oddNs_A = 35
    nil_A = 17
    repItems_A(x1) = x1 + 27

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(incr(cons(X,XS))) -> mark#(cons(s(X),incr(XS)))
p3: mark#(s(X)) -> active#(s(mark(X)))
p4: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p5: mark#(incr(X)) -> active#(incr(mark(X)))
p6: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p7: mark#(tail(X)) -> active#(tail(mark(X)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{1, x1 - 10}
    cons_A(x1,x2) = max{8, x1 - 8, x2 - 6}
    active#_A(x1) = max{0, x1 - 10}
    mark_A(x1) = x1
    zip_A(x1,x2) = max{x1 + 15, x2 + 15}
    pair_A(x1,x2) = max{x1 + 15, x2 + 15}
    tail_A(x1) = x1 + 12
    incr_A(x1) = x1 + 3
    s_A(x1) = 2
    active_A(x1) = max{1, x1}
    pairNs_A = 8
    |0|_A = 10
    oddNs_A = 11
    take_A(x1,x2) = x2 + 16
    nil_A = 2
    repItems_A(x1) = x1 + 14

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{13, x1 + 9}
    cons_A(x1,x2) = max{5, x2 - 2}
    active#_A(x1) = x1 + 9
    mark_A(x1) = x1
    incr_A(x1) = 13
    s_A(x1) = x1 + 10
    zip_A(x1,x2) = max{x1 + 14, x2 + 14}
    pair_A(x1,x2) = max{x1 + 10, x2 + 10}
    tail_A(x1) = x1 + 5
    active_A(x1) = max{1, x1}
    pairNs_A = 11
    |0|_A = 10
    oddNs_A = 16
    take_A(x1,x2) = max{x1 + 5, x2 + 7}
    nil_A = 2
    repItems_A(x1) = x1 + 7

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: mark#(incr(X)) -> active#(incr(mark(X)))
p3: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p4: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p5: mark#(tail(X)) -> active#(tail(mark(X)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(tail(X)) -> active#(tail(mark(X)))
p4: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p5: mark#(incr(X)) -> active#(incr(mark(X)))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{9, x1}
    cons_A(x1,x2) = max{4, x2 - 2}
    active#_A(x1) = max{3, x1}
    mark_A(x1) = x1
    zip_A(x1,x2) = max{x1 + 12, x2 + 12}
    pair_A(x1,x2) = max{x1 + 24, x2 + 24}
    tail_A(x1) = x1 + 10
    incr_A(x1) = 8
    active_A(x1) = max{1, x1}
    pairNs_A = 7
    |0|_A = 15
    oddNs_A = 8
    s_A(x1) = x1 + 19
    take_A(x1,x2) = max{x1 + 8, x2 + 9}
    nil_A = 7
    repItems_A(x1) = x1 + 6

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(tail(X)) -> active#(tail(mark(X)))
p4: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))
p4: mark#(tail(X)) -> active#(tail(mark(X)))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{45, x1}
    cons_A(x1,x2) = max{25, x2 - 20}
    active#_A(x1) = 45
    mark_A(x1) = x1 + 9
    zip_A(x1,x2) = 44
    pair_A(x1,x2) = max{x1 + 83, x2 + 84}
    tail_A(x1) = max{51, x1 + 47}
    active_A(x1) = max{13, x1}
    pairNs_A = 37
    |0|_A = 52
    incr_A(x1) = 38
    oddNs_A = 47
    s_A(x1) = max{65, x1 + 56}
    take_A(x1,x2) = max{38, x1 + 29}
    nil_A = 9
    repItems_A(x1) = x1 + 54

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))
p3: mark#(zip(X1,X2)) -> active#(zip(mark(X1),mark(X2)))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{0, x1 - 8}
    cons_A(x1,x2) = max{8, x2 - 4}
    active#_A(x1) = max{0, x1 - 14}
    mark_A(x1) = max{7, x1 + 5}
    zip_A(x1,x2) = 12
    pair_A(x1,x2) = max{12, x1 + 8, x2 + 10}
    active_A(x1) = max{13, x1}
    pairNs_A = 19
    |0|_A = 16
    incr_A(x1) = 12
    oddNs_A = 17
    s_A(x1) = max{14, x1 + 9}
    take_A(x1,x2) = max{13, x1 + 8}
    nil_A = 8
    tail_A(x1) = max{13, x1 + 11}
    repItems_A(x1) = 17

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p2: active#(zip(cons(X,XS),cons(Y,YS))) -> mark#(cons(pair(X,Y),zip(XS,YS)))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = x1 + 3
    cons_A(x1,x2) = max{3, x2 - 1}
    active#_A(x1) = x1 + 3
    mark_A(x1) = x1
    zip_A(x1,x2) = 16
    pair_A(x1,x2) = max{x1 + 10, x2 + 10}
    active_A(x1) = max{1, x1}
    pairNs_A = 3
    |0|_A = 3
    incr_A(x1) = 3
    oddNs_A = 6
    s_A(x1) = x1 + 8
    take_A(x1,x2) = max{x1 + 3, x2 + 4}
    nil_A = 2
    tail_A(x1) = x1 + 1
    repItems_A(x1) = x1 + 4

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#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(X1,mark(X2)) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)
p3: cons#(X1,active(X2)) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: cons#(mark(X1),X2) -> cons#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    s#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 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: s#(mark(X)) -> s#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: s#(mark(X)) -> s#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    s#_A(x1) = x1
    mark_A(x1) = x1 + 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: incr#(mark(X)) -> incr#(X)
p2: incr#(active(X)) -> incr#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    incr#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 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: incr#(mark(X)) -> incr#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: incr#(mark(X)) -> incr#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    incr#_A(x1) = x1
    mark_A(x1) = x1 + 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: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(X1,active(X2)) -> take#(X1,X2)
p3: take#(active(X1),X2) -> take#(X1,X2)
p4: take#(X1,mark(X2)) -> take#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    take#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(X1,active(X2)) -> take#(X1,X2)
p3: take#(active(X1),X2) -> take#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(active(X1),X2) -> take#(X1,X2)
p3: take#(X1,active(X2)) -> take#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    take#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

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: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(active(X1),X2) -> take#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: take#(mark(X1),X2) -> take#(X1,X2)
p2: take#(active(X1),X2) -> take#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    take#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: take#(mark(X1),X2) -> take#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    take#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(X1,active(X2)) -> pair#(X1,X2)
p3: pair#(active(X1),X2) -> pair#(X1,X2)
p4: pair#(X1,mark(X2)) -> pair#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    pair#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(X1,active(X2)) -> pair#(X1,X2)
p3: pair#(active(X1),X2) -> pair#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(active(X1),X2) -> pair#(X1,X2)
p3: pair#(X1,active(X2)) -> pair#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    pair#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

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: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(active(X1),X2) -> pair#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: pair#(mark(X1),X2) -> pair#(X1,X2)
p2: pair#(active(X1),X2) -> pair#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    pair#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: pair#(mark(X1),X2) -> pair#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    pair#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: zip#(mark(X1),X2) -> zip#(X1,X2)
p2: zip#(X1,active(X2)) -> zip#(X1,X2)
p3: zip#(active(X1),X2) -> zip#(X1,X2)
p4: zip#(X1,mark(X2)) -> zip#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    zip#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: zip#(mark(X1),X2) -> zip#(X1,X2)
p2: zip#(X1,active(X2)) -> zip#(X1,X2)
p3: zip#(active(X1),X2) -> zip#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    zip#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

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: zip#(mark(X1),X2) -> zip#(X1,X2)
p2: zip#(active(X1),X2) -> zip#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    zip#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: zip#(mark(X1),X2) -> zip#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    zip#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: repItems#(mark(X)) -> repItems#(X)
p2: repItems#(active(X)) -> repItems#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    repItems#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 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: repItems#(mark(X)) -> repItems#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: repItems#(mark(X)) -> repItems#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    repItems#_A(x1) = x1
    mark_A(x1) = x1 + 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: tail#(mark(X)) -> tail#(X)
p2: tail#(active(X)) -> tail#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    tail#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 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: tail#(mark(X)) -> tail#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: tail#(mark(X)) -> tail#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    tail#_A(x1) = x1
    mark_A(x1) = x1 + 1

The next rules are strictly ordered:

  p1

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