YES

We show the termination of the TRS R:

  active(and(tt(),T)) -> mark(T)
  active(isNatIList(IL)) -> mark(isNatList(IL))
  active(isNat(|0|())) -> mark(tt())
  active(isNat(s(N))) -> mark(isNat(N))
  active(isNat(length(L))) -> mark(isNatList(L))
  active(isNatIList(zeros())) -> mark(tt())
  active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
  active(isNatList(nil())) -> mark(tt())
  active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
  active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
  active(zeros()) -> mark(cons(|0|(),zeros()))
  active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
  active(uTake1(tt())) -> mark(nil())
  active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
  active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
  active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
  active(uLength(tt(),L)) -> mark(s(length(L)))
  mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
  mark(tt()) -> active(tt())
  mark(isNatIList(X)) -> active(isNatIList(X))
  mark(isNatList(X)) -> active(isNatList(X))
  mark(isNat(X)) -> active(isNat(X))
  mark(|0|()) -> active(|0|())
  mark(s(X)) -> active(s(mark(X)))
  mark(length(X)) -> active(length(mark(X)))
  mark(zeros()) -> active(zeros())
  mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
  mark(nil()) -> active(nil())
  mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
  mark(uTake1(X)) -> active(uTake1(mark(X)))
  mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
  mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
  and(mark(X1),X2) -> and(X1,X2)
  and(X1,mark(X2)) -> and(X1,X2)
  and(active(X1),X2) -> and(X1,X2)
  and(X1,active(X2)) -> and(X1,X2)
  isNatIList(mark(X)) -> isNatIList(X)
  isNatIList(active(X)) -> isNatIList(X)
  isNatList(mark(X)) -> isNatList(X)
  isNatList(active(X)) -> isNatList(X)
  isNat(mark(X)) -> isNat(X)
  isNat(active(X)) -> isNat(X)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  length(mark(X)) -> length(X)
  length(active(X)) -> length(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)
  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)
  uTake1(mark(X)) -> uTake1(X)
  uTake1(active(X)) -> uTake1(X)
  uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
  uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
  uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
  uLength(mark(X1),X2) -> uLength(X1,X2)
  uLength(X1,mark(X2)) -> uLength(X1,X2)
  uLength(active(X1),X2) -> uLength(X1,X2)
  uLength(X1,active(X2)) -> uLength(X1,X2)

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p3: active#(isNatIList(IL)) -> isNatList#(IL)
p4: active#(isNat(|0|())) -> mark#(tt())
p5: active#(isNat(s(N))) -> mark#(isNat(N))
p6: active#(isNat(s(N))) -> isNat#(N)
p7: active#(isNat(length(L))) -> mark#(isNatList(L))
p8: active#(isNat(length(L))) -> isNatList#(L)
p9: active#(isNatIList(zeros())) -> mark#(tt())
p10: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p11: active#(isNatIList(cons(N,IL))) -> and#(isNat(N),isNatIList(IL))
p12: active#(isNatIList(cons(N,IL))) -> isNat#(N)
p13: active#(isNatIList(cons(N,IL))) -> isNatIList#(IL)
p14: active#(isNatList(nil())) -> mark#(tt())
p15: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p16: active#(isNatList(cons(N,L))) -> and#(isNat(N),isNatList(L))
p17: active#(isNatList(cons(N,L))) -> isNat#(N)
p18: active#(isNatList(cons(N,L))) -> isNatList#(L)
p19: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p20: active#(isNatList(take(N,IL))) -> and#(isNat(N),isNatIList(IL))
p21: active#(isNatList(take(N,IL))) -> isNat#(N)
p22: active#(isNatList(take(N,IL))) -> isNatIList#(IL)
p23: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p24: active#(zeros()) -> cons#(|0|(),zeros())
p25: active#(take(|0|(),IL)) -> mark#(uTake1(isNatIList(IL)))
p26: active#(take(|0|(),IL)) -> uTake1#(isNatIList(IL))
p27: active#(take(|0|(),IL)) -> isNatIList#(IL)
p28: active#(uTake1(tt())) -> mark#(nil())
p29: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p30: active#(take(s(M),cons(N,IL))) -> uTake2#(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL)
p31: active#(take(s(M),cons(N,IL))) -> and#(isNat(M),and(isNat(N),isNatIList(IL)))
p32: active#(take(s(M),cons(N,IL))) -> isNat#(M)
p33: active#(take(s(M),cons(N,IL))) -> and#(isNat(N),isNatIList(IL))
p34: active#(take(s(M),cons(N,IL))) -> isNat#(N)
p35: active#(take(s(M),cons(N,IL))) -> isNatIList#(IL)
p36: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p37: active#(uTake2(tt(),M,N,IL)) -> cons#(N,take(M,IL))
p38: active#(uTake2(tt(),M,N,IL)) -> take#(M,IL)
p39: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p40: active#(length(cons(N,L))) -> uLength#(and(isNat(N),isNatList(L)),L)
p41: active#(length(cons(N,L))) -> and#(isNat(N),isNatList(L))
p42: active#(length(cons(N,L))) -> isNat#(N)
p43: active#(length(cons(N,L))) -> isNatList#(L)
p44: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p45: active#(uLength(tt(),L)) -> s#(length(L))
p46: active#(uLength(tt(),L)) -> length#(L)
p47: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p48: mark#(and(X1,X2)) -> and#(mark(X1),mark(X2))
p49: mark#(and(X1,X2)) -> mark#(X1)
p50: mark#(and(X1,X2)) -> mark#(X2)
p51: mark#(tt()) -> active#(tt())
p52: mark#(isNatIList(X)) -> active#(isNatIList(X))
p53: mark#(isNatList(X)) -> active#(isNatList(X))
p54: mark#(isNat(X)) -> active#(isNat(X))
p55: mark#(|0|()) -> active#(|0|())
p56: mark#(s(X)) -> active#(s(mark(X)))
p57: mark#(s(X)) -> s#(mark(X))
p58: mark#(s(X)) -> mark#(X)
p59: mark#(length(X)) -> active#(length(mark(X)))
p60: mark#(length(X)) -> length#(mark(X))
p61: mark#(length(X)) -> mark#(X)
p62: mark#(zeros()) -> active#(zeros())
p63: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p64: mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
p65: mark#(cons(X1,X2)) -> mark#(X1)
p66: mark#(nil()) -> active#(nil())
p67: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p68: mark#(take(X1,X2)) -> take#(mark(X1),mark(X2))
p69: mark#(take(X1,X2)) -> mark#(X1)
p70: mark#(take(X1,X2)) -> mark#(X2)
p71: mark#(uTake1(X)) -> active#(uTake1(mark(X)))
p72: mark#(uTake1(X)) -> uTake1#(mark(X))
p73: mark#(uTake1(X)) -> mark#(X)
p74: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p75: mark#(uTake2(X1,X2,X3,X4)) -> uTake2#(mark(X1),X2,X3,X4)
p76: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p77: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p78: mark#(uLength(X1,X2)) -> uLength#(mark(X1),X2)
p79: mark#(uLength(X1,X2)) -> mark#(X1)
p80: and#(mark(X1),X2) -> and#(X1,X2)
p81: and#(X1,mark(X2)) -> and#(X1,X2)
p82: and#(active(X1),X2) -> and#(X1,X2)
p83: and#(X1,active(X2)) -> and#(X1,X2)
p84: isNatIList#(mark(X)) -> isNatIList#(X)
p85: isNatIList#(active(X)) -> isNatIList#(X)
p86: isNatList#(mark(X)) -> isNatList#(X)
p87: isNatList#(active(X)) -> isNatList#(X)
p88: isNat#(mark(X)) -> isNat#(X)
p89: isNat#(active(X)) -> isNat#(X)
p90: s#(mark(X)) -> s#(X)
p91: s#(active(X)) -> s#(X)
p92: length#(mark(X)) -> length#(X)
p93: length#(active(X)) -> length#(X)
p94: cons#(mark(X1),X2) -> cons#(X1,X2)
p95: cons#(X1,mark(X2)) -> cons#(X1,X2)
p96: cons#(active(X1),X2) -> cons#(X1,X2)
p97: cons#(X1,active(X2)) -> cons#(X1,X2)
p98: take#(mark(X1),X2) -> take#(X1,X2)
p99: take#(X1,mark(X2)) -> take#(X1,X2)
p100: take#(active(X1),X2) -> take#(X1,X2)
p101: take#(X1,active(X2)) -> take#(X1,X2)
p102: uTake1#(mark(X)) -> uTake1#(X)
p103: uTake1#(active(X)) -> uTake1#(X)
p104: uTake2#(mark(X1),X2,X3,X4) -> uTake2#(X1,X2,X3,X4)
p105: uTake2#(X1,mark(X2),X3,X4) -> uTake2#(X1,X2,X3,X4)
p106: uTake2#(X1,X2,mark(X3),X4) -> uTake2#(X1,X2,X3,X4)
p107: uTake2#(X1,X2,X3,mark(X4)) -> uTake2#(X1,X2,X3,X4)
p108: uTake2#(active(X1),X2,X3,X4) -> uTake2#(X1,X2,X3,X4)
p109: uTake2#(X1,active(X2),X3,X4) -> uTake2#(X1,X2,X3,X4)
p110: uTake2#(X1,X2,active(X3),X4) -> uTake2#(X1,X2,X3,X4)
p111: uTake2#(X1,X2,X3,active(X4)) -> uTake2#(X1,X2,X3,X4)
p112: uLength#(mark(X1),X2) -> uLength#(X1,X2)
p113: uLength#(X1,mark(X2)) -> uLength#(X1,X2)
p114: uLength#(active(X1),X2) -> uLength#(X1,X2)
p115: uLength#(X1,active(X2)) -> uLength#(X1,X2)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p5, p7, p10, p15, p19, p23, p25, p29, p36, p39, p44, p47, p49, p50, p52, p53, p54, p56, p58, p59, p61, p62, p63, p65, p67, p69, p70, p71, p73, p74, p76, p77, p79}
  {p86, p87}
  {p88, p89}
  {p80, p81, p82, p83}
  {p84, p85}
  {p102, p103}
  {p104, p105, p106, p107, p108, p109, p110, p111}
  {p94, p95, p96, p97}
  {p98, p99, p100, p101}
  {p112, p113, p114, p115}
  {p90, p91}
  {p92, p93}


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> mark#(X1)
p3: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p4: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p5: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p6: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p7: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p8: mark#(uTake1(X)) -> mark#(X)
p9: mark#(uTake1(X)) -> active#(uTake1(mark(X)))
p10: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p11: mark#(take(X1,X2)) -> mark#(X2)
p12: mark#(take(X1,X2)) -> mark#(X1)
p13: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p14: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p15: mark#(cons(X1,X2)) -> mark#(X1)
p16: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p17: active#(take(|0|(),IL)) -> mark#(uTake1(isNatIList(IL)))
p18: mark#(zeros()) -> active#(zeros())
p19: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p20: mark#(length(X)) -> mark#(X)
p21: mark#(length(X)) -> active#(length(mark(X)))
p22: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p23: mark#(s(X)) -> mark#(X)
p24: mark#(s(X)) -> active#(s(mark(X)))
p25: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p26: mark#(isNat(X)) -> active#(isNat(X))
p27: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p28: mark#(isNatList(X)) -> active#(isNatList(X))
p29: active#(isNat(length(L))) -> mark#(isNatList(L))
p30: mark#(isNatIList(X)) -> active#(isNatIList(X))
p31: active#(isNat(s(N))) -> mark#(isNat(N))
p32: mark#(and(X1,X2)) -> mark#(X2)
p33: mark#(and(X1,X2)) -> mark#(X1)
p34: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p35: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = x1
        and_A(x1,x2) = (2,1)
        tt_A() = (1,1)
        mark#_A(x1) = (2,0)
        uLength_A(x1,x2) = (2,1)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        length_A(x1) = (2,1)
        uTake2_A(x1,x2,x3,x4) = (2,1)
        cons_A(x1,x2) = (1,1)
        isNat_A(x1) = (2,1)
        isNatList_A(x1) = (2,1)
        uTake1_A(x1) = (1,1)
        take_A(x1,x2) = (2,1)
        isNatIList_A(x1) = (2,1)
        |0|_A() = (1,0)
        zeros_A() = (2,1)
        active_A(x1) = (1,1)
        nil_A() = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,0)) x1
        and_A(x1,x2) = (1,2)
        tt_A() = (1,1)
        mark#_A(x1) = (2,0)
        uLength_A(x1,x2) = (1,2)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        length_A(x1) = (1,2)
        uTake2_A(x1,x2,x3,x4) = (1,2)
        cons_A(x1,x2) = (0,1)
        isNat_A(x1) = (1,2)
        isNatList_A(x1) = (1,2)
        uTake1_A(x1) = (0,1)
        take_A(x1,x2) = (1,2)
        isNatIList_A(x1) = (1,2)
        |0|_A() = (0,0)
        zeros_A() = (1,2)
        active_A(x1) = (1,1)
        nil_A() = (1,1)
    

The next rules are strictly ordered:

  p9, p16, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> mark#(X1)
p3: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p4: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p5: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p6: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p7: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p8: mark#(uTake1(X)) -> mark#(X)
p9: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p10: mark#(take(X1,X2)) -> mark#(X2)
p11: mark#(take(X1,X2)) -> mark#(X1)
p12: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p13: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p14: mark#(cons(X1,X2)) -> mark#(X1)
p15: active#(take(|0|(),IL)) -> mark#(uTake1(isNatIList(IL)))
p16: mark#(zeros()) -> active#(zeros())
p17: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p18: mark#(length(X)) -> mark#(X)
p19: mark#(length(X)) -> active#(length(mark(X)))
p20: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p21: mark#(s(X)) -> mark#(X)
p22: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p23: mark#(isNat(X)) -> active#(isNat(X))
p24: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p25: mark#(isNatList(X)) -> active#(isNatList(X))
p26: active#(isNat(length(L))) -> mark#(isNatList(L))
p27: mark#(isNatIList(X)) -> active#(isNatIList(X))
p28: active#(isNat(s(N))) -> mark#(isNat(N))
p29: mark#(and(X1,X2)) -> mark#(X2)
p30: mark#(and(X1,X2)) -> mark#(X1)
p31: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p32: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32}


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNat(s(N))) -> mark#(isNat(N))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: active#(isNat(length(L))) -> mark#(isNatList(L))
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(length(X)) -> mark#(X)
p16: mark#(zeros()) -> active#(zeros())
p17: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p18: mark#(cons(X1,X2)) -> mark#(X1)
p19: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p20: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p21: mark#(take(X1,X2)) -> mark#(X1)
p22: mark#(take(X1,X2)) -> mark#(X2)
p23: mark#(uTake1(X)) -> mark#(X)
p24: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p25: active#(take(|0|(),IL)) -> mark#(uTake1(isNatIList(IL)))
p26: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p27: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p28: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p29: mark#(uLength(X1,X2)) -> mark#(X1)
p30: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p31: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p32: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,0)) x1
        and_A(x1,x2) = x1 + ((0,1),(0,1)) x2
        tt_A() = (1,0)
        mark#_A(x1) = ((0,1),(0,0)) x1
        mark_A(x1) = x1 + (1,0)
        isNatIList_A(x1) = (0,0)
        isNatList_A(x1) = (1,0)
        isNat_A(x1) = (0,0)
        s_A(x1) = x1
        length_A(x1) = ((0,1),(0,1)) x1
        cons_A(x1,x2) = x1 + x2
        zeros_A() = (1,1)
        |0|_A() = (1,0)
        take_A(x1,x2) = x1 + x2 + (0,2)
        uTake1_A(x1) = x1 + (1,1)
        uTake2_A(x1,x2,x3,x4) = x1 + x2 + ((0,1),(0,1)) x3 + ((0,1),(0,1)) x4 + (0,2)
        uLength_A(x1,x2) = x1 + ((0,1),(0,1)) x2
        active_A(x1) = x1 + (1,0)
        nil_A() = (1,0)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        and_A(x1,x2) = (1,0)
        tt_A() = (0,0)
        mark#_A(x1) = (0,0)
        mark_A(x1) = (1,1)
        isNatIList_A(x1) = (1,0)
        isNatList_A(x1) = (1,0)
        isNat_A(x1) = (1,0)
        s_A(x1) = (0,0)
        length_A(x1) = (1,0)
        cons_A(x1,x2) = (0,1)
        zeros_A() = (1,1)
        |0|_A() = (1,0)
        take_A(x1,x2) = (1,0)
        uTake1_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (1,0)
        uLength_A(x1,x2) = (1,0)
        active_A(x1) = (1,1)
        nil_A() = (0,1)
    

The next rules are strictly ordered:

  p21, p22, p23, p25, p26

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNat(s(N))) -> mark#(isNat(N))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: active#(isNat(length(L))) -> mark#(isNatList(L))
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(length(X)) -> mark#(X)
p16: mark#(zeros()) -> active#(zeros())
p17: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p18: mark#(cons(X1,X2)) -> mark#(X1)
p19: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p20: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p21: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p22: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p23: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p24: mark#(uLength(X1,X2)) -> mark#(X1)
p25: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p26: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p27: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> mark#(X1)
p3: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p4: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p5: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p6: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p7: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p8: active#(uTake2(tt(),M,N,IL)) -> mark#(cons(N,take(M,IL)))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(zeros()) -> active#(zeros())
p11: active#(zeros()) -> mark#(cons(|0|(),zeros()))
p12: mark#(length(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(take(s(M),cons(N,IL))) -> mark#(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
p15: mark#(s(X)) -> mark#(X)
p16: mark#(isNat(X)) -> active#(isNat(X))
p17: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p18: mark#(isNatList(X)) -> active#(isNatList(X))
p19: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p20: mark#(isNatIList(X)) -> active#(isNatIList(X))
p21: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p22: mark#(and(X1,X2)) -> mark#(X2)
p23: mark#(and(X1,X2)) -> mark#(X1)
p24: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p25: active#(isNat(length(L))) -> mark#(isNatList(L))
p26: active#(isNat(s(N))) -> mark#(isNat(N))
p27: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,0)) x1
        and_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
        tt_A() = (0,0)
        mark#_A(x1) = ((0,1),(0,0)) x1
        uLength_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (0,1)
        mark_A(x1) = ((0,0),(1,1)) x1
        s_A(x1) = ((0,0),(1,1)) x1
        length_A(x1) = ((0,0),(1,1)) x1 + (0,1)
        uTake2_A(x1,x2,x3,x4) = ((1,1),(1,1)) x2 + ((0,0),(1,1)) x3 + ((0,0),(1,1)) x4 + (2,1)
        cons_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,0)) x2
        isNat_A(x1) = (0,0)
        isNatList_A(x1) = (0,0)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 + (1,2)
        zeros_A() = (1,1)
        |0|_A() = (0,0)
        isNatIList_A(x1) = (0,0)
        active_A(x1) = ((0,0),(1,1)) x1
        nil_A() = (0,0)
        uTake1_A(x1) = (0,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        and_A(x1,x2) = (0,0)
        tt_A() = (0,1)
        mark#_A(x1) = (0,0)
        uLength_A(x1,x2) = (0,0)
        mark_A(x1) = (1,1)
        s_A(x1) = (1,1)
        length_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (1,1)
        cons_A(x1,x2) = (0,0)
        isNat_A(x1) = (0,0)
        isNatList_A(x1) = (0,0)
        take_A(x1,x2) = (0,1)
        zeros_A() = (1,1)
        |0|_A() = (1,0)
        isNatIList_A(x1) = (1,0)
        active_A(x1) = (1,1)
        nil_A() = (1,1)
        uTake1_A(x1) = (1,1)
    

The next rules are strictly ordered:

  p2, p8, p11, p12, p14

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p3: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p4: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p5: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p6: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p7: mark#(cons(X1,X2)) -> mark#(X1)
p8: mark#(zeros()) -> active#(zeros())
p9: mark#(length(X)) -> active#(length(mark(X)))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(isNat(X)) -> active#(isNat(X))
p12: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p13: mark#(isNatList(X)) -> active#(isNatList(X))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(isNatIList(X)) -> active#(isNatIList(X))
p16: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p17: mark#(and(X1,X2)) -> mark#(X2)
p18: mark#(and(X1,X2)) -> mark#(X1)
p19: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p20: active#(isNat(length(L))) -> mark#(isNatList(L))
p21: active#(isNat(s(N))) -> mark#(isNat(N))
p22: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNat(s(N))) -> mark#(isNat(N))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: active#(isNat(length(L))) -> mark#(isNatList(L))
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(cons(X1,X2)) -> mark#(X1)
p16: mark#(take(X1,X2)) -> active#(take(mark(X1),mark(X2)))
p17: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p18: mark#(uTake2(X1,X2,X3,X4)) -> active#(uTake2(mark(X1),X2,X3,X4))
p19: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p20: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p21: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = x1
        and_A(x1,x2) = (2,1)
        tt_A() = (1,1)
        mark#_A(x1) = (2,0)
        mark_A(x1) = (1,1)
        isNatIList_A(x1) = (2,1)
        isNatList_A(x1) = (2,1)
        isNat_A(x1) = (2,1)
        s_A(x1) = (1,1)
        length_A(x1) = (2,1)
        cons_A(x1,x2) = (1,1)
        take_A(x1,x2) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (2,1)
        uLength_A(x1,x2) = (2,1)
        active_A(x1) = (1,1)
        |0|_A() = (1,1)
        zeros_A() = (0,0)
        nil_A() = (1,1)
        uTake1_A(x1) = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = x1
        and_A(x1,x2) = (2,1)
        tt_A() = (1,1)
        mark#_A(x1) = (2,1)
        mark_A(x1) = (1,1)
        isNatIList_A(x1) = (2,1)
        isNatList_A(x1) = (2,1)
        isNat_A(x1) = (2,1)
        s_A(x1) = (1,1)
        length_A(x1) = (2,1)
        cons_A(x1,x2) = (1,1)
        take_A(x1,x2) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (1,1)
        uLength_A(x1,x2) = (2,1)
        active_A(x1) = (1,1)
        |0|_A() = (1,0)
        zeros_A() = (1,1)
        nil_A() = (1,1)
        uTake1_A(x1) = (1,1)
    

The next rules are strictly ordered:

  p16, p18

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNat(s(N))) -> mark#(isNat(N))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: active#(isNat(length(L))) -> mark#(isNatList(L))
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(cons(X1,X2)) -> mark#(X1)
p16: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p17: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p18: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p19: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

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}


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p3: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(length(X)) -> active#(length(mark(X)))
p6: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p7: mark#(s(X)) -> mark#(X)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p10: mark#(isNatList(X)) -> active#(isNatList(X))
p11: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p12: mark#(isNatIList(X)) -> active#(isNatIList(X))
p13: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p14: mark#(and(X1,X2)) -> mark#(X2)
p15: mark#(and(X1,X2)) -> mark#(X1)
p16: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p17: active#(isNat(length(L))) -> mark#(isNatList(L))
p18: active#(isNat(s(N))) -> mark#(isNat(N))
p19: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,1)) x1
        and_A(x1,x2) = x1 + ((0,1),(0,1)) x2
        tt_A() = (1,0)
        mark#_A(x1) = ((0,1),(0,1)) x1
        uLength_A(x1,x2) = (0,1)
        mark_A(x1) = ((0,1),(0,1)) x1 + (1,0)
        s_A(x1) = ((0,1),(0,1)) x1 + (1,0)
        length_A(x1) = ((0,1),(0,0)) x1 + (1,1)
        cons_A(x1,x2) = x1 + (0,1)
        isNat_A(x1) = (1,0)
        isNatList_A(x1) = (1,0)
        take_A(x1,x2) = ((0,1),(0,1)) x1 + x2 + (1,2)
        isNatIList_A(x1) = ((0,1),(0,0)) x1 + (1,0)
        active_A(x1) = ((0,1),(0,1)) x1 + (1,0)
        |0|_A() = (1,1)
        zeros_A() = (0,3)
        nil_A() = (1,1)
        uTake1_A(x1) = ((0,1),(0,0)) x1 + (1,2)
        uTake2_A(x1,x2,x3,x4) = x2 + x3 + (1,2)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        and_A(x1,x2) = (0,1)
        tt_A() = (0,1)
        mark#_A(x1) = (0,0)
        uLength_A(x1,x2) = (0,0)
        mark_A(x1) = (0,1)
        s_A(x1) = (1,1)
        length_A(x1) = (0,0)
        cons_A(x1,x2) = (0,0)
        isNat_A(x1) = (0,1)
        isNatList_A(x1) = (0,0)
        take_A(x1,x2) = (1,0)
        isNatIList_A(x1) = (0,1)
        active_A(x1) = (0,1)
        |0|_A() = (0,1)
        zeros_A() = (1,0)
        nil_A() = (0,1)
        uTake1_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (0,0)
    

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: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p3: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p4: mark#(length(X)) -> active#(length(mark(X)))
p5: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(isNat(X)) -> active#(isNat(X))
p8: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p9: mark#(isNatList(X)) -> active#(isNatList(X))
p10: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p11: mark#(isNatIList(X)) -> active#(isNatIList(X))
p12: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p13: mark#(and(X1,X2)) -> mark#(X2)
p14: mark#(and(X1,X2)) -> mark#(X1)
p15: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p16: active#(isNat(length(L))) -> mark#(isNatList(L))
p17: active#(isNat(s(N))) -> mark#(isNat(N))
p18: active#(isNatIList(IL)) -> mark#(isNatList(IL))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

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}


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(IL)) -> mark#(isNatList(IL))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNat(s(N))) -> mark#(isNat(N))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: active#(isNat(length(L))) -> mark#(isNatList(L))
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(length(X)) -> active#(length(mark(X)))
p14: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p15: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p16: active#(isNatList(take(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p17: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p18: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((1,1),(0,0)) x1
        and_A(x1,x2) = ((1,1),(0,0)) x1 + ((0,0),(1,1)) x2
        tt_A() = (0,0)
        mark#_A(x1) = ((1,1),(0,0)) x1
        mark_A(x1) = ((0,0),(1,1)) x1
        isNatIList_A(x1) = ((0,0),(1,1)) x1 + (1,2)
        isNatList_A(x1) = ((0,0),(1,1)) x1 + (1,1)
        isNat_A(x1) = ((1,1),(1,1)) x1
        s_A(x1) = ((1,1),(0,0)) x1
        length_A(x1) = ((1,1),(1,1)) x1 + (1,1)
        cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2
        uLength_A(x1,x2) = ((1,1),(1,1)) x2 + (1,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 + (4,1)
        active_A(x1) = ((0,0),(1,1)) x1
        |0|_A() = (0,0)
        zeros_A() = (1,1)
        nil_A() = (1,1)
        uTake1_A(x1) = ((1,1),(0,0)) x1 + (1,1)
        uTake2_A(x1,x2,x3,x4) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + ((1,1),(0,0)) x4 + (4,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        and_A(x1,x2) = (1,1)
        tt_A() = (0,1)
        mark#_A(x1) = (0,0)
        mark_A(x1) = (1,0)
        isNatIList_A(x1) = (1,1)
        isNatList_A(x1) = (1,1)
        isNat_A(x1) = (1,1)
        s_A(x1) = (0,1)
        length_A(x1) = (1,0)
        cons_A(x1,x2) = (1,1)
        uLength_A(x1,x2) = (1,1)
        take_A(x1,x2) = (1,0)
        active_A(x1) = (1,0)
        |0|_A() = (1,1)
        zeros_A() = (1,0)
        nil_A() = (0,0)
        uTake1_A(x1) = (1,0)
        uTake2_A(x1,x2,x3,x4) = (0,0)
    

The next rules are strictly ordered:

  p3, p9, p16

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> active#(isNatIList(X))
p6: active#(isNat(s(N))) -> mark#(isNat(N))
p7: mark#(isNatList(X)) -> active#(isNatList(X))
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(length(X)) -> active#(length(mark(X)))
p12: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p13: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p14: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p15: active#(uLength(tt(),L)) -> mark#(s(length(L)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p3: active#(uLength(tt(),L)) -> mark#(s(length(L)))
p4: mark#(length(X)) -> active#(length(mark(X)))
p5: active#(length(cons(N,L))) -> mark#(uLength(and(isNat(N),isNatList(L)),L))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(isNat(X)) -> active#(isNat(X))
p8: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p9: mark#(isNatList(X)) -> active#(isNatList(X))
p10: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p11: mark#(isNatIList(X)) -> active#(isNatIList(X))
p12: active#(isNat(s(N))) -> mark#(isNat(N))
p13: mark#(and(X1,X2)) -> mark#(X2)
p14: mark#(and(X1,X2)) -> mark#(X1)
p15: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((1,0),(1,0)) x1
        and_A(x1,x2) = x1 + x2
        tt_A() = (0,5)
        mark#_A(x1) = ((1,0),(1,0)) x1
        uLength_A(x1,x2) = ((0,1),(0,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
        mark_A(x1) = x1
        s_A(x1) = x1 + (2,4)
        length_A(x1) = ((1,0),(1,1)) x1 + (3,2)
        cons_A(x1,x2) = ((1,1),(1,0)) x1 + ((1,1),(0,1)) x2
        isNat_A(x1) = ((1,1),(1,1)) x1 + (0,5)
        isNatList_A(x1) = ((1,1),(0,1)) x1 + (1,1)
        isNatIList_A(x1) = ((1,1),(0,1)) x1 + (2,5)
        active_A(x1) = x1
        |0|_A() = (0,0)
        zeros_A() = (1,0)
        nil_A() = (1,4)
        take_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (3,4)
        uTake1_A(x1) = (2,4)
        uTake2_A(x1,x2,x3,x4) = ((1,1),(0,0)) x2 + ((1,1),(1,0)) x3 + ((1,1),(0,1)) x4 + (8,4)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,1)) x1
        and_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2
        tt_A() = (0,0)
        mark#_A(x1) = ((0,1),(0,1)) x1
        uLength_A(x1,x2) = (0,1)
        mark_A(x1) = ((1,1),(0,0)) x1
        s_A(x1) = (0,2)
        length_A(x1) = (0,0)
        cons_A(x1,x2) = ((0,0),(1,1)) x2
        isNat_A(x1) = (0,0)
        isNatList_A(x1) = ((0,0),(1,1)) x1
        isNatIList_A(x1) = (0,2)
        active_A(x1) = ((0,1),(1,0)) x1
        |0|_A() = (0,1)
        zeros_A() = (0,1)
        nil_A() = (0,4)
        take_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (0,1)
        uTake1_A(x1) = (0,3)
        uTake2_A(x1,x2,x3,x4) = ((0,0),(1,1)) x3 + ((0,0),(1,1)) x4 + (0,2)
    

The next rules are strictly ordered:

  p3, p5, p6, p12

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))
p3: mark#(length(X)) -> active#(length(mark(X)))
p4: mark#(isNat(X)) -> active#(isNat(X))
p5: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p6: mark#(isNatList(X)) -> active#(isNatList(X))
p7: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p8: mark#(isNatIList(X)) -> active#(isNatIList(X))
p9: mark#(and(X1,X2)) -> mark#(X2)
p10: mark#(and(X1,X2)) -> mark#(X1)
p11: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

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: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p8: mark#(isNatList(X)) -> active#(isNatList(X))
p9: mark#(isNat(X)) -> active#(isNat(X))
p10: mark#(length(X)) -> active#(length(mark(X)))
p11: mark#(uLength(X1,X2)) -> active#(uLength(mark(X1),X2))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((0,1),(0,0)) x1
        and_A(x1,x2) = (1,2)
        tt_A() = (1,1)
        mark#_A(x1) = (2,0)
        mark_A(x1) = (1,1)
        isNatIList_A(x1) = (1,2)
        cons_A(x1,x2) = (1,1)
        isNat_A(x1) = (1,1)
        isNatList_A(x1) = (1,2)
        length_A(x1) = (1,1)
        uLength_A(x1,x2) = (1,1)
        active_A(x1) = (1,1)
        |0|_A() = (1,1)
        s_A(x1) = (1,1)
        zeros_A() = (1,1)
        nil_A() = (1,1)
        take_A(x1,x2) = (1,1)
        uTake1_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = (0,0)
        and_A(x1,x2) = (1,1)
        tt_A() = (1,1)
        mark#_A(x1) = (0,0)
        mark_A(x1) = (1,1)
        isNatIList_A(x1) = (1,1)
        cons_A(x1,x2) = (1,1)
        isNat_A(x1) = (1,1)
        isNatList_A(x1) = (1,1)
        length_A(x1) = (1,1)
        uLength_A(x1,x2) = (1,1)
        active_A(x1) = (1,1)
        |0|_A() = (1,1)
        s_A(x1) = (1,1)
        zeros_A() = (1,1)
        nil_A() = (1,1)
        take_A(x1,x2) = (1,1)
        uTake1_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = (1,1)
    

The next rules are strictly ordered:

  p9, p10, p11

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(and(tt(),T)) -> mark#(T)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))
p3: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> mark#(X2)
p6: mark#(isNatIList(X)) -> active#(isNatIList(X))
p7: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p8: mark#(isNatList(X)) -> active#(isNatList(X))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

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: active#(and(tt(),T)) -> mark#(T)
p2: mark#(isNatList(X)) -> active#(isNatList(X))
p3: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p4: mark#(isNatIList(X)) -> active#(isNatIList(X))
p5: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))
p6: mark#(and(X1,X2)) -> mark#(X2)
p7: mark#(and(X1,X2)) -> mark#(X1)
p8: mark#(and(X1,X2)) -> active#(and(mark(X1),mark(X2)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = x1
        and_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (0,1)
        tt_A() = (0,1)
        mark#_A(x1) = x1
        isNatList_A(x1) = x1 + (1,1)
        cons_A(x1,x2) = x1 + x2 + (0,1)
        isNat_A(x1) = x1 + (0,1)
        isNatIList_A(x1) = x1 + (2,1)
        mark_A(x1) = x1 + (0,1)
        active_A(x1) = x1 + (0,1)
        |0|_A() = (0,1)
        s_A(x1) = x1 + (0,1)
        length_A(x1) = x1 + (2,1)
        zeros_A() = (1,1)
        nil_A() = (0,1)
        take_A(x1,x2) = x1 + x2 + (2,1)
        uTake1_A(x1) = (1,1)
        uTake2_A(x1,x2,x3,x4) = ((0,0),(1,0)) x1 + x2 + x3 + x4 + (2,1)
        uLength_A(x1,x2) = x2 + (2,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        active#_A(x1) = ((1,1),(1,1)) x1
        and_A(x1,x2) = ((0,0),(1,1)) x1 + ((0,0),(1,1)) x2 + (4,1)
        tt_A() = (7,1)
        mark#_A(x1) = ((1,1),(1,1)) x1 + (1,0)
        isNatList_A(x1) = ((0,1),(0,1)) x1 + (1,4)
        cons_A(x1,x2) = ((0,0),(1,1)) x1 + x2 + (1,4)
        isNat_A(x1) = ((0,0),(1,1)) x1 + (1,1)
        isNatIList_A(x1) = ((0,1),(0,1)) x1 + (0,1)
        mark_A(x1) = ((0,0),(1,1)) x1
        active_A(x1) = ((0,0),(1,1)) x1
        |0|_A() = (1,5)
        s_A(x1) = ((1,1),(0,0)) x1
        length_A(x1) = (1,1)
        zeros_A() = (11,1)
        nil_A() = (15,1)
        take_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(0,0)) x2 + (1,1)
        uTake1_A(x1) = (1,14)
        uTake2_A(x1,x2,x3,x4) = ((1,1),(0,0)) x2 + ((0,0),(1,1)) x3 + ((0,1),(0,0)) x4 + (1,5)
        uLength_A(x1,x2) = (1,1)
    

The next rules are strictly ordered:

  p1, p2, p4, p6, p7, p8

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(isNatList(cons(N,L))) -> mark#(and(isNat(N),isNatList(L)))
p2: active#(isNatIList(cons(N,IL))) -> mark#(and(isNat(N),isNatIList(IL)))

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: isNatList#(mark(X)) -> isNatList#(X)
p2: isNatList#(active(X)) -> isNatList#(X)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

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: isNat#(mark(X)) -> isNat#(X)
p2: isNat#(active(X)) -> isNat#(X)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

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

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

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: isNatIList#(mark(X)) -> isNatIList#(X)
p2: isNatIList#(active(X)) -> isNatIList#(X)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: uTake1#(mark(X)) -> uTake1#(X)
p2: uTake1#(active(X)) -> uTake1#(X)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: uTake2#(mark(X1),X2,X3,X4) -> uTake2#(X1,X2,X3,X4)
p2: uTake2#(X1,X2,X3,active(X4)) -> uTake2#(X1,X2,X3,X4)
p3: uTake2#(X1,X2,active(X3),X4) -> uTake2#(X1,X2,X3,X4)
p4: uTake2#(X1,active(X2),X3,X4) -> uTake2#(X1,X2,X3,X4)
p5: uTake2#(active(X1),X2,X3,X4) -> uTake2#(X1,X2,X3,X4)
p6: uTake2#(X1,X2,X3,mark(X4)) -> uTake2#(X1,X2,X3,X4)
p7: uTake2#(X1,X2,mark(X3),X4) -> uTake2#(X1,X2,X3,X4)
p8: uTake2#(X1,mark(X2),X3,X4) -> uTake2#(X1,X2,X3,X4)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

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

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4

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

-- Reduction pair.

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

p1: 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(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68

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

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4

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(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: length#(mark(X)) -> length#(X)
p2: length#(active(X)) -> length#(X)

and R consists of:

r1: active(and(tt(),T)) -> mark(T)
r2: active(isNatIList(IL)) -> mark(isNatList(IL))
r3: active(isNat(|0|())) -> mark(tt())
r4: active(isNat(s(N))) -> mark(isNat(N))
r5: active(isNat(length(L))) -> mark(isNatList(L))
r6: active(isNatIList(zeros())) -> mark(tt())
r7: active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r8: active(isNatList(nil())) -> mark(tt())
r9: active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L)))
r10: active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL)))
r11: active(zeros()) -> mark(cons(|0|(),zeros()))
r12: active(take(|0|(),IL)) -> mark(uTake1(isNatIList(IL)))
r13: active(uTake1(tt())) -> mark(nil())
r14: active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL))
r15: active(uTake2(tt(),M,N,IL)) -> mark(cons(N,take(M,IL)))
r16: active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L))
r17: active(uLength(tt(),L)) -> mark(s(length(L)))
r18: mark(and(X1,X2)) -> active(and(mark(X1),mark(X2)))
r19: mark(tt()) -> active(tt())
r20: mark(isNatIList(X)) -> active(isNatIList(X))
r21: mark(isNatList(X)) -> active(isNatList(X))
r22: mark(isNat(X)) -> active(isNat(X))
r23: mark(|0|()) -> active(|0|())
r24: mark(s(X)) -> active(s(mark(X)))
r25: mark(length(X)) -> active(length(mark(X)))
r26: mark(zeros()) -> active(zeros())
r27: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r28: mark(nil()) -> active(nil())
r29: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2)))
r30: mark(uTake1(X)) -> active(uTake1(mark(X)))
r31: mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4))
r32: mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2))
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNatIList(mark(X)) -> isNatIList(X)
r38: isNatIList(active(X)) -> isNatIList(X)
r39: isNatList(mark(X)) -> isNatList(X)
r40: isNatList(active(X)) -> isNatList(X)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: s(mark(X)) -> s(X)
r44: s(active(X)) -> s(X)
r45: length(mark(X)) -> length(X)
r46: length(active(X)) -> length(X)
r47: cons(mark(X1),X2) -> cons(X1,X2)
r48: cons(X1,mark(X2)) -> cons(X1,X2)
r49: cons(active(X1),X2) -> cons(X1,X2)
r50: cons(X1,active(X2)) -> cons(X1,X2)
r51: take(mark(X1),X2) -> take(X1,X2)
r52: take(X1,mark(X2)) -> take(X1,X2)
r53: take(active(X1),X2) -> take(X1,X2)
r54: take(X1,active(X2)) -> take(X1,X2)
r55: uTake1(mark(X)) -> uTake1(X)
r56: uTake1(active(X)) -> uTake1(X)
r57: uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r58: uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r59: uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4)
r60: uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4)
r61: uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r62: uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4)
r63: uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4)
r64: uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4)
r65: uLength(mark(X1),X2) -> uLength(X1,X2)
r66: uLength(X1,mark(X2)) -> uLength(X1,X2)
r67: uLength(active(X1),X2) -> uLength(X1,X2)
r68: uLength(X1,active(X2)) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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