YES

We show the termination of the TRS R:

  a__zeros() -> cons(|0|(),zeros())
  a__U11(tt(),L) -> s(a__length(mark(L)))
  a__and(tt(),X) -> mark(X)
  a__isNat(|0|()) -> tt()
  a__isNat(length(V1)) -> a__isNatList(V1)
  a__isNat(s(V1)) -> a__isNat(V1)
  a__isNatIList(V) -> a__isNatList(V)
  a__isNatIList(zeros()) -> tt()
  a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
  a__isNatList(nil()) -> tt()
  a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
  a__length(nil()) -> |0|()
  a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
  mark(zeros()) -> a__zeros()
  mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
  mark(length(X)) -> a__length(mark(X))
  mark(and(X1,X2)) -> a__and(mark(X1),X2)
  mark(isNat(X)) -> a__isNat(X)
  mark(isNatList(X)) -> a__isNatList(X)
  mark(isNatIList(X)) -> a__isNatIList(X)
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(|0|()) -> |0|()
  mark(tt()) -> tt()
  mark(s(X)) -> s(mark(X))
  mark(nil()) -> nil()
  a__zeros() -> zeros()
  a__U11(X1,X2) -> U11(X1,X2)
  a__length(X) -> length(X)
  a__and(X1,X2) -> and(X1,X2)
  a__isNat(X) -> isNat(X)
  a__isNatList(X) -> isNatList(X)
  a__isNatIList(X) -> isNatIList(X)

-- SCC decomposition.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))
p2: a__U11#(tt(),L) -> mark#(L)
p3: a__and#(tt(),X) -> mark#(X)
p4: a__isNat#(length(V1)) -> a__isNatList#(V1)
p5: a__isNat#(s(V1)) -> a__isNat#(V1)
p6: a__isNatIList#(V) -> a__isNatList#(V)
p7: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p8: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p9: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p10: a__isNatList#(cons(V1,V2)) -> a__isNat#(V1)
p11: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p12: a__length#(cons(N,L)) -> a__and#(a__isNatList(L),isNat(N))
p13: a__length#(cons(N,L)) -> a__isNatList#(L)
p14: mark#(zeros()) -> a__zeros#()
p15: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p16: mark#(U11(X1,X2)) -> mark#(X1)
p17: mark#(length(X)) -> a__length#(mark(X))
p18: mark#(length(X)) -> mark#(X)
p19: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p20: mark#(and(X1,X2)) -> mark#(X1)
p21: mark#(isNat(X)) -> a__isNat#(X)
p22: mark#(isNatList(X)) -> a__isNatList#(X)
p23: mark#(isNatIList(X)) -> a__isNatIList#(X)
p24: mark#(cons(X1,X2)) -> mark#(X1)
p25: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

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}


-- Reduction pair.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__isNatList#(L)
p3: a__isNatList#(cons(V1,V2)) -> a__isNat#(V1)
p4: a__isNat#(s(V1)) -> a__isNat#(V1)
p5: a__isNat#(length(V1)) -> a__isNatList#(V1)
p6: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(s(X)) -> mark#(X)
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(isNatIList(X)) -> a__isNatIList#(X)
p11: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p12: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p13: a__isNatIList#(V) -> a__isNatList#(V)
p14: mark#(isNatList(X)) -> a__isNatList#(X)
p15: mark#(isNat(X)) -> a__isNat#(X)
p16: mark#(and(X1,X2)) -> mark#(X1)
p17: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p18: mark#(length(X)) -> mark#(X)
p19: mark#(length(X)) -> a__length#(mark(X))
p20: a__length#(cons(N,L)) -> a__and#(a__isNatList(L),isNat(N))
p21: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p22: a__U11#(tt(),L) -> mark#(L)
p23: mark#(U11(X1,X2)) -> mark#(X1)
p24: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = max{90, x1 - 115, x2 + 50}
          tt_A = 117
          a__length#_A(x1) = max{90, x1 - 52}
          mark_A(x1) = max{141, x1 + 35}
          cons_A(x1,x2) = max{105, x1, x2 + 102}
          a__isNatList#_A(x1) = x1 + 15
          a__isNat#_A(x1) = max{2, x1 - 56}
          s_A(x1) = max{129, x1}
          length_A(x1) = max{232, x1 + 92}
          a__and#_A(x1,x2) = max{x1 - 105, x2 + 2}
          a__isNat_A(x1) = max{116, x1 - 21}
          isNatList_A(x1) = max{19, x1 + 18}
          mark#_A(x1) = max{1, x1 - 1}
          isNatIList_A(x1) = x1 + 100
          a__isNatIList#_A(x1) = x1 + 98
          isNat_A(x1) = max{80, x1 - 55}
          and_A(x1,x2) = max{x1 + 11, x2 + 118}
          a__isNatList_A(x1) = max{52, x1 + 51}
          a__and_A(x1,x2) = max{152, x1 + 11, x2 + 118}
          U11_A(x1,x2) = max{234, x1, x2 + 128}
          a__zeros_A = 140
          |0|_A = 139
          zeros_A = 37
          a__U11_A(x1,x2) = max{234, x1, x2 + 128}
          a__length_A(x1) = max{234, x1 + 92}
          a__isNatIList_A(x1) = max{129, x1 + 128}
          nil_A = 142
    
      precedence:
      
        mark = |0| > a__zeros > cons > a__and# > a__U11# = a__length# = mark# > a__isNatList > a__and > a__length > a__U11 > isNatList > length = a__isNatIList# = and > a__isNatIList > isNatIList > a__isNat > isNat > U11 > tt = nil > a__isNatList# = a__isNat# = s = zeros
      
      partial status:
    
        pi(a__U11#) = []
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = []
        pi(cons) = []
        pi(a__isNatList#) = [1]
        pi(a__isNat#) = []
        pi(s) = []
        pi(length) = []
        pi(a__and#) = [2]
        pi(a__isNat) = []
        pi(isNatList) = []
        pi(mark#) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = [1]
        pi(isNat) = []
        pi(and) = []
        pi(a__isNatList) = []
        pi(a__and) = []
        pi(U11) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__U11) = []
        pi(a__length) = [1]
        pi(a__isNatIList) = [1]
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = 0
          tt_A = 120
          a__length#_A(x1) = 0
          mark_A(x1) = 137
          cons_A(x1,x2) = 53
          a__isNatList#_A(x1) = 0
          a__isNat#_A(x1) = 0
          s_A(x1) = 112
          length_A(x1) = 1
          a__and#_A(x1,x2) = x2
          a__isNat_A(x1) = 122
          isNatList_A(x1) = 96
          mark#_A(x1) = 0
          isNatIList_A(x1) = 86
          a__isNatIList#_A(x1) = 86
          isNat_A(x1) = 0
          and_A(x1,x2) = 17
          a__isNatList_A(x1) = 122
          a__and_A(x1,x2) = 137
          U11_A(x1,x2) = 137
          a__zeros_A = 60
          |0|_A = 119
          zeros_A = 34
          a__U11_A(x1,x2) = 137
          a__length_A(x1) = max{137, x1 - 20}
          a__isNatIList_A(x1) = max{123, x1 - 29}
          nil_A = 138
    
      precedence:
      
        tt > a__length > length > s > a__isNatIList# > a__U11# = a__length# = isNatIList = and > a__and# > isNat > a__U11 = nil > mark = a__and = U11 > a__isNat > a__zeros = |0| > a__isNatIList > a__isNatList > cons = a__isNatList# = a__isNat# = isNatList = mark# = zeros
      
      partial status:
    
        pi(a__U11#) = []
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = []
        pi(cons) = []
        pi(a__isNatList#) = []
        pi(a__isNat#) = []
        pi(s) = []
        pi(length) = []
        pi(a__and#) = [2]
        pi(a__isNat) = []
        pi(isNatList) = []
        pi(mark#) = []
        pi(isNatIList) = []
        pi(a__isNatIList#) = []
        pi(isNat) = []
        pi(and) = []
        pi(a__isNatList) = []
        pi(a__and) = []
        pi(U11) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__U11) = []
        pi(a__length) = []
        pi(a__isNatIList) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p2, p6, p10, p13, p14, p17, p19, p20, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))
p2: a__isNatList#(cons(V1,V2)) -> a__isNat#(V1)
p3: a__isNat#(s(V1)) -> a__isNat#(V1)
p4: a__isNat#(length(V1)) -> a__isNatList#(V1)
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(s(X)) -> mark#(X)
p7: mark#(cons(X1,X2)) -> mark#(X1)
p8: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p9: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p10: mark#(isNat(X)) -> a__isNat#(X)
p11: mark#(and(X1,X2)) -> mark#(X1)
p12: mark#(length(X)) -> mark#(X)
p13: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p14: a__U11#(tt(),L) -> mark#(L)
p15: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The estimated dependency graph contains the following SCCs:

  {p1, p13}
  {p6, p7, p11, p12, p15}
  {p2, p3, p4}


-- Reduction pair.

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

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

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = max{x1 - 21, x2 + 97}
          tt_A = 124
          a__length#_A(x1) = max{69, x1 - 28}
          mark_A(x1) = max{128, x1 + 110}
          cons_A(x1,x2) = max{x1 + 99, x2 + 126}
          a__and_A(x1,x2) = max{119, x1 + 10, x2 + 111}
          a__isNatList_A(x1) = max{51, x1 + 50}
          isNat_A(x1) = max{1, x1 - 50}
          a__zeros_A = 127
          |0|_A = 27
          zeros_A = 0
          a__U11_A(x1,x2) = max{x1 + 37, x2 + 143}
          s_A(x1) = x1
          a__length_A(x1) = max{129, x1 + 32}
          a__isNat_A(x1) = max{125, x1 + 59}
          length_A(x1) = max{50, x1 + 32}
          a__isNatIList_A(x1) = max{136, x1 + 135}
          isNatIList_A(x1) = x1 + 26
          nil_A = 129
          U11_A(x1,x2) = max{143, x1 + 37, x2 + 33}
          isNatList_A(x1) = x1 + 49
          and_A(x1,x2) = max{111, x1 + 10, x2 + 110}
    
      precedence:
      
        mark > a__length = length > isNatIList > a__U11 > a__zeros = a__isNat > |0| > a__length# = a__isNatList > cons = s = a__isNatIList = U11 > nil > tt = a__and > a__U11# = zeros = isNatList > and > isNat
      
      partial status:
    
        pi(a__U11#) = [2]
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = []
        pi(cons) = []
        pi(a__and) = []
        pi(a__isNatList) = []
        pi(isNat) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__U11) = [1, 2]
        pi(s) = []
        pi(a__length) = [1]
        pi(a__isNat) = []
        pi(length) = []
        pi(a__isNatIList) = []
        pi(isNatIList) = [1]
        pi(nil) = []
        pi(U11) = [2]
        pi(isNatList) = []
        pi(and) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2) = x2 + 20
          tt_A = 8
          a__length#_A(x1) = 0
          mark_A(x1) = 0
          cons_A(x1,x2) = 0
          a__and_A(x1,x2) = 0
          a__isNatList_A(x1) = 0
          isNat_A(x1) = 0
          a__zeros_A = 0
          |0|_A = 0
          zeros_A = 0
          a__U11_A(x1,x2) = max{0, x1 - 3}
          s_A(x1) = 0
          a__length_A(x1) = 0
          a__isNat_A(x1) = 0
          length_A(x1) = 0
          a__isNatIList_A(x1) = 7
          isNatIList_A(x1) = 6
          nil_A = 9
          U11_A(x1,x2) = 0
          isNatList_A(x1) = 0
          and_A(x1,x2) = x2 + 36
    
      precedence:
      
        isNatList > a__zeros = a__isNatIList > s > zeros > a__U11# = tt = a__length# = mark = cons = a__and = a__isNatList = isNat = |0| = a__U11 = a__length = a__isNat = length = isNatIList = nil = U11 = and
      
      partial status:
    
        pi(a__U11#) = [2]
        pi(tt) = []
        pi(a__length#) = []
        pi(mark) = []
        pi(cons) = []
        pi(a__and) = []
        pi(a__isNatList) = []
        pi(isNat) = []
        pi(a__zeros) = []
        pi(|0|) = []
        pi(zeros) = []
        pi(a__U11) = []
        pi(s) = []
        pi(a__length) = []
        pi(a__isNat) = []
        pi(length) = []
        pi(a__isNatIList) = []
        pi(isNatIList) = []
        pi(nil) = []
        pi(U11) = []
        pi(isNatList) = []
        pi(and) = [2]
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(length(X)) -> mark#(X)
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{4, x1 + 2}
          U11_A(x1,x2) = max{x1, x2}
          length_A(x1) = max{2, x1 + 1}
          and_A(x1,x2) = max{x1, x2}
          cons_A(x1,x2) = max{x1, x2}
          s_A(x1) = max{2, x1}
    
      precedence:
      
        mark# = U11 = length = and = cons = s
      
      partial status:
    
        pi(mark#) = [1]
        pi(U11) = [1, 2]
        pi(length) = [1]
        pi(and) = [1, 2]
        pi(cons) = [1, 2]
        pi(s) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          U11_A(x1,x2) = max{x1, x2}
          length_A(x1) = x1 + 2
          and_A(x1,x2) = max{x1, x2}
          cons_A(x1,x2) = max{x1, x2}
          s_A(x1) = x1
    
      precedence:
      
        mark# = U11 = length = and = cons = s
      
      partial status:
    
        pi(mark#) = [1]
        pi(U11) = [1, 2]
        pi(length) = [1]
        pi(and) = [1, 2]
        pi(cons) = [1, 2]
        pi(s) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5

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(V1,V2)) -> a__isNat#(V1)
p2: a__isNat#(length(V1)) -> a__isNatList#(V1)
p3: a__isNat#(s(V1)) -> a__isNat#(V1)

and R consists of:

r1: a__zeros() -> cons(|0|(),zeros())
r2: a__U11(tt(),L) -> s(a__length(mark(L)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(length(V1)) -> a__isNatList(V1)
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__isNatIList(V) -> a__isNatList(V)
r8: a__isNatIList(zeros()) -> tt()
r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2))
r10: a__isNatList(nil()) -> tt()
r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2))
r12: a__length(nil()) -> |0|()
r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L)
r14: mark(zeros()) -> a__zeros()
r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r16: mark(length(X)) -> a__length(mark(X))
r17: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r18: mark(isNat(X)) -> a__isNat(X)
r19: mark(isNatList(X)) -> a__isNatList(X)
r20: mark(isNatIList(X)) -> a__isNatIList(X)
r21: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r22: mark(|0|()) -> |0|()
r23: mark(tt()) -> tt()
r24: mark(s(X)) -> s(mark(X))
r25: mark(nil()) -> nil()
r26: a__zeros() -> zeros()
r27: a__U11(X1,X2) -> U11(X1,X2)
r28: a__length(X) -> length(X)
r29: a__and(X1,X2) -> and(X1,X2)
r30: a__isNat(X) -> isNat(X)
r31: a__isNatList(X) -> isNatList(X)
r32: a__isNatIList(X) -> isNatIList(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3

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