YES

We show the termination of the TRS R:

  a__and(tt(),T) -> mark(T)
  a__isNatIList(IL) -> a__isNatList(IL)
  a__isNat(|0|()) -> tt()
  a__isNat(s(N)) -> a__isNat(N)
  a__isNat(length(L)) -> a__isNatList(L)
  a__isNatIList(zeros()) -> tt()
  a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
  a__isNatList(nil()) -> tt()
  a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
  a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
  a__zeros() -> cons(|0|(),zeros())
  a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
  a__uTake1(tt()) -> nil()
  a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
  a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
  a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
  a__uLength(tt(),L) -> s(a__length(mark(L)))
  mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
  mark(isNatIList(X)) -> a__isNatIList(X)
  mark(isNatList(X)) -> a__isNatList(X)
  mark(isNat(X)) -> a__isNat(X)
  mark(length(X)) -> a__length(mark(X))
  mark(zeros()) -> a__zeros()
  mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
  mark(uTake1(X)) -> a__uTake1(mark(X))
  mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
  mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
  mark(tt()) -> tt()
  mark(|0|()) -> |0|()
  mark(s(X)) -> s(mark(X))
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(nil()) -> nil()
  a__and(X1,X2) -> and(X1,X2)
  a__isNatIList(X) -> isNatIList(X)
  a__isNatList(X) -> isNatList(X)
  a__isNat(X) -> isNat(X)
  a__length(X) -> length(X)
  a__zeros() -> zeros()
  a__take(X1,X2) -> take(X1,X2)
  a__uTake1(X) -> uTake1(X)
  a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
  a__uLength(X1,X2) -> uLength(X1,X2)

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: a__isNatIList#(IL) -> a__isNatList#(IL)
p3: a__isNat#(s(N)) -> a__isNat#(N)
p4: a__isNat#(length(L)) -> a__isNatList#(L)
p5: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p6: a__isNatIList#(cons(N,IL)) -> a__isNat#(N)
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p9: a__isNatList#(cons(N,L)) -> a__isNat#(N)
p10: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p11: a__isNatList#(take(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p12: a__isNatList#(take(N,IL)) -> a__isNat#(N)
p13: a__isNatList#(take(N,IL)) -> a__isNatIList#(IL)
p14: a__take#(|0|(),IL) -> a__uTake1#(a__isNatIList(IL))
p15: a__take#(|0|(),IL) -> a__isNatIList#(IL)
p16: a__take#(s(M),cons(N,IL)) -> a__uTake2#(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
p17: a__take#(s(M),cons(N,IL)) -> a__and#(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL)))
p18: a__take#(s(M),cons(N,IL)) -> a__isNat#(M)
p19: a__take#(s(M),cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p20: a__take#(s(M),cons(N,IL)) -> a__isNat#(N)
p21: a__take#(s(M),cons(N,IL)) -> a__isNatIList#(IL)
p22: a__uTake2#(tt(),M,N,IL) -> mark#(N)
p23: a__length#(cons(N,L)) -> a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)
p24: a__length#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p25: a__length#(cons(N,L)) -> a__isNat#(N)
p26: a__length#(cons(N,L)) -> a__isNatList#(L)
p27: a__uLength#(tt(),L) -> a__length#(mark(L))
p28: a__uLength#(tt(),L) -> mark#(L)
p29: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p30: mark#(and(X1,X2)) -> mark#(X1)
p31: mark#(and(X1,X2)) -> mark#(X2)
p32: mark#(isNatIList(X)) -> a__isNatIList#(X)
p33: mark#(isNatList(X)) -> a__isNatList#(X)
p34: mark#(isNat(X)) -> a__isNat#(X)
p35: mark#(length(X)) -> a__length#(mark(X))
p36: mark#(length(X)) -> mark#(X)
p37: mark#(zeros()) -> a__zeros#()
p38: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p39: mark#(take(X1,X2)) -> mark#(X1)
p40: mark#(take(X1,X2)) -> mark#(X2)
p41: mark#(uTake1(X)) -> a__uTake1#(mark(X))
p42: mark#(uTake1(X)) -> mark#(X)
p43: mark#(uTake2(X1,X2,X3,X4)) -> a__uTake2#(mark(X1),X2,X3,X4)
p44: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p45: mark#(uLength(X1,X2)) -> a__uLength#(mark(X1),X2)
p46: mark#(uLength(X1,X2)) -> mark#(X1)
p47: mark#(s(X)) -> mark#(X)
p48: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p38, p39, p40, p42, p43, p44, p45, p46, p47, p48}


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(cons(X1,X2)) -> mark#(X1)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(uLength(X1,X2)) -> mark#(X1)
p5: mark#(uLength(X1,X2)) -> a__uLength#(mark(X1),X2)
p6: a__uLength#(tt(),L) -> mark#(L)
p7: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p8: mark#(uTake2(X1,X2,X3,X4)) -> a__uTake2#(mark(X1),X2,X3,X4)
p9: a__uTake2#(tt(),M,N,IL) -> mark#(N)
p10: mark#(uTake1(X)) -> mark#(X)
p11: mark#(take(X1,X2)) -> mark#(X2)
p12: mark#(take(X1,X2)) -> mark#(X1)
p13: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p14: a__take#(s(M),cons(N,IL)) -> a__isNatIList#(IL)
p15: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p16: a__isNatIList#(cons(N,IL)) -> a__isNat#(N)
p17: a__isNat#(length(L)) -> a__isNatList#(L)
p18: a__isNatList#(take(N,IL)) -> a__isNatIList#(IL)
p19: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p20: a__isNatIList#(IL) -> a__isNatList#(IL)
p21: a__isNatList#(take(N,IL)) -> a__isNat#(N)
p22: a__isNat#(s(N)) -> a__isNat#(N)
p23: a__isNatList#(take(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p24: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p25: a__isNatList#(cons(N,L)) -> a__isNat#(N)
p26: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p27: a__take#(s(M),cons(N,IL)) -> a__isNat#(N)
p28: a__take#(s(M),cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p29: a__take#(s(M),cons(N,IL)) -> a__isNat#(M)
p30: a__take#(s(M),cons(N,IL)) -> a__and#(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL)))
p31: a__take#(s(M),cons(N,IL)) -> a__uTake2#(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
p32: a__take#(|0|(),IL) -> a__isNatIList#(IL)
p33: mark#(length(X)) -> mark#(X)
p34: mark#(length(X)) -> a__length#(mark(X))
p35: a__length#(cons(N,L)) -> a__isNatList#(L)
p36: a__length#(cons(N,L)) -> a__isNat#(N)
p37: a__length#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p38: a__length#(cons(N,L)) -> a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)
p39: a__uLength#(tt(),L) -> a__length#(mark(L))
p40: mark#(isNat(X)) -> a__isNat#(X)
p41: mark#(isNatList(X)) -> a__isNatList#(X)
p42: mark#(isNatIList(X)) -> a__isNatIList#(X)
p43: mark#(and(X1,X2)) -> mark#(X2)
p44: mark#(and(X1,X2)) -> mark#(X1)
p45: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{0, x2 - 54}
          tt_A = 5
          mark#_A(x1) = max{0, x1 - 54}
          cons_A(x1,x2) = max{16, x1, x2}
          s_A(x1) = max{55, x1}
          uLength_A(x1,x2) = max{117, x1 + 36, x2 + 69}
          a__uLength#_A(x1,x2) = max{61, x1 - 35, x2 + 14}
          mark_A(x1) = max{47, x1}
          uTake2_A(x1,x2,x3,x4) = max{212, x1 + 103, x2 + 157, x3 + 149, x4 + 156}
          a__uTake2#_A(x1,x2,x3,x4) = max{x1 - 4, x2 + 1, x3 + 1, x4 + 53}
          uTake1_A(x1) = max{201, x1 + 102}
          take_A(x1,x2) = max{204, x1 + 157, x2 + 156}
          a__take#_A(x1,x2) = max{101, x1 + 50, x2 + 54}
          a__isNatIList#_A(x1) = max{0, x1 - 1}
          a__isNat#_A(x1) = max{0, x1 - 94}
          length_A(x1) = max{117, x1 + 69}
          a__isNatList#_A(x1) = max{0, x1 - 42}
          a__isNat_A(x1) = max{11, x1 - 39}
          a__isNatIList_A(x1) = x1 + 53
          a__isNatList_A(x1) = max{52, x1 + 12}
          a__and_A(x1,x2) = max{50, x1 + 2, x2}
          |0|_A = 45
          a__length#_A(x1) = max{61, x1 + 14}
          isNat_A(x1) = max{11, x1 - 39}
          isNatList_A(x1) = max{52, x1 + 12}
          isNatIList_A(x1) = x1 + 53
          and_A(x1,x2) = max{50, x1 + 2, x2}
          a__zeros_A = 46
          zeros_A = 46
          a__take_A(x1,x2) = max{204, x1 + 157, x2 + 156}
          a__uTake1_A(x1) = max{201, x1 + 102}
          nil_A = 0
          a__uTake2_A(x1,x2,x3,x4) = max{212, x1 + 103, x2 + 157, x3 + 149, x4 + 156}
          a__length_A(x1) = max{117, x1 + 69}
          a__uLength_A(x1,x2) = max{117, x1 + 36, x2 + 69}
    
      precedence:
      
        |0| > a__take# > a__isNatIList = isNatIList > a__isNatList = isNatList > a__isNat = isNat > tt = uLength = mark = length = a__and = and = a__length = a__uLength > a__take > a__uTake2 > uTake2 = a__uTake1 > take > uTake1 > a__zeros > a__and# = mark# = a__uTake2# = a__isNatIList# = a__isNatList# > a__isNat# > zeros > s > cons = a__uLength# = a__length# = nil
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = [2]
        pi(s) = []
        pi(uLength) = []
        pi(a__uLength#) = []
        pi(mark) = [1]
        pi(uTake2) = [2, 3]
        pi(a__uTake2#) = [2, 3, 4]
        pi(uTake1) = []
        pi(take) = [1, 2]
        pi(a__take#) = [2]
        pi(a__isNatIList#) = []
        pi(a__isNat#) = []
        pi(length) = []
        pi(a__isNatList#) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = [1]
        pi(a__isNatList) = [1]
        pi(a__and) = [2]
        pi(|0|) = []
        pi(a__length#) = []
        pi(isNat) = []
        pi(isNatList) = [1]
        pi(isNatIList) = [1]
        pi(and) = [2]
        pi(a__zeros) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = [1]
        pi(a__uLength) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 3
          tt_A = 66
          mark#_A(x1) = 3
          cons_A(x1,x2) = x2 + 903
          s_A(x1) = 429
          uLength_A(x1,x2) = 208
          a__uLength#_A(x1,x2) = 26
          mark_A(x1) = x1 + 223
          uTake2_A(x1,x2,x3,x4) = max{214, x2 + 4, x3 + 212}
          a__uTake2#_A(x1,x2,x3,x4) = max{x2 + 5, x3 + 213, x4 + 1419}
          uTake1_A(x1) = 2
          take_A(x1,x2) = max{x1 + 117, x2 + 442}
          a__take#_A(x1,x2) = x2 + 516
          a__isNatIList#_A(x1) = 3
          a__isNat#_A(x1) = 3
          length_A(x1) = 215
          a__isNatList#_A(x1) = 3
          a__isNat_A(x1) = 639
          a__isNatIList_A(x1) = x1 + 327
          a__isNatList_A(x1) = x1 + 426
          a__and_A(x1,x2) = x2 + 542
          |0|_A = 6
          a__length#_A(x1) = 26
          isNat_A(x1) = 417
          isNatList_A(x1) = x1 + 426
          isNatIList_A(x1) = x1 + 327
          and_A(x1,x2) = x2 + 542
          a__zeros_A = 217
          zeros_A = 218
          a__take_A(x1,x2) = 217
          a__uTake1_A(x1) = 217
          nil_A = 0
          a__uTake2_A(x1,x2,x3,x4) = 215
          a__length_A(x1) = 430
          a__uLength_A(x1,x2) = 430
    
      precedence:
      
        uLength = uTake2 > |0| > nil > a__and# = mark# = a__isNatIList# = a__isNatList# > a__uLength# = a__length# > a__uTake2# = a__take# = a__isNat# = zeros = a__length > a__uLength > s > mark = a__isNatIList = a__uTake2 > a__zeros > cons > a__isNat = a__isNatList = a__and = isNat = a__take > take > a__uTake1 > isNatIList > tt = length > isNatList > uTake1 > and
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = []
        pi(s) = []
        pi(uLength) = []
        pi(a__uLength#) = []
        pi(mark) = []
        pi(uTake2) = [2]
        pi(a__uTake2#) = []
        pi(uTake1) = []
        pi(take) = []
        pi(a__take#) = [2]
        pi(a__isNatIList#) = []
        pi(a__isNat#) = []
        pi(length) = []
        pi(a__isNatList#) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(a__isNatList) = [1]
        pi(a__and) = []
        pi(|0|) = []
        pi(a__length#) = []
        pi(isNat) = []
        pi(isNatList) = [1]
        pi(isNatIList) = [1]
        pi(and) = []
        pi(a__zeros) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
    

The next rules are strictly ordered:

  p5, p6, p8, p9, p13, p14, p16, p17, p21, p27, p28, p29, p30, p31, p32, p34, p35, p36

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__uLength#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__uLength#(a__and(a__isNat(N),a__isNatList(L)),L)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__uLength#_A(x1,x2) = max{151, x1 - 268, x2 + 43}
          tt_A = 478
          a__length#_A(x1) = max{152, x1 - 1}
          mark_A(x1) = max{108, x1}
          cons_A(x1,x2) = x2 + 45
          a__and_A(x1,x2) = max{311, x2 + 35}
          a__isNat_A(x1) = max{309, x1 + 264}
          a__isNatList_A(x1) = max{273, x1 + 272}
          a__isNatIList_A(x1) = max{420, x1 + 418}
          zeros_A = 61
          a__zeros_A = 107
          |0|_A = 215
          a__take_A(x1,x2) = max{593, x1 + 332, x2 + 441}
          a__uTake1_A(x1) = max{440, x1 + 22}
          nil_A = 479
          s_A(x1) = max{308, x1 + 45}
          a__uTake2_A(x1,x2,x3,x4) = max{639, x2 + 377, x4 + 486}
          take_A(x1,x2) = max{593, x1 + 332, x2 + 441}
          a__length_A(x1) = max{274, x1 + 113}
          a__uLength_A(x1,x2) = max{274, x1 - 159, x2 + 158}
          isNatIList_A(x1) = max{420, x1 + 418}
          length_A(x1) = max{274, x1 + 113}
          uTake1_A(x1) = max{440, x1 + 22}
          uTake2_A(x1,x2,x3,x4) = max{639, x2 + 377, x4 + 486}
          uLength_A(x1,x2) = max{274, x1 - 159, x2 + 158}
          and_A(x1,x2) = max{311, x2 + 35}
          isNatList_A(x1) = max{273, x1 + 272}
          isNat_A(x1) = max{309, x1 + 264}
    
      precedence:
      
        mark = a__isNatList > a__isNatIList > isNatIList = isNatList > a__take = take > nil > a__zeros > a__uTake2 > a__length# > a__and > a__length > cons = a__isNat = a__uLength > a__uTake1 = isNat > length > a__uLength# > uTake2 > tt > zeros > |0| = uLength > uTake1 > s = and
      
      partial status:
    
        pi(a__uLength#) = [2]
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = [1]
        pi(cons) = []
        pi(a__and) = [2]
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(zeros) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(a__take) = []
        pi(a__uTake1) = [1]
        pi(nil) = []
        pi(s) = []
        pi(a__uTake2) = [4]
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = [2]
        pi(isNatIList) = [1]
        pi(length) = [1]
        pi(uTake1) = [1]
        pi(uTake2) = [4]
        pi(uLength) = []
        pi(and) = [2]
        pi(isNatList) = [1]
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__uLength#_A(x1,x2) = 60
          tt_A = 89
          a__length#_A(x1) = 202
          mark_A(x1) = max{61, x1 - 21}
          cons_A(x1,x2) = 83
          a__and_A(x1,x2) = max{61, x2 - 21}
          a__isNat_A(x1) = 201
          a__isNatList_A(x1) = 88
          a__isNatIList_A(x1) = 88
          zeros_A = 662
          a__zeros_A = 741
          |0|_A = 682
          a__take_A(x1,x2) = 89
          a__uTake1_A(x1) = 89
          nil_A = 90
          s_A(x1) = 58
          a__uTake2_A(x1,x2,x3,x4) = 83
          take_A(x1,x2) = 0
          a__length_A(x1) = 87
          a__uLength_A(x1,x2) = 60
          isNatIList_A(x1) = x1 + 110
          length_A(x1) = max{228, x1 + 226}
          uTake1_A(x1) = max{111, x1 - 22}
          uTake2_A(x1,x2,x3,x4) = 74
          uLength_A(x1,x2) = 58
          and_A(x1,x2) = max{0, x2 - 21}
          isNatList_A(x1) = x1 + 110
          isNat_A(x1) = 223
    
      precedence:
      
        a__zeros > a__take > a__uTake2 > cons > a__isNatIList > a__isNat = nil > a__isNatList > a__and > mark > a__uTake1 = s > take > length = uTake1 > zeros = a__length > tt = a__length# = |0| = a__uLength = isNatIList = and > a__uLength# > uTake2 = isNatList > uLength > isNat
      
      partial status:
    
        pi(a__uLength#) = []
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = []
        pi(cons) = []
        pi(a__and) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(zeros) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(s) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNatIList) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(and) = []
        pi(isNatList) = []
        pi(isNat) = []
    

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: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(IL) -> a__isNatList#(IL)
p7: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p8: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p9: a__isNatList#(take(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p10: a__isNatList#(take(N,IL)) -> a__isNatIList#(IL)
p11: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p12: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p13: mark#(isNatList(X)) -> a__isNatList#(X)
p14: mark#(length(X)) -> mark#(X)
p15: mark#(take(X1,X2)) -> mark#(X1)
p16: mark#(take(X1,X2)) -> mark#(X2)
p17: mark#(uTake1(X)) -> mark#(X)
p18: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p19: mark#(uLength(X1,X2)) -> mark#(X1)
p20: mark#(s(X)) -> mark#(X)
p21: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 - 3, x2}
          tt_A = 6
          mark#_A(x1) = max{2, x1}
          and_A(x1,x2) = max{x1 + 13, x2}
          mark_A(x1) = x1
          isNatIList_A(x1) = x1 + 17
          a__isNatIList#_A(x1) = x1 + 17
          a__isNatList#_A(x1) = x1 + 16
          cons_A(x1,x2) = max{24, x1 + 3, x2}
          a__isNat_A(x1) = x1 + 2
          a__isNatList_A(x1) = x1 + 16
          take_A(x1,x2) = max{22, x1 + 19, x2 + 21}
          a__isNatIList_A(x1) = x1 + 17
          isNatList_A(x1) = x1 + 16
          length_A(x1) = max{20, x1 + 19}
          uTake1_A(x1) = x1 + 2
          uTake2_A(x1,x2,x3,x4) = max{x1 + 3, x2 + 19, x3 + 24, x4 + 21}
          uLength_A(x1,x2) = max{23, x1 + 3, x2 + 19}
          s_A(x1) = x1
          a__and_A(x1,x2) = max{x1 + 13, x2}
          a__zeros_A = 25
          |0|_A = 22
          zeros_A = 25
          a__take_A(x1,x2) = max{22, x1 + 19, x2 + 21}
          a__uTake1_A(x1) = x1 + 2
          nil_A = 7
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 3, x2 + 19, x3 + 24, x4 + 21}
          a__length_A(x1) = max{20, x1 + 19}
          a__uLength_A(x1,x2) = max{23, x1 + 3, x2 + 19}
          isNat_A(x1) = x1 + 2
    
      precedence:
      
        a__and# = tt = mark# = and = mark = isNatIList = a__isNatIList# = a__isNatList# = cons = a__isNat = a__isNatList = take = a__isNatIList = isNatList = length = uTake1 = uTake2 = uLength = s = a__and = a__zeros = |0| = zeros = a__take = a__uTake1 = nil = a__uTake2 = a__length = a__uLength = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(take) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 14
          tt_A = 18
          mark#_A(x1) = 14
          and_A(x1,x2) = 26
          mark_A(x1) = 26
          isNatIList_A(x1) = 1
          a__isNatIList#_A(x1) = 14
          a__isNatList#_A(x1) = 14
          cons_A(x1,x2) = 15
          a__isNat_A(x1) = 26
          a__isNatList_A(x1) = 26
          take_A(x1,x2) = 24
          a__isNatIList_A(x1) = 26
          isNatList_A(x1) = 26
          length_A(x1) = 13
          uTake1_A(x1) = 0
          uTake2_A(x1,x2,x3,x4) = 22
          uLength_A(x1,x2) = 13
          s_A(x1) = 13
          a__and_A(x1,x2) = 26
          a__zeros_A = 16
          |0|_A = 17
          zeros_A = 15
          a__take_A(x1,x2) = 25
          a__uTake1_A(x1) = 0
          nil_A = 25
          a__uTake2_A(x1,x2,x3,x4) = 22
          a__length_A(x1) = 26
          a__uLength_A(x1,x2) = 26
          isNat_A(x1) = 26
    
      precedence:
      
        |0| > mark = a__isNat = a__isNatList = a__isNatIList = a__and = a__uTake1 = nil > a__length > zeros > tt = and = s = a__take > a__uTake2 > uTake2 > uTake1 > length > a__and# = mark# = isNatIList = a__isNatIList# = a__isNatList# = cons = isNatList = uLength > a__uLength > take = a__zeros = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(take) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p9

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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}


-- Reduction pair.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{0, x1 - 8, x2 - 7}
          tt_A = 3
          mark#_A(x1) = max{0, x1 - 7}
          cons_A(x1,x2) = max{x1, x2}
          s_A(x1) = max{8, x1}
          uLength_A(x1,x2) = max{x1, x2 + 9}
          uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 17, x3 + 14, x4 + 14}
          uTake1_A(x1) = max{13, x1 + 8}
          take_A(x1,x2) = max{x1 + 17, x2 + 14}
          length_A(x1) = x1 + 9
          isNatList_A(x1) = x1 + 6
          a__isNatList#_A(x1) = max{0, x1 - 1}
          a__isNatIList#_A(x1) = max{0, x1 - 1}
          a__isNat_A(x1) = x1 + 6
          a__isNatIList_A(x1) = x1 + 6
          a__isNatList_A(x1) = x1 + 6
          isNatIList_A(x1) = x1 + 6
          and_A(x1,x2) = max{5, x1, x2}
          mark_A(x1) = x1
          a__and_A(x1,x2) = max{5, x1, x2}
          a__zeros_A = 0
          |0|_A = 0
          zeros_A = 0
          a__take_A(x1,x2) = max{x1 + 17, x2 + 14}
          a__uTake1_A(x1) = max{13, x1 + 8}
          nil_A = 12
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 17, x3 + 14, x4 + 14}
          a__length_A(x1) = x1 + 9
          a__uLength_A(x1,x2) = max{x1, x2 + 9}
          isNat_A(x1) = x1 + 6
    
      precedence:
      
        a__isNatIList = a__isNatList = mark = a__and = a__length > |0| > a__take > a__uTake2 > a__uLength > s = a__isNat > a__zeros > and > uLength > isNat > cons = take > length > tt > zeros > uTake2 > a__uTake1 > a__and# = mark# = a__isNatList# = a__isNatIList# > uTake1 = isNatIList > nil > isNatList
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = []
        pi(s) = []
        pi(uLength) = [2]
        pi(uTake2) = []
        pi(uTake1) = []
        pi(take) = []
        pi(length) = [1]
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatIList#) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [1, 2]
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = [1, 3]
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 293
          tt_A = 15
          mark#_A(x1) = 293
          cons_A(x1,x2) = 30
          s_A(x1) = 19
          uLength_A(x1,x2) = 2
          uTake2_A(x1,x2,x3,x4) = 28
          uTake1_A(x1) = 27
          take_A(x1,x2) = 3
          length_A(x1) = 26
          isNatList_A(x1) = 28
          a__isNatList#_A(x1) = 293
          a__isNatIList#_A(x1) = 293
          a__isNat_A(x1) = 19
          a__isNatIList_A(x1) = 28
          a__isNatList_A(x1) = 28
          isNatIList_A(x1) = 27
          and_A(x1,x2) = 0
          mark_A(x1) = 28
          a__and_A(x1,x2) = 28
          a__zeros_A = 31
          |0|_A = 11
          zeros_A = 54
          a__take_A(x1,x2) = max{x1 + 257, x2 + 24}
          a__uTake1_A(x1) = 28
          nil_A = 257
          a__uTake2_A(x1,x2,x3,x4) = max{162, x1 + 16}
          a__length_A(x1) = 27
          a__uLength_A(x1,x2) = 26
          isNat_A(x1) = 19
    
      precedence:
      
        a__isNat > s > a__isNatIList = a__isNatList = mark = a__and > isNatIList > and > cons = isNatList > a__take > a__uTake1 > |0| > isNat > a__and# = tt = mark# = a__isNatList# = a__isNatIList# = a__zeros > zeros > uTake1 > uLength = uTake2 = take = a__uTake2 > a__length > nil > length > a__uLength
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(uTake1) = []
        pi(take) = []
        pi(length) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatIList#) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p11

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(IL) -> a__isNatList#(IL)
p7: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p8: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p9: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p10: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p11: mark#(isNatList(X)) -> a__isNatList#(X)
p12: mark#(length(X)) -> mark#(X)
p13: mark#(take(X1,X2)) -> mark#(X1)
p14: mark#(take(X1,X2)) -> mark#(X2)
p15: mark#(uTake1(X)) -> mark#(X)
p16: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p17: mark#(uLength(X1,X2)) -> mark#(X1)
p18: mark#(s(X)) -> mark#(X)
p19: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 + 24, x2 + 29}
          tt_A = 3
          mark#_A(x1) = x1 + 29
          and_A(x1,x2) = max{x1 + 22, x2}
          mark_A(x1) = x1
          isNatIList_A(x1) = max{2, x1}
          a__isNatIList#_A(x1) = x1 + 29
          a__isNatList#_A(x1) = x1 + 29
          cons_A(x1,x2) = max{x1 + 30, x2}
          a__isNat_A(x1) = max{7, x1 - 23}
          a__isNatList_A(x1) = max{2, x1}
          a__isNatIList_A(x1) = max{2, x1}
          isNatList_A(x1) = max{2, x1}
          length_A(x1) = x1 + 35
          take_A(x1,x2) = max{48, x1 + 33, x2 + 47}
          uTake1_A(x1) = max{48, x1 + 29}
          uTake2_A(x1,x2,x3,x4) = max{x1 + 30, x2 + 33, x3 + 48, x4 + 47}
          uLength_A(x1,x2) = max{49, x1 + 30, x2 + 35}
          s_A(x1) = max{34, x1}
          a__and_A(x1,x2) = max{x1 + 22, x2}
          a__zeros_A = 32
          |0|_A = 1
          zeros_A = 32
          a__take_A(x1,x2) = max{48, x1 + 33, x2 + 47}
          a__uTake1_A(x1) = max{48, x1 + 29}
          nil_A = 4
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 30, x2 + 33, x3 + 48, x4 + 47}
          a__length_A(x1) = x1 + 35
          a__uLength_A(x1,x2) = max{49, x1 + 30, x2 + 35}
          isNat_A(x1) = max{7, x1 - 23}
    
      precedence:
      
        and = mark = isNatIList = cons = a__isNatList = a__isNatIList = isNatList = s = a__and = a__zeros = a__take = a__uTake2 = a__length = a__uLength > zeros > a__uTake1 > a__isNat = uTake1 > nil > uTake2 > tt > |0| > take > a__and# = mark# = a__isNatIList# = a__isNatList# = length > isNat > uLength
      
      partial status:
    
        pi(a__and#) = [2]
        pi(tt) = []
        pi(mark#) = [1]
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = [1]
        pi(a__isNatList#) = [1]
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(take) = [1]
        pi(uTake1) = [1]
        pi(uTake2) = [3]
        pi(uLength) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = x2 + 65
          tt_A = 0
          mark#_A(x1) = 65
          and_A(x1,x2) = 0
          mark_A(x1) = 0
          isNatIList_A(x1) = 0
          a__isNatIList#_A(x1) = 65
          a__isNatList#_A(x1) = 65
          cons_A(x1,x2) = 0
          a__isNat_A(x1) = 0
          a__isNatList_A(x1) = 0
          a__isNatIList_A(x1) = 0
          isNatList_A(x1) = 0
          length_A(x1) = 55
          take_A(x1,x2) = max{21, x1}
          uTake1_A(x1) = 0
          uTake2_A(x1,x2,x3,x4) = 0
          uLength_A(x1,x2) = 0
          s_A(x1) = 0
          a__and_A(x1,x2) = 0
          a__zeros_A = 0
          |0|_A = 55
          zeros_A = 57
          a__take_A(x1,x2) = 0
          a__uTake1_A(x1) = 0
          nil_A = 0
          a__uTake2_A(x1,x2,x3,x4) = 0
          a__length_A(x1) = 0
          a__uLength_A(x1,x2) = 0
          isNat_A(x1) = 0
    
      precedence:
      
        zeros > mark = isNatIList = a__isNat = a__isNatList = a__isNatIList = isNatList = a__and = |0| = isNat > a__length > a__uLength > a__uTake1 > a__and# = mark# = a__isNatIList# = a__isNatList# = uTake1 = uLength > tt = a__take = nil = a__uTake2 > cons = a__zeros > length > s > uTake2 > and > take
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(take) = [1]
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p14

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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: a__and#(tt(),T) -> mark#(T)
p2: mark#(cons(X1,X2)) -> mark#(X1)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(uLength(X1,X2)) -> mark#(X1)
p5: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p6: mark#(uTake1(X)) -> mark#(X)
p7: mark#(take(X1,X2)) -> mark#(X1)
p8: mark#(length(X)) -> mark#(X)
p9: mark#(isNatList(X)) -> a__isNatList#(X)
p10: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p11: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p12: mark#(isNatIList(X)) -> a__isNatIList#(X)
p13: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p14: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p15: a__isNatIList#(IL) -> a__isNatList#(IL)
p16: mark#(and(X1,X2)) -> mark#(X2)
p17: mark#(and(X1,X2)) -> mark#(X1)
p18: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{15, x1 - 16, x2 - 4}
          tt_A = 0
          mark#_A(x1) = max{0, x1 - 4}
          cons_A(x1,x2) = max{30, x1, x2}
          s_A(x1) = max{3, x1}
          uLength_A(x1,x2) = max{50, x1 + 10, x2 + 20}
          uTake2_A(x1,x2,x3,x4) = max{30, x1 + 2, x2 + 8, x3 + 27, x4 + 27}
          uTake1_A(x1) = max{5, x1 + 1}
          take_A(x1,x2) = max{30, x1 + 8, x2 + 27}
          length_A(x1) = max{24, x1 + 20}
          isNatList_A(x1) = x1 + 10
          a__isNatList#_A(x1) = x1 + 6
          a__isNat_A(x1) = max{38, x1 - 1}
          a__isNatList_A(x1) = x1 + 10
          isNatIList_A(x1) = x1 + 25
          a__isNatIList#_A(x1) = x1 + 21
          a__isNatIList_A(x1) = x1 + 25
          and_A(x1,x2) = max{19, x1 + 2, x2}
          mark_A(x1) = max{3, x1}
          a__and_A(x1,x2) = max{19, x1 + 2, x2}
          a__zeros_A = 31
          |0|_A = 1
          zeros_A = 31
          a__take_A(x1,x2) = max{30, x1 + 8, x2 + 27}
          a__uTake1_A(x1) = max{5, x1 + 1}
          nil_A = 4
          a__uTake2_A(x1,x2,x3,x4) = max{30, x1 + 2, x2 + 8, x3 + 27, x4 + 27}
          a__length_A(x1) = max{24, x1 + 20}
          a__uLength_A(x1,x2) = max{50, x1 + 10, x2 + 20}
          isNat_A(x1) = max{38, x1 - 1}
    
      precedence:
      
        a__isNat = a__isNatList = a__isNatIList = mark = a__and > nil > a__length > length > a__zeros > zeros > and > a__take > take > |0| > a__uTake1 > a__uTake2 > isNatList > uTake1 > uTake2 > isNatIList > isNat > cons > tt > a__uLength > uLength > a__and# = mark# = s = a__isNatList# = a__isNatIList#
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = []
        pi(s) = []
        pi(uLength) = [1, 2]
        pi(uTake2) = []
        pi(uTake1) = [1]
        pi(take) = [1, 2]
        pi(length) = [1]
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [1, 2]
        pi(a__uTake1) = [1]
        pi(nil) = []
        pi(a__uTake2) = [1]
        pi(a__length) = []
        pi(a__uLength) = [2]
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 17
          tt_A = 36
          mark#_A(x1) = 17
          cons_A(x1,x2) = 16
          s_A(x1) = 37
          uLength_A(x1,x2) = 35
          uTake2_A(x1,x2,x3,x4) = 13
          uTake1_A(x1) = x1
          take_A(x1,x2) = max{43, x2 + 6}
          length_A(x1) = 17
          isNatList_A(x1) = 16
          a__isNatList#_A(x1) = 17
          a__isNat_A(x1) = 37
          a__isNatList_A(x1) = 37
          isNatIList_A(x1) = 1
          a__isNatIList#_A(x1) = 17
          a__isNatIList_A(x1) = 37
          and_A(x1,x2) = 37
          mark_A(x1) = 37
          a__and_A(x1,x2) = 37
          a__zeros_A = 43
          |0|_A = 24
          zeros_A = 35
          a__take_A(x1,x2) = max{x1 + 109, x2 + 6}
          a__uTake1_A(x1) = 0
          nil_A = 2
          a__uTake2_A(x1,x2,x3,x4) = max{13, x1 - 19}
          a__length_A(x1) = 37
          a__uLength_A(x1,x2) = 37
          isNat_A(x1) = 37
    
      precedence:
      
        a__uTake1 > a__take > a__isNat = a__isNatList = a__isNatIList = mark = a__and = a__uLength = isNat > zeros > a__zeros > and > isNatList = |0| = a__uTake2 = a__length > uTake1 > a__and# = mark# = cons = s = length = a__isNatList# = a__isNatIList# = nil > isNatIList > tt = take > uLength > uTake2
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(cons) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(uTake1) = []
        pi(take) = [2]
        pi(length) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [2]
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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}


-- Reduction pair.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{2, x2 - 4}
          tt_A = 19
          mark#_A(x1) = max{0, x1 - 4}
          and_A(x1,x2) = max{15, x1 + 1, x2}
          mark_A(x1) = x1
          isNatIList_A(x1) = max{8, x1}
          a__isNatIList#_A(x1) = max{3, x1 - 4}
          a__isNatList#_A(x1) = max{0, x1 - 4}
          cons_A(x1,x2) = max{x1 + 23, x2}
          a__isNat_A(x1) = x1 + 7
          a__isNatList_A(x1) = x1
          a__isNatIList_A(x1) = max{8, x1}
          isNatList_A(x1) = x1
          length_A(x1) = x1 + 4
          take_A(x1,x2) = max{24, x1 + 15, x2 + 22}
          uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 15, x3 + 23, x4 + 22}
          uLength_A(x1,x2) = max{x1 + 1, x2 + 4}
          s_A(x1) = x1
          a__and_A(x1,x2) = max{15, x1 + 1, x2}
          a__zeros_A = 36
          |0|_A = 13
          zeros_A = 36
          a__take_A(x1,x2) = max{24, x1 + 15, x2 + 22}
          a__uTake1_A(x1) = max{21, x1}
          nil_A = 20
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 15, x3 + 23, x4 + 22}
          a__length_A(x1) = x1 + 4
          a__uLength_A(x1,x2) = max{x1 + 1, x2 + 4}
          uTake1_A(x1) = max{21, x1}
          isNat_A(x1) = x1 + 7
    
      precedence:
      
        a__isNat = isNat > |0| > isNatIList = a__isNatIList > a__isNatList = isNatList > and = mark = a__and = a__zeros = a__take = a__uTake1 = a__length > nil > a__uTake2 > take > cons > a__uLength > tt = uLength > uTake2 = uTake1 > zeros > a__and# = mark# = a__isNatIList# = a__isNatList# = length = s
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = [2]
        pi(mark) = [1]
        pi(isNatIList) = [1]
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = [2]
        pi(a__isNat) = []
        pi(a__isNatList) = [1]
        pi(a__isNatIList) = [1]
        pi(isNatList) = [1]
        pi(length) = []
        pi(take) = [1]
        pi(uTake2) = [1]
        pi(uLength) = [2]
        pi(s) = []
        pi(a__and) = [2]
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [1, 2]
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = [1, 2, 3, 4]
        pi(a__length) = []
        pi(a__uLength) = [1]
        pi(uTake1) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 31
          tt_A = 0
          mark#_A(x1) = 31
          and_A(x1,x2) = 116
          mark_A(x1) = 116
          isNatIList_A(x1) = 32
          a__isNatIList#_A(x1) = 31
          a__isNatList#_A(x1) = 31
          cons_A(x1,x2) = 114
          a__isNat_A(x1) = 204
          a__isNatList_A(x1) = 0
          a__isNatIList_A(x1) = 116
          isNatList_A(x1) = 0
          length_A(x1) = 116
          take_A(x1,x2) = 18
          uTake2_A(x1,x2,x3,x4) = 116
          uLength_A(x1,x2) = 184
          s_A(x1) = 107
          a__and_A(x1,x2) = 116
          a__zeros_A = 115
          |0|_A = 85
          zeros_A = 0
          a__take_A(x1,x2) = max{43, x1 - 26}
          a__uTake1_A(x1) = 116
          nil_A = 115
          a__uTake2_A(x1,x2,x3,x4) = max{x2 + 116, x3 + 116, x4 + 116}
          a__length_A(x1) = 116
          a__uLength_A(x1,x2) = 115
          uTake1_A(x1) = 115
          isNat_A(x1) = 204
    
      precedence:
      
        a__isNat > a__isNatList > uLength > isNatIList > isNat > uTake2 = a__uTake2 > a__and# = mark# = and = mark = a__isNatIList# = a__isNatList# = cons = isNatList = s = a__and = nil = uTake1 > a__length = a__uLength > a__isNatIList > tt > length > |0| > a__uTake1 > a__take > take > a__zeros > zeros
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(take) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = [2]
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p17

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(IL) -> a__isNatList#(IL)
p7: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p8: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p9: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p10: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p11: mark#(isNatList(X)) -> a__isNatList#(X)
p12: mark#(length(X)) -> mark#(X)
p13: mark#(take(X1,X2)) -> mark#(X1)
p14: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p15: mark#(uLength(X1,X2)) -> mark#(X1)
p16: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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}


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(uLength(X1,X2)) -> mark#(X1)
p4: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p5: mark#(take(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> mark#(X)
p7: mark#(isNatList(X)) -> a__isNatList#(X)
p8: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p9: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p10: mark#(isNatIList(X)) -> a__isNatIList#(X)
p11: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p12: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p13: a__isNatIList#(IL) -> a__isNatList#(IL)
p14: mark#(and(X1,X2)) -> mark#(X2)
p15: mark#(and(X1,X2)) -> mark#(X1)
p16: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 - 11, x2 + 5}
          tt_A = 43
          mark#_A(x1) = x1 + 5
          s_A(x1) = max{13, x1}
          uLength_A(x1,x2) = max{1, x1, x2}
          uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 44, x3 + 81, x4 + 46}
          take_A(x1,x2) = max{58, x1 + 44, x2 + 46}
          length_A(x1) = max{1, x1}
          isNatList_A(x1) = max{13, x1}
          a__isNatList#_A(x1) = x1 + 5
          cons_A(x1,x2) = max{48, x1 + 35, x2}
          a__isNat_A(x1) = x1 + 16
          a__isNatList_A(x1) = max{13, x1}
          isNatIList_A(x1) = max{37, x1 + 12}
          a__isNatIList#_A(x1) = x1 + 17
          a__isNatIList_A(x1) = max{37, x1 + 12}
          and_A(x1,x2) = max{36, x1 + 18, x2}
          mark_A(x1) = max{12, x1}
          a__and_A(x1,x2) = max{36, x1 + 18, x2}
          a__zeros_A = 80
          |0|_A = 44
          zeros_A = 80
          a__take_A(x1,x2) = max{58, x1 + 44, x2 + 46}
          a__uTake1_A(x1) = 45
          nil_A = 44
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 6, x2 + 44, x3 + 81, x4 + 46}
          a__length_A(x1) = max{1, x1}
          a__uLength_A(x1,x2) = max{2, x1, x2}
          uTake1_A(x1) = 45
          isNat_A(x1) = x1 + 16
    
      precedence:
      
        a__isNat = isNat > isNatIList = a__isNatIList > isNatList = a__isNatList > and = mark = a__and = a__zeros = a__take > a__uTake1 > nil > a__uTake2 > a__length > uTake2 = length = cons > |0| > zeros > tt = uTake1 > a__uLength > uLength > a__and# = mark# = a__isNatList# = a__isNatIList# > s > take
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(take) = [2]
        pi(length) = []
        pi(isNatList) = [1]
        pi(a__isNatList#) = []
        pi(cons) = [1, 2]
        pi(a__isNat) = []
        pi(a__isNatList) = [1]
        pi(isNatIList) = [1]
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = [1]
        pi(and) = [2]
        pi(mark) = [1]
        pi(a__and) = [2]
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [2]
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = [4]
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 42
          tt_A = 74
          mark#_A(x1) = 42
          s_A(x1) = 116
          uLength_A(x1,x2) = 1
          uTake2_A(x1,x2,x3,x4) = 118
          take_A(x1,x2) = max{111, x2 + 25}
          length_A(x1) = 118
          isNatList_A(x1) = 2
          a__isNatList#_A(x1) = 42
          cons_A(x1,x2) = max{x1 + 117, x2 - 1}
          a__isNat_A(x1) = 29
          a__isNatList_A(x1) = x1 + 5
          isNatIList_A(x1) = 158
          a__isNatIList#_A(x1) = 42
          a__isNatIList_A(x1) = 158
          and_A(x1,x2) = 41
          mark_A(x1) = 117
          a__and_A(x1,x2) = 117
          a__zeros_A = 76
          |0|_A = 118
          zeros_A = 44
          a__take_A(x1,x2) = 24
          a__uTake1_A(x1) = 2
          nil_A = 118
          a__uTake2_A(x1,x2,x3,x4) = max{235, x4 + 119}
          a__length_A(x1) = 75
          a__uLength_A(x1,x2) = 2
          uTake1_A(x1) = 1
          isNat_A(x1) = 28
    
      precedence:
      
        a__isNatList > a__uLength > mark = a__and > a__uTake1 > a__take > and > a__isNatIList > zeros > uLength > isNatIList > cons > isNatList > take = a__length = uTake1 > |0| > nil > a__isNat > length > a__uTake2 = isNat > uTake2 > a__and# = tt = mark# = s = a__isNatList# = a__isNatIList# = a__zeros
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(take) = [2]
        pi(length) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = [1]
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(IL) -> a__isNatList#(IL)
p7: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p8: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p9: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p10: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p11: mark#(isNatList(X)) -> a__isNatList#(X)
p12: mark#(length(X)) -> mark#(X)
p13: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p14: mark#(uLength(X1,X2)) -> mark#(X1)
p15: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 - 8, x2 + 4}
          tt_A = 9
          mark#_A(x1) = x1 + 4
          and_A(x1,x2) = max{16, x1 + 5, x2}
          mark_A(x1) = x1
          isNatIList_A(x1) = x1 + 17
          a__isNatIList#_A(x1) = x1 + 21
          a__isNatList#_A(x1) = max{4, x1}
          cons_A(x1,x2) = max{x1 + 29, x2}
          a__isNat_A(x1) = x1 + 3
          a__isNatList_A(x1) = max{1, x1 - 4}
          a__isNatIList_A(x1) = x1 + 17
          isNatList_A(x1) = max{1, x1 - 4}
          length_A(x1) = x1 + 36
          uTake2_A(x1,x2,x3,x4) = max{x1 + 5, x2 + 33, x3 + 62, x4 + 33}
          uLength_A(x1,x2) = max{x1 + 21, x2 + 36}
          s_A(x1) = max{1, x1}
          a__and_A(x1,x2) = max{16, x1 + 5, x2}
          a__zeros_A = 36
          |0|_A = 7
          zeros_A = 36
          a__take_A(x1,x2) = max{x1 + 33, x2 + 33}
          a__uTake1_A(x1) = 34
          nil_A = 14
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 5, x2 + 33, x3 + 62, x4 + 33}
          take_A(x1,x2) = max{x1 + 33, x2 + 33}
          a__length_A(x1) = x1 + 36
          a__uLength_A(x1,x2) = max{x1 + 21, x2 + 36}
          uTake1_A(x1) = 34
          isNat_A(x1) = x1 + 3
    
      precedence:
      
        and = mark = isNatIList = cons = a__isNatList = a__isNatIList = a__and = a__zeros = a__take = a__uTake2 = take > |0| > a__uTake1 > uTake2 > a__isNat = a__length > a__uLength = isNat > uLength > s > a__and# = mark# = a__isNatIList# = a__isNatList# > isNatList > nil > zeros > tt = length = uTake1
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(uTake2) = []
        pi(uLength) = [2]
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = [1]
        pi(a__uLength) = [2]
        pi(uTake1) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 0
          tt_A = 15
          mark#_A(x1) = 0
          and_A(x1,x2) = 19
          mark_A(x1) = 19
          isNatIList_A(x1) = 19
          a__isNatIList#_A(x1) = 0
          a__isNatList#_A(x1) = 0
          cons_A(x1,x2) = 15
          a__isNat_A(x1) = 19
          a__isNatList_A(x1) = 19
          a__isNatIList_A(x1) = 19
          isNatList_A(x1) = 19
          length_A(x1) = 18
          uTake2_A(x1,x2,x3,x4) = 15
          uLength_A(x1,x2) = max{19, x2 + 18}
          s_A(x1) = 8
          a__and_A(x1,x2) = 19
          a__zeros_A = 18
          |0|_A = 20
          zeros_A = 0
          a__take_A(x1,x2) = 17
          a__uTake1_A(x1) = 18
          nil_A = 20
          a__uTake2_A(x1,x2,x3,x4) = 16
          take_A(x1,x2) = 17
          a__length_A(x1) = max{19, x1}
          a__uLength_A(x1,x2) = x2 + 22
          uTake1_A(x1) = 18
          isNat_A(x1) = 19
    
      precedence:
      
        nil > and = mark = a__isNatList = a__isNatIList = isNatList = a__and > a__isNat > tt > isNatIList = cons = a__uTake1 = uTake1 > |0| > a__zeros > zeros > s = isNat > a__length > a__and# = mark# = a__isNatIList# = a__isNatList# = length > a__uLength > a__take = take > uTake2 = a__uTake2 > uLength
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(length) = []
        pi(uTake2) = []
        pi(uLength) = [2]
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = [2]
        pi(uTake1) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p7: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p8: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p9: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p10: mark#(isNatList(X)) -> a__isNatList#(X)
p11: mark#(length(X)) -> mark#(X)
p12: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p13: mark#(uLength(X1,X2)) -> mark#(X1)
p14: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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}


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(uLength(X1,X2)) -> mark#(X1)
p4: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p5: mark#(length(X)) -> mark#(X)
p6: mark#(isNatList(X)) -> a__isNatList#(X)
p7: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p8: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p9: mark#(isNatIList(X)) -> a__isNatIList#(X)
p10: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p11: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p12: mark#(and(X1,X2)) -> mark#(X2)
p13: mark#(and(X1,X2)) -> mark#(X1)
p14: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{0, x1 - 10, x2 - 2}
          tt_A = 12
          mark#_A(x1) = max{2, x1 - 2}
          s_A(x1) = max{1, x1}
          uLength_A(x1,x2) = max{x1 + 5, x2 + 43}
          uTake2_A(x1,x2,x3,x4) = max{53, x1 + 5, x2 + 44, x3 + 42, x4 + 44}
          length_A(x1) = x1 + 43
          isNatList_A(x1) = x1 + 37
          a__isNatList#_A(x1) = x1 + 35
          cons_A(x1,x2) = max{8, x1 - 1, x2}
          a__isNat_A(x1) = x1 + 22
          a__isNatList_A(x1) = x1 + 37
          isNatIList_A(x1) = x1 + 38
          a__isNatIList#_A(x1) = x1 + 36
          a__isNatIList_A(x1) = x1 + 38
          and_A(x1,x2) = max{x1 + 14, x2}
          mark_A(x1) = x1
          a__and_A(x1,x2) = max{x1 + 14, x2}
          a__zeros_A = 14
          |0|_A = 13
          zeros_A = 14
          a__take_A(x1,x2) = max{53, x1 + 44, x2 + 44}
          a__uTake1_A(x1) = max{57, x1 + 1}
          nil_A = 12
          a__uTake2_A(x1,x2,x3,x4) = max{53, x1 + 5, x2 + 44, x3 + 42, x4 + 44}
          take_A(x1,x2) = max{53, x1 + 44, x2 + 44}
          a__length_A(x1) = x1 + 43
          a__uLength_A(x1,x2) = max{x1 + 5, x2 + 43}
          uTake1_A(x1) = max{57, x1 + 1}
          isNat_A(x1) = x1 + 22
    
      precedence:
      
        a__and# = tt = mark# = s = uLength = uTake2 = length = isNatList = a__isNatList# = cons = a__isNat = a__isNatList = isNatIList = a__isNatIList# = a__isNatIList = and = mark = a__and = a__zeros = |0| = zeros = a__take = a__uTake1 = nil = a__uTake2 = take = a__length = a__uLength = uTake1 = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(length) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 0
          tt_A = 12
          mark#_A(x1) = 0
          s_A(x1) = 10
          uLength_A(x1,x2) = 10
          uTake2_A(x1,x2,x3,x4) = 2
          length_A(x1) = 0
          isNatList_A(x1) = 18
          a__isNatList#_A(x1) = 0
          cons_A(x1,x2) = 18
          a__isNat_A(x1) = 18
          a__isNatList_A(x1) = 18
          isNatIList_A(x1) = 18
          a__isNatIList#_A(x1) = 0
          a__isNatIList_A(x1) = 18
          and_A(x1,x2) = 17
          mark_A(x1) = 18
          a__and_A(x1,x2) = 18
          a__zeros_A = 18
          |0|_A = 17
          zeros_A = 12
          a__take_A(x1,x2) = 18
          a__uTake1_A(x1) = 16
          nil_A = 17
          a__uTake2_A(x1,x2,x3,x4) = 18
          take_A(x1,x2) = 18
          a__length_A(x1) = 17
          a__uLength_A(x1,x2) = 10
          uTake1_A(x1) = 10
          isNat_A(x1) = 17
    
      precedence:
      
        a__length > cons = a__isNat = a__isNatList = a__isNatIList = mark = a__and = a__zeros = a__take = a__uTake2 = uTake1 > a__uTake1 > |0| > uTake2 = length = isNatIList = and = isNat > zeros > a__uLength > s = uLength > nil > tt > a__and# = mark# = isNatList = a__isNatList# = a__isNatIList# = take
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uLength) = []
        pi(uTake2) = []
        pi(length) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p4: mark#(length(X)) -> mark#(X)
p5: mark#(isNatList(X)) -> a__isNatList#(X)
p6: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p7: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p8: mark#(isNatIList(X)) -> a__isNatIList#(X)
p9: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p10: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p11: mark#(and(X1,X2)) -> mark#(X2)
p12: mark#(and(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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}


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: mark#(isNatList(X)) -> a__isNatList#(X)
p9: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p10: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p11: mark#(length(X)) -> mark#(X)
p12: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p13: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 + 8, x2 + 26}
          tt_A = 18
          mark#_A(x1) = x1 + 26
          and_A(x1,x2) = max{23, x1, x2}
          mark_A(x1) = max{23, x1}
          isNatIList_A(x1) = 23
          a__isNatIList#_A(x1) = 49
          cons_A(x1,x2) = x2 + 18
          a__isNat_A(x1) = 23
          a__isNatIList_A(x1) = 23
          isNatList_A(x1) = 23
          a__isNatList#_A(x1) = 49
          a__isNatList_A(x1) = 23
          length_A(x1) = max{25, x1 + 1}
          uTake2_A(x1,x2,x3,x4) = max{16, x1}
          s_A(x1) = max{22, x1}
          a__and_A(x1,x2) = max{23, x1, x2}
          a__zeros_A = 22
          |0|_A = 30
          zeros_A = 0
          a__take_A(x1,x2) = 23
          a__uTake1_A(x1) = max{20, x1 - 43}
          nil_A = 19
          a__uTake2_A(x1,x2,x3,x4) = max{17, x1}
          take_A(x1,x2) = 0
          a__length_A(x1) = max{25, x1 + 1}
          a__uLength_A(x1,x2) = max{25, x1 - 6, x2 + 17}
          uTake1_A(x1) = max{20, x1 - 43}
          uLength_A(x1,x2) = max{25, x1 - 6, x2 + 17}
          isNat_A(x1) = 23
    
      precedence:
      
        a__and# = tt = mark# = and = mark = isNatIList = a__isNatIList# = cons = a__isNat = a__isNatIList = isNatList = a__isNatList# = a__isNatList = length = uTake2 = s = a__and = a__zeros = |0| = zeros = a__take = a__uTake1 = nil = a__uTake2 = take = a__length = a__uLength = uTake1 = uLength = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(length) = []
        pi(uTake2) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 18
          tt_A = 58
          mark#_A(x1) = 18
          and_A(x1,x2) = 170
          mark_A(x1) = 174
          isNatIList_A(x1) = 11
          a__isNatIList#_A(x1) = 18
          cons_A(x1,x2) = 24
          a__isNat_A(x1) = 174
          a__isNatIList_A(x1) = 174
          isNatList_A(x1) = 19
          a__isNatList#_A(x1) = 18
          a__isNatList_A(x1) = 174
          length_A(x1) = 1
          uTake2_A(x1,x2,x3,x4) = 57
          s_A(x1) = 130
          a__and_A(x1,x2) = 174
          a__zeros_A = 56
          |0|_A = 57
          zeros_A = 49
          a__take_A(x1,x2) = 164
          a__uTake1_A(x1) = 174
          nil_A = 175
          a__uTake2_A(x1,x2,x3,x4) = 148
          take_A(x1,x2) = 90
          a__length_A(x1) = 173
          a__uLength_A(x1,x2) = 131
          uTake1_A(x1) = 1
          uLength_A(x1,x2) = 116
          isNat_A(x1) = 174
    
      precedence:
      
        and > a__and# = tt = mark# = mark = isNatIList = a__isNatIList# = a__isNat = a__isNatIList = a__isNatList# = a__isNatList = length = a__and = isNat > isNatList > a__zeros > zeros > |0| > a__take = take = uLength > a__uTake2 > uTake2 > a__length > cons = a__uTake1 = nil = a__uLength = uTake1 > s
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(length) = []
        pi(uTake2) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(uTake1) = []
        pi(uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p11

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: mark#(isNatList(X)) -> a__isNatList#(X)
p9: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p10: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p11: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p12: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(uTake2(X1,X2,X3,X4)) -> mark#(X1)
p4: mark#(isNatList(X)) -> a__isNatList#(X)
p5: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p6: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p7: mark#(isNatIList(X)) -> a__isNatIList#(X)
p8: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p9: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p10: mark#(and(X1,X2)) -> mark#(X2)
p11: mark#(and(X1,X2)) -> mark#(X1)
p12: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{0, x1 - 10, x2 - 10}
          tt_A = 36
          mark#_A(x1) = max{1, x1 - 10}
          s_A(x1) = max{2, x1}
          uTake2_A(x1,x2,x3,x4) = max{x1 + 15, x2 + 52, x3 + 116, x4 + 97}
          isNatList_A(x1) = x1 + 42
          a__isNatList#_A(x1) = x1 + 32
          cons_A(x1,x2) = max{x1 + 19, x2}
          a__isNat_A(x1) = max{10, x1 - 4}
          a__isNatList_A(x1) = x1 + 42
          isNatIList_A(x1) = x1 + 42
          a__isNatIList#_A(x1) = x1 + 32
          a__isNatIList_A(x1) = x1 + 42
          and_A(x1,x2) = max{x1 + 41, x2}
          mark_A(x1) = x1
          a__and_A(x1,x2) = max{x1 + 41, x2}
          a__zeros_A = 60
          |0|_A = 41
          zeros_A = 60
          a__take_A(x1,x2) = max{x1 + 52, x2 + 97}
          a__uTake1_A(x1) = 94
          nil_A = 0
          a__uTake2_A(x1,x2,x3,x4) = max{x1 + 15, x2 + 52, x3 + 116, x4 + 97}
          take_A(x1,x2) = max{x1 + 52, x2 + 97}
          a__length_A(x1) = x1 + 52
          a__uLength_A(x1,x2) = max{x1 - 33, x2 + 52}
          length_A(x1) = x1 + 52
          uTake1_A(x1) = 94
          uLength_A(x1,x2) = max{x1 - 33, x2 + 52}
          isNat_A(x1) = max{10, x1 - 4}
    
      precedence:
      
        a__and# = tt = mark# = s = uTake2 = isNatList = a__isNatList# = cons = a__isNat = a__isNatList = isNatIList = a__isNatIList# = a__isNatIList = and = mark = a__and = a__zeros = |0| = zeros = a__take = a__uTake1 = nil = a__uTake2 = take = a__length = a__uLength = length = uTake1 = uLength = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uTake2) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 54
          tt_A = 67
          mark#_A(x1) = 54
          s_A(x1) = 27
          uTake2_A(x1,x2,x3,x4) = 68
          isNatList_A(x1) = 0
          a__isNatList#_A(x1) = 54
          cons_A(x1,x2) = 68
          a__isNat_A(x1) = 75
          a__isNatList_A(x1) = 75
          isNatIList_A(x1) = 75
          a__isNatIList#_A(x1) = 54
          a__isNatIList_A(x1) = 75
          and_A(x1,x2) = 53
          mark_A(x1) = 75
          a__and_A(x1,x2) = 75
          a__zeros_A = 75
          |0|_A = 74
          zeros_A = 67
          a__take_A(x1,x2) = 69
          a__uTake1_A(x1) = 75
          nil_A = 37
          a__uTake2_A(x1,x2,x3,x4) = 68
          take_A(x1,x2) = 27
          a__length_A(x1) = 74
          a__uLength_A(x1,x2) = 56
          length_A(x1) = 74
          uTake1_A(x1) = 29
          uLength_A(x1,x2) = 55
          isNat_A(x1) = 27
    
      precedence:
      
        a__uTake2 > a__and# = mark# = uTake2 = a__isNatList# = cons = a__isNatIList# > a__isNatList = a__isNatIList = mark = a__and = uTake1 > a__zeros > zeros > a__take > a__uTake1 > a__length > and > take > s = a__isNat = isNatIList = |0| = a__uLength = isNat > length > tt = nil = uLength > isNatList
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(uTake2) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(isNatList(X)) -> a__isNatList#(X)
p4: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p5: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p6: mark#(isNatIList(X)) -> a__isNatIList#(X)
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p9: mark#(and(X1,X2)) -> mark#(X2)
p10: mark#(and(X1,X2)) -> mark#(X1)
p11: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> mark#(X2)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: mark#(isNatList(X)) -> a__isNatList#(X)
p9: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p10: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p11: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 - 80, x2 + 124}
          tt_A = 172
          mark#_A(x1) = x1 + 124
          and_A(x1,x2) = max{327, x1 + 79, x2}
          mark_A(x1) = max{202, x1}
          isNatIList_A(x1) = x1 + 163
          a__isNatIList#_A(x1) = x1 + 287
          cons_A(x1,x2) = max{197, x1 - 4, x2}
          a__isNat_A(x1) = max{260, x1 + 77}
          a__isNatIList_A(x1) = x1 + 163
          isNatList_A(x1) = x1 + 161
          a__isNatList#_A(x1) = x1 + 285
          a__isNatList_A(x1) = x1 + 161
          s_A(x1) = max{261, x1}
          a__and_A(x1,x2) = max{327, x1 + 79, x2}
          a__zeros_A = 201
          |0|_A = 94
          zeros_A = 171
          a__take_A(x1,x2) = max{381, x1 + 179, x2 + 165}
          a__uTake1_A(x1) = max{274, x1 + 1}
          nil_A = 12
          a__uTake2_A(x1,x2,x3,x4) = max{382, x2 + 179, x3 + 160, x4 + 165}
          take_A(x1,x2) = max{381, x1 + 179, x2 + 165}
          a__length_A(x1) = max{371, x1 + 162}
          a__uLength_A(x1,x2) = max{371, x2 + 162}
          length_A(x1) = max{371, x1 + 162}
          uTake1_A(x1) = max{274, x1 + 1}
          uTake2_A(x1,x2,x3,x4) = max{382, x2 + 179, x3 + 160, x4 + 165}
          uLength_A(x1,x2) = max{371, x2 + 162}
          isNat_A(x1) = max{260, x1 + 77}
    
      precedence:
      
        |0| > and = mark = a__isNatIList = a__isNatList = a__and > a__zeros > a__length > a__uLength > isNatList > a__take = a__uTake2 > a__uTake1 > isNatIList > cons > a__isNat = take > isNat > length > uLength > nil > tt = uTake1 > a__and# = mark# = a__isNatIList# = a__isNatList# = s = zeros = uTake2
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(isNatList) = [1]
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [2]
        pi(a__uTake1) = [1]
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = [2]
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 21
          tt_A = 631
          mark#_A(x1) = 21
          and_A(x1,x2) = 102
          mark_A(x1) = 102
          isNatIList_A(x1) = 103
          a__isNatIList#_A(x1) = 21
          cons_A(x1,x2) = 298
          a__isNat_A(x1) = 405
          a__isNatIList_A(x1) = 102
          isNatList_A(x1) = 20
          a__isNatList#_A(x1) = 21
          a__isNatList_A(x1) = 102
          s_A(x1) = 11
          a__and_A(x1,x2) = 102
          a__zeros_A = 101
          |0|_A = 0
          zeros_A = 0
          a__take_A(x1,x2) = max{101, x2 + 16}
          a__uTake1_A(x1) = 101
          nil_A = 100
          a__uTake2_A(x1,x2,x3,x4) = 313
          take_A(x1,x2) = 17
          a__length_A(x1) = 102
          a__uLength_A(x1,x2) = 102
          length_A(x1) = 102
          uTake1_A(x1) = 100
          uTake2_A(x1,x2,x3,x4) = 312
          uLength_A(x1,x2) = 81
          isNat_A(x1) = 405
    
      precedence:
      
        a__isNat > a__take > cons > tt = uLength > mark = a__isNatIList = a__isNatList = a__and = nil > isNatIList > a__uTake1 > a__uTake2 > zeros = isNat > uTake2 > take > a__and# = mark# = a__isNatIList# = isNatList = a__isNatList# = a__length = length > a__uLength > s = uTake1 > and > a__zeros > |0|
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(s) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))
p3: mark#(and(X1,X2)) -> mark#(X2)
p4: mark#(isNatIList(X)) -> a__isNatIList#(X)
p5: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p6: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p7: mark#(isNatList(X)) -> a__isNatList#(X)
p8: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p9: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p10: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__and#(tt(),T) -> mark#(T)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(isNatList(X)) -> a__isNatList#(X)
p4: a__isNatList#(cons(N,L)) -> a__isNatList#(L)
p5: a__isNatList#(cons(N,L)) -> a__and#(a__isNat(N),a__isNatList(L))
p6: mark#(isNatIList(X)) -> a__isNatIList#(X)
p7: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p8: a__isNatIList#(cons(N,IL)) -> a__and#(a__isNat(N),a__isNatIList(IL))
p9: mark#(and(X1,X2)) -> mark#(X2)
p10: mark#(and(X1,X2)) -> a__and#(mark(X1),mark(X2))

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{x1 - 126, x2 + 19}
          tt_A = 134
          mark#_A(x1) = x1 + 19
          s_A(x1) = max{99, x1 + 26}
          isNatList_A(x1) = max{59, x1 - 35}
          a__isNatList#_A(x1) = max{78, x1 - 17}
          cons_A(x1,x2) = max{x1, x2 + 26}
          a__isNat_A(x1) = x1 + 104
          a__isNatList_A(x1) = max{59, x1 - 35}
          isNatIList_A(x1) = max{135, x1 - 20}
          a__isNatIList#_A(x1) = max{154, x1 - 21}
          a__isNatIList_A(x1) = max{135, x1 - 20}
          and_A(x1,x2) = max{57, x1 - 139, x2}
          mark_A(x1) = max{37, x1}
          a__and_A(x1,x2) = max{57, x1 - 139, x2}
          a__zeros_A = 32
          |0|_A = 31
          zeros_A = 0
          a__take_A(x1,x2) = max{207, x1 + 136, x2 + 169}
          a__uTake1_A(x1) = max{168, x1 + 37}
          nil_A = 170
          a__uTake2_A(x1,x2,x3,x4) = max{208, x1 + 100, x2 + 162, x3 + 1, x4 + 195}
          take_A(x1,x2) = max{207, x1 + 136, x2 + 169}
          a__length_A(x1) = x1
          a__uLength_A(x1,x2) = max{x1 - 34, x2 + 26}
          length_A(x1) = x1
          uTake1_A(x1) = max{168, x1 + 37}
          uTake2_A(x1,x2,x3,x4) = max{208, x1 + 100, x2 + 162, x3 + 1, x4 + 195}
          uLength_A(x1,x2) = max{x1 - 34, x2 + 26}
          isNat_A(x1) = x1 + 104
    
      precedence:
      
        a__and# = tt = mark# = s = isNatList = a__isNatList# = cons = a__isNat = a__isNatList = isNatIList = a__isNatIList# = a__isNatIList = and = mark = a__and = a__zeros = |0| = zeros = a__take = a__uTake1 = nil = a__uTake2 = take = a__length = a__uLength = length = uTake1 = uTake2 = uLength = isNat
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 29
          tt_A = 25
          mark#_A(x1) = 29
          s_A(x1) = 5
          isNatList_A(x1) = 1
          a__isNatList#_A(x1) = 29
          cons_A(x1,x2) = 22
          a__isNat_A(x1) = 33
          a__isNatList_A(x1) = 33
          isNatIList_A(x1) = 32
          a__isNatIList#_A(x1) = 29
          a__isNatIList_A(x1) = 33
          and_A(x1,x2) = 30
          mark_A(x1) = 33
          a__and_A(x1,x2) = 33
          a__zeros_A = 23
          |0|_A = 24
          zeros_A = 15
          a__take_A(x1,x2) = 26
          a__uTake1_A(x1) = 25
          nil_A = 26
          a__uTake2_A(x1,x2,x3,x4) = 23
          take_A(x1,x2) = 24
          a__length_A(x1) = max{20, x1}
          a__uLength_A(x1,x2) = 16
          length_A(x1) = 10
          uTake1_A(x1) = 17
          uTake2_A(x1,x2,x3,x4) = 15
          uLength_A(x1,x2) = 15
          isNat_A(x1) = 32
    
      precedence:
      
        a__zeros > zeros > take > a__uTake2 > length > uTake1 > a__uTake1 > |0| > a__isNat = a__isNatList = a__isNatIList = mark = a__and > a__length > a__uLength > a__and# = mark# = a__isNatList# = a__isNatIList# > isNatList > a__take > isNat > tt = cons = and = nil > s > uLength > isNatIList > uTake2
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatList) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(a__isNatIList) = []
        pi(and) = []
        pi(mark) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = max{3, x1 - 323, x2 - 169}
          tt_A = 305
          mark#_A(x1) = max{2, x1 - 170}
          and_A(x1,x2) = max{259, x1 - 79, x2 + 4}
          mark_A(x1) = max{88, x1}
          isNatIList_A(x1) = x1 + 243
          a__isNatIList#_A(x1) = x1 + 70
          cons_A(x1,x2) = max{86, x1 - 66, x2 + 23}
          a__isNat_A(x1) = max{328, x1 + 2}
          a__isNatIList_A(x1) = x1 + 243
          isNatList_A(x1) = x1 + 186
          a__isNatList#_A(x1) = max{1, x1 - 5}
          a__isNatList_A(x1) = x1 + 186
          a__and_A(x1,x2) = max{259, x1 - 79, x2 + 4}
          a__zeros_A = 87
          |0|_A = 152
          zeros_A = 63
          a__take_A(x1,x2) = max{188, x1 + 99, x2 + 62}
          a__uTake1_A(x1) = max{250, x1 - 182}
          nil_A = 249
          s_A(x1) = max{327, x1 + 23}
          a__uTake2_A(x1,x2,x3,x4) = max{211, x2 + 122, x3 - 4, x4 + 85}
          take_A(x1,x2) = max{188, x1 + 99, x2 + 62}
          a__length_A(x1) = max{326, x1 + 237}
          a__uLength_A(x1,x2) = max{326, x1 + 67, x2 + 260}
          length_A(x1) = max{326, x1 + 237}
          uTake1_A(x1) = max{250, x1 - 182}
          uTake2_A(x1,x2,x3,x4) = max{211, x2 + 122, x3 - 4, x4 + 85}
          uLength_A(x1,x2) = max{326, x1 + 67, x2 + 260}
          isNat_A(x1) = max{328, x1 + 2}
    
      precedence:
      
        |0| > mark# > a__and# = a__isNatList# > mark = a__isNat = a__zeros = isNat > a__uTake1 > a__take > zeros > take > a__isNatList > tt = isNatIList = a__isNatIList# = a__isNatIList = a__and > a__length > a__uLength > uTake1 > a__uTake2 > nil > cons > isNatList > uTake2 > length > and > s > uLength
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = [2]
        pi(mark) = [1]
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = [1]
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = [1, 2]
        pi(a__uTake1) = []
        pi(nil) = []
        pi(s) = [1]
        pi(a__uTake2) = [2, 4]
        pi(take) = [2]
        pi(a__length) = []
        pi(a__uLength) = [1, 2]
        pi(length) = [1]
        pi(uTake1) = []
        pi(uTake2) = [4]
        pi(uLength) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__and#_A(x1,x2) = 194
          tt_A = 1
          mark#_A(x1) = 156
          and_A(x1,x2) = 116
          mark_A(x1) = x1 + 158
          isNatIList_A(x1) = 16
          a__isNatIList#_A(x1) = 5
          cons_A(x1,x2) = 193
          a__isNat_A(x1) = 6
          a__isNatIList_A(x1) = 15
          isNatList_A(x1) = 6
          a__isNatList#_A(x1) = 167
          a__isNatList_A(x1) = 5
          a__and_A(x1,x2) = 4
          a__zeros_A = 194
          |0|_A = 0
          zeros_A = 37
          a__take_A(x1,x2) = max{x1 + 203, x2 - 179}
          a__uTake1_A(x1) = 3
          nil_A = 2
          s_A(x1) = 1
          a__uTake2_A(x1,x2,x3,x4) = max{13, x4 - 453}
          take_A(x1,x2) = 202
          a__length_A(x1) = 166
          a__uLength_A(x1,x2) = max{167, x1 - 37}
          length_A(x1) = x1 + 9
          uTake1_A(x1) = 1
          uTake2_A(x1,x2,x3,x4) = 0
          uLength_A(x1,x2) = 10
          isNat_A(x1) = 1
    
      precedence:
      
        mark > a__isNat > a__length > |0| > a__uTake1 > a__isNatIList = a__isNatList = a__take > isNatIList > take > a__and > a__zeros = zeros > a__and# = mark# = a__isNatIList# = cons > a__isNatList# > isNat > and > uLength > a__uTake2 > a__uLength > isNatList = length > tt = uTake1 > s > nil = uTake2
      
      partial status:
    
        pi(a__and#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(and) = []
        pi(mark) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(cons) = []
        pi(a__isNat) = []
        pi(a__isNatIList) = []
        pi(isNatList) = []
        pi(a__isNatList#) = []
        pi(a__isNatList) = []
        pi(a__and) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__take) = []
        pi(a__uTake1) = []
        pi(nil) = []
        pi(s) = []
        pi(a__uTake2) = []
        pi(take) = []
        pi(a__length) = []
        pi(a__uLength) = []
        pi(length) = []
        pi(uTake1) = []
        pi(uTake2) = []
        pi(uLength) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p1, p2, p4, p5, p7, p8

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(and(X1,X2)) -> mark#(X2)
p2: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)
p3: a__isNatList#(cons(N,L)) -> a__isNatList#(L)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1}
  {p2}
  {p3}


-- Reduction pair.

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

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

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 2
          and_A(x1,x2) = max{x1 + 2, x2 + 2}
    
      precedence:
      
        and > mark#
      
      partial status:
    
        pi(mark#) = [1]
        pi(and) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          and_A(x1,x2) = max{x1 - 1, x2}
    
      precedence:
      
        mark# = and
      
      partial status:
    
        pi(mark#) = []
        pi(and) = [2]
    

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: a__isNatIList#(cons(N,IL)) -> a__isNatIList#(IL)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatIList#_A(x1) = max{3, x1 + 2}
          cons_A(x1,x2) = max{1, x2}
    
      precedence:
      
        a__isNatIList# = cons
      
      partial status:
    
        pi(a__isNatIList#) = [1]
        pi(cons) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatIList#_A(x1) = max{3, x1 + 2}
          cons_A(x1,x2) = x2 + 1
    
      precedence:
      
        a__isNatIList# = cons
      
      partial status:
    
        pi(a__isNatIList#) = []
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: a__isNatList#(cons(N,L)) -> a__isNatList#(L)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatList#_A(x1) = max{3, x1 + 2}
          cons_A(x1,x2) = max{1, x2}
    
      precedence:
      
        a__isNatList# = cons
      
      partial status:
    
        pi(a__isNatList#) = [1]
        pi(cons) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatList#_A(x1) = max{3, x1 + 2}
          cons_A(x1,x2) = x2 + 1
    
      precedence:
      
        a__isNatList# = cons
      
      partial status:
    
        pi(a__isNatList#) = []
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: a__isNat#(s(N)) -> a__isNat#(N)

and R consists of:

r1: a__and(tt(),T) -> mark(T)
r2: a__isNatIList(IL) -> a__isNatList(IL)
r3: a__isNat(|0|()) -> tt()
r4: a__isNat(s(N)) -> a__isNat(N)
r5: a__isNat(length(L)) -> a__isNatList(L)
r6: a__isNatIList(zeros()) -> tt()
r7: a__isNatIList(cons(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r8: a__isNatList(nil()) -> tt()
r9: a__isNatList(cons(N,L)) -> a__and(a__isNat(N),a__isNatList(L))
r10: a__isNatList(take(N,IL)) -> a__and(a__isNat(N),a__isNatIList(IL))
r11: a__zeros() -> cons(|0|(),zeros())
r12: a__take(|0|(),IL) -> a__uTake1(a__isNatIList(IL))
r13: a__uTake1(tt()) -> nil()
r14: a__take(s(M),cons(N,IL)) -> a__uTake2(a__and(a__isNat(M),a__and(a__isNat(N),a__isNatIList(IL))),M,N,IL)
r15: a__uTake2(tt(),M,N,IL) -> cons(mark(N),take(M,IL))
r16: a__length(cons(N,L)) -> a__uLength(a__and(a__isNat(N),a__isNatList(L)),L)
r17: a__uLength(tt(),L) -> s(a__length(mark(L)))
r18: mark(and(X1,X2)) -> a__and(mark(X1),mark(X2))
r19: mark(isNatIList(X)) -> a__isNatIList(X)
r20: mark(isNatList(X)) -> a__isNatList(X)
r21: mark(isNat(X)) -> a__isNat(X)
r22: mark(length(X)) -> a__length(mark(X))
r23: mark(zeros()) -> a__zeros()
r24: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r25: mark(uTake1(X)) -> a__uTake1(mark(X))
r26: mark(uTake2(X1,X2,X3,X4)) -> a__uTake2(mark(X1),X2,X3,X4)
r27: mark(uLength(X1,X2)) -> a__uLength(mark(X1),X2)
r28: mark(tt()) -> tt()
r29: mark(|0|()) -> |0|()
r30: mark(s(X)) -> s(mark(X))
r31: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r32: mark(nil()) -> nil()
r33: a__and(X1,X2) -> and(X1,X2)
r34: a__isNatIList(X) -> isNatIList(X)
r35: a__isNatList(X) -> isNatList(X)
r36: a__isNat(X) -> isNat(X)
r37: a__length(X) -> length(X)
r38: a__zeros() -> zeros()
r39: a__take(X1,X2) -> take(X1,X2)
r40: a__uTake1(X) -> uTake1(X)
r41: a__uTake2(X1,X2,X3,X4) -> uTake2(X1,X2,X3,X4)
r42: a__uLength(X1,X2) -> uLength(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNat#_A(x1) = max{4, x1 + 3}
          s_A(x1) = max{3, x1 + 2}
    
      precedence:
      
        a__isNat# = s
      
      partial status:
    
        pi(a__isNat#) = [1]
        pi(s) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNat#_A(x1) = max{1, x1 - 1}
          s_A(x1) = x1
    
      precedence:
      
        a__isNat# = s
      
      partial status:
    
        pi(a__isNat#) = []
        pi(s) = [1]
    

The next rules are strictly ordered:

  p1

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