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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = x2 + 21
        tt_A = 56
        a__length#_A(x1) = max{2, x1 - 43}
        mark_A(x1) = x1 + 64
        cons_A(x1,x2) = max{164, x1 + 70, x2 + 64}
        a__isNatList#_A(x1) = max{22, x1 - 165}
        a__isNat#_A(x1) = max{0, x1 - 95}
        s_A(x1) = max{3, x1}
        length_A(x1) = max{118, x1 + 116}
        a__and#_A(x1,x2) = max{22, x2 - 33}
        a__isNat_A(x1) = max{72, x1 + 25}
        isNatList_A(x1) = max{55, x1 - 68}
        mark#_A(x1) = max{4, x1 - 33}
        isNatIList_A(x1) = max{197, x1 + 65}
        a__isNatIList#_A(x1) = x1 + 32
        isNat_A(x1) = max{71, x1 - 38}
        and_A(x1,x2) = max{x1, x2 + 64}
        a__isNatList_A(x1) = max{119, x1 - 45}
        a__and_A(x1,x2) = max{x1, x2 + 64}
        U11_A(x1,x2) = max{x1, x2 + 117}
        a__zeros_A = 165
        |0|_A = 58
        zeros_A = 101
        a__U11_A(x1,x2) = max{x1, x2 + 180}
        a__length_A(x1) = max{136, x1 + 116}
        a__isNatIList_A(x1) = max{261, x1 + 65}
        nil_A = 102
  
    precedence:
    
      a__isNat > a__U11# = a__length# = mark = cons = a__isNatList# = length = a__and# = mark# = a__isNatList = a__and = a__zeros = |0| = a__length = a__isNatIList = nil > a__isNat# = a__isNatIList# = U11 = a__U11 > s > isNat > tt = isNatList = isNatIList = and = 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#) = []
      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) = []
      pi(a__isNatIList) = []
      pi(nil) = []

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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__isNatList#(L)
p3: a__isNat#(s(V1)) -> a__isNat#(V1)
p4: a__isNat#(length(V1)) -> a__isNatList#(V1)
p5: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p6: a__and#(tt(),X) -> mark#(X)
p7: mark#(s(X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> mark#(X1)
p9: mark#(isNatIList(X)) -> a__isNatIList#(X)
p10: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p11: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p12: a__isNatIList#(V) -> a__isNatList#(V)
p13: mark#(isNatList(X)) -> a__isNatList#(X)
p14: mark#(isNat(X)) -> a__isNat#(X)
p15: mark#(and(X1,X2)) -> mark#(X1)
p16: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p17: mark#(length(X)) -> mark#(X)
p18: mark#(length(X)) -> a__length#(mark(X))
p19: a__length#(cons(N,L)) -> a__and#(a__isNatList(L),isNat(N))
p20: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p21: a__U11#(tt(),L) -> mark#(L)
p22: mark#(U11(X1,X2)) -> mark#(X1)
p23: 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 estimated dependency graph contains the following SCCs:

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


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{x1 - 30, x2 + 43}
        tt_A = 86
        a__length#_A(x1) = max{56, x1 - 5}
        mark_A(x1) = max{57, x1 + 48}
        cons_A(x1,x2) = max{x1, x2 + 55}
        a__and_A(x1,x2) = max{x1, x2 + 48}
        a__isNatList_A(x1) = max{86, x1 + 51}
        isNat_A(x1) = max{38, x1 - 54}
        mark#_A(x1) = max{28, x1 + 4}
        U11_A(x1,x2) = max{x1 + 95, x2 + 104}
        length_A(x1) = max{134, x1 + 97}
        a__and#_A(x1,x2) = max{x1 - 57, x2 + 5}
        and_A(x1,x2) = max{25, x1, x2 + 6}
        a__isNat#_A(x1) = max{1, x1 - 55}
        a__isNatList#_A(x1) = max{41, x1 + 39}
        a__isNat_A(x1) = max{86, x1 - 6}
        isNatList_A(x1) = max{41, x1 + 40}
        s_A(x1) = max{9, x1}
        isNatIList_A(x1) = x1 + 50
        a__isNatIList#_A(x1) = max{47, x1 + 40}
        a__zeros_A = 56
        |0|_A = 55
        zeros_A = 0
        a__U11_A(x1,x2) = max{x1 + 95, x2 + 152}
        a__length_A(x1) = max{181, x1 + 97}
        a__isNatIList_A(x1) = x1 + 97
        nil_A = 87
  
    precedence:
    
      a__U11# = a__length# = mark = cons = a__and = a__isNatList = U11 = length = a__and# = and = a__isNat = s = a__zeros = |0| = a__U11 = a__length > zeros > tt = isNatIList = a__isNatIList > isNat = isNatList > nil > mark# = a__isNat# = a__isNatIList# > a__isNatList#
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = []
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = [1]
      pi(U11) = []
      pi(length) = []
      pi(a__and#) = []
      pi(and) = []
      pi(a__isNat#) = []
      pi(a__isNatList#) = [1]
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(s) = []
      pi(isNatIList) = []
      pi(a__isNatIList#) = [1]
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = [1]
      pi(nil) = []

The next rules are strictly ordered:

  p23

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


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{206, x1 + 8, x2 + 205}
        tt_A = 253
        a__length#_A(x1) = max{68, x1 + 1}
        mark_A(x1) = max{259, x1 + 140}
        cons_A(x1,x2) = max{257, x1 + 85, x2 + 205}
        a__and#_A(x1,x2) = max{x1 - 246, x2 + 140}
        a__isNatList_A(x1) = x1 + 149
        isNat_A(x1) = max{67, x1 - 104}
        mark#_A(x1) = x1 + 7
        s_A(x1) = max{160, x1 + 41}
        isNatIList_A(x1) = x1 + 63
        a__isNatIList#_A(x1) = x1 + 62
        a__isNat#_A(x1) = max{1, x1 - 104}
        length_A(x1) = max{380, x1 + 261}
        a__isNatList#_A(x1) = x1 + 49
        a__isNat_A(x1) = max{253, x1 - 40}
        isNatList_A(x1) = x1 + 65
        and_A(x1,x2) = max{x1 + 7, x2 + 141}
        a__and_A(x1,x2) = max{x1 + 7, x2 + 141}
        U11_A(x1,x2) = max{x1 + 309, x2 + 429}
        a__zeros_A = 258
        |0|_A = 173
        zeros_A = 52
        a__U11_A(x1,x2) = max{x1 + 309, x2 + 466}
        a__length_A(x1) = max{426, x1 + 261}
        a__isNatIList_A(x1) = x1 + 202
        nil_A = 105
  
    precedence:
    
      a__zeros = zeros > mark = cons = a__isNatIList = nil > isNat = a__isNat > isNatIList > tt = a__isNatList = isNatList > a__and > a__U11# = length = a__U11 = a__length > and > a__length# = mark# = s = a__isNat# = a__isNatList# = |0| > a__and# = a__isNatIList# > U11
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = [1]
      pi(mark) = [1]
      pi(cons) = [2]
      pi(a__and#) = [2]
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = [1]
      pi(s) = [1]
      pi(isNatIList) = [1]
      pi(a__isNatIList#) = [1]
      pi(a__isNat#) = []
      pi(length) = []
      pi(a__isNatList#) = [1]
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(and) = []
      pi(a__and) = [2]
      pi(U11) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = [1]
      pi(nil) = []

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))
p2: a__and#(tt(),X) -> mark#(X)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(isNatIList(X)) -> a__isNatIList#(X)
p6: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p7: a__isNat#(s(V1)) -> a__isNat#(V1)
p8: a__isNat#(length(V1)) -> a__isNatList#(V1)
p9: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p10: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p11: a__isNatIList#(V) -> a__isNatList#(V)
p12: mark#(isNatList(X)) -> a__isNatList#(X)
p13: mark#(isNat(X)) -> a__isNat#(X)
p14: mark#(and(X1,X2)) -> mark#(X1)
p15: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p16: mark#(length(X)) -> mark#(X)
p17: mark#(length(X)) -> a__length#(mark(X))
p18: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p19: a__U11#(tt(),L) -> mark#(L)
p20: mark#(U11(X1,X2)) -> mark#(X1)
p21: 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 estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{x1 - 5, x2 + 105}
        tt_A = 7
        a__length#_A(x1) = max{1, x1}
        mark_A(x1) = x1 + 105
        cons_A(x1,x2) = max{140, x1 + 135, x2 + 105}
        a__and_A(x1,x2) = max{x1 + 60, x2 + 115}
        a__isNatList_A(x1) = max{6, x1 - 23}
        isNat_A(x1) = max{25, x1 - 48}
        mark#_A(x1) = max{3, x1 - 1}
        U11_A(x1,x2) = max{x1 + 174, x2 + 212}
        length_A(x1) = max{210, x1 + 107}
        and_A(x1,x2) = max{x1 + 60, x2 + 76}
        a__and#_A(x1,x2) = max{x1 - 82, x2 + 4}
        a__isNat#_A(x1) = max{2, x1 - 106}
        a__isNatList#_A(x1) = max{0, x1 - 130}
        a__isNat_A(x1) = max{56, x1 - 48}
        isNatList_A(x1) = max{2, x1 - 128}
        s_A(x1) = max{106, x1}
        isNatIList_A(x1) = max{135, x1 + 59}
        a__isNatIList#_A(x1) = max{57, x1 + 35}
        a__zeros_A = 191
        |0|_A = 55
        zeros_A = 86
        a__U11_A(x1,x2) = max{314, x1 + 174, x2 + 212}
        a__length_A(x1) = max{314, x1 + 107}
        a__isNatIList_A(x1) = x1 + 163
        nil_A = 56
  
    precedence:
    
      a__isNatIList > mark = isNatList = a__isNatIList# = a__zeros = zeros > length = a__length > tt = a__isNatList = a__isNat = |0| = a__U11 > s > a__isNatList# = nil > U11 > isNatIList > a__U11# = a__length# = cons = a__and = isNat = mark# = and = a__and# = a__isNat#
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = [1, 2]
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = []
      pi(U11) = []
      pi(length) = []
      pi(and) = []
      pi(a__and#) = []
      pi(a__isNat#) = []
      pi(a__isNatList#) = []
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(s) = []
      pi(isNatIList) = []
      pi(a__isNatIList#) = [1]
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = []
      pi(nil) = []

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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> a__length#(mark(X))
p7: mark#(length(X)) -> mark#(X)
p8: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p9: a__and#(tt(),X) -> mark#(X)
p10: mark#(and(X1,X2)) -> mark#(X1)
p11: mark#(isNat(X)) -> a__isNat#(X)
p12: a__isNat#(length(V1)) -> a__isNatList#(V1)
p13: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p14: a__isNat#(s(V1)) -> a__isNat#(V1)
p15: mark#(isNatList(X)) -> a__isNatList#(X)
p16: mark#(isNatIList(X)) -> a__isNatIList#(X)
p17: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))
p18: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p19: mark#(cons(X1,X2)) -> mark#(X1)
p20: 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, p14, p15, p16, p17, p18, p19, p20}


-- 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)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> mark#(X1)
p6: mark#(isNatIList(X)) -> a__isNatIList#(X)
p7: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p8: a__isNat#(s(V1)) -> a__isNat#(V1)
p9: a__isNat#(length(V1)) -> a__isNatList#(V1)
p10: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p11: a__and#(tt(),X) -> mark#(X)
p12: mark#(isNatList(X)) -> a__isNatList#(X)
p13: mark#(isNat(X)) -> a__isNat#(X)
p14: mark#(and(X1,X2)) -> mark#(X1)
p15: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p16: mark#(length(X)) -> mark#(X)
p17: mark#(length(X)) -> a__length#(mark(X))
p18: mark#(U11(X1,X2)) -> mark#(X1)
p19: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p20: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))

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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{100, x1, x2 + 96}
        tt_A = 69
        a__length#_A(x1) = max{100, x1 + 35}
        mark_A(x1) = max{64, x1 + 60}
        cons_A(x1,x2) = max{x1 + 50, x2 + 62}
        a__and_A(x1,x2) = max{x1 + 33, x2 + 86}
        a__isNatList_A(x1) = x1 + 61
        isNat_A(x1) = max{8, x1 - 1}
        mark#_A(x1) = max{70, x1 + 32}
        s_A(x1) = max{1, x1}
        isNatIList_A(x1) = x1 + 109
        a__isNatIList#_A(x1) = x1 + 140
        a__isNat#_A(x1) = x1
        length_A(x1) = max{211, x1 + 146}
        a__isNatList#_A(x1) = x1 + 46
        a__and#_A(x1,x2) = max{x1 - 32, x2 + 71}
        a__isNat_A(x1) = max{68, x1 + 58}
        isNatList_A(x1) = max{36, x1 + 15}
        and_A(x1,x2) = max{x1 + 33, x2 + 71}
        U11_A(x1,x2) = max{152, x1 + 101, x2 + 147}
        a__zeros_A = 63
        |0|_A = 12
        zeros_A = 0
        a__U11_A(x1,x2) = max{211, x1 + 101, x2 + 207}
        a__length_A(x1) = max{211, x1 + 146}
        a__isNatIList_A(x1) = x1 + 169
        nil_A = 8
  
    precedence:
    
      nil > zeros > a__isNatList > mark = a__and = length = a__zeros = a__length = a__isNatIList > isNatIList > s = a__U11 > isNatList > and > a__U11# = a__length# = mark# = a__isNatIList# = a__isNat# = a__isNatList# = a__and# > |0| > tt = cons = isNat = a__isNat = U11
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = [1]
      pi(cons) = [2]
      pi(a__and) = [2]
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = []
      pi(s) = []
      pi(isNatIList) = [1]
      pi(a__isNatIList#) = [1]
      pi(a__isNat#) = []
      pi(length) = []
      pi(a__isNatList#) = [1]
      pi(a__and#) = []
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(and) = [2]
      pi(U11) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = [1]
      pi(a__isNatIList) = []
      pi(nil) = []

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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> mark#(X1)
p6: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1)
p7: a__isNat#(s(V1)) -> a__isNat#(V1)
p8: a__isNat#(length(V1)) -> a__isNatList#(V1)
p9: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p10: a__and#(tt(),X) -> mark#(X)
p11: mark#(isNatList(X)) -> a__isNatList#(X)
p12: mark#(isNat(X)) -> a__isNat#(X)
p13: mark#(and(X1,X2)) -> mark#(X1)
p14: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p15: mark#(length(X)) -> mark#(X)
p16: mark#(length(X)) -> a__length#(mark(X))
p17: mark#(U11(X1,X2)) -> mark#(X1)
p18: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p19: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2))

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, 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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> a__length#(mark(X))
p7: mark#(length(X)) -> mark#(X)
p8: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p9: a__and#(tt(),X) -> mark#(X)
p10: mark#(and(X1,X2)) -> mark#(X1)
p11: mark#(isNat(X)) -> a__isNat#(X)
p12: a__isNat#(length(V1)) -> a__isNatList#(V1)
p13: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p14: a__isNat#(s(V1)) -> a__isNat#(V1)
p15: mark#(isNatList(X)) -> a__isNatList#(X)
p16: mark#(cons(X1,X2)) -> mark#(X1)
p17: 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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{110, x1 - 187, x2 + 97}
        tt_A = 276
        a__length#_A(x1) = max{110, x1 - 189}
        mark_A(x1) = max{299, x1 + 161}
        cons_A(x1,x2) = max{x1 + 86, x2 + 287}
        a__and_A(x1,x2) = max{271, x1 + 23, x2 + 162}
        a__isNatList_A(x1) = max{259, x1 + 66}
        isNat_A(x1) = max{111, x1 - 94}
        mark#_A(x1) = x1 + 96
        U11_A(x1,x2) = max{204, x1 + 17, x2 + 139}
        length_A(x1) = max{111, x1}
        and_A(x1,x2) = max{x1 + 23, x2 + 161}
        a__and#_A(x1,x2) = max{x1 - 259, x2 + 257}
        a__isNat#_A(x1) = max{3, x1 + 2}
        a__isNatList#_A(x1) = x1 + 2
        a__isNat_A(x1) = max{275, x1 + 66}
        isNatList_A(x1) = x1 + 29
        s_A(x1) = max{160, x1}
        a__zeros_A = 298
        |0|_A = 211
        zeros_A = 10
        a__U11_A(x1,x2) = max{299, x1 + 17, x2 + 287}
        a__length_A(x1) = max{299, x1}
        a__isNatIList_A(x1) = max{299, x1 + 260}
        isNatIList_A(x1) = x1 + 99
        nil_A = 300
  
    precedence:
    
      zeros > a__U11# = a__length# > mark = a__and = a__isNatList = a__isNat = isNatList > cons = a__zeros > mark# = and = a__and# = nil > a__length > a__U11 > s > tt = isNat = a__isNat# = |0| = a__isNatIList > isNatIList > length = a__isNatList# > U11
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = []
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = []
      pi(U11) = []
      pi(length) = []
      pi(and) = [2]
      pi(a__and#) = []
      pi(a__isNat#) = []
      pi(a__isNatList#) = [1]
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(s) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = []
      pi(isNatIList) = []
      pi(nil) = []

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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> mark#(X)
p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p8: a__and#(tt(),X) -> mark#(X)
p9: mark#(and(X1,X2)) -> mark#(X1)
p10: mark#(isNat(X)) -> a__isNat#(X)
p11: a__isNat#(length(V1)) -> a__isNatList#(V1)
p12: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p13: a__isNat#(s(V1)) -> a__isNat#(V1)
p14: mark#(isNatList(X)) -> a__isNatList#(X)
p15: mark#(cons(X1,X2)) -> mark#(X1)
p16: 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, p14, p15, p16}


-- 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)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> mark#(X1)
p6: mark#(isNatList(X)) -> a__isNatList#(X)
p7: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p8: a__and#(tt(),X) -> mark#(X)
p9: mark#(isNat(X)) -> a__isNat#(X)
p10: a__isNat#(s(V1)) -> a__isNat#(V1)
p11: a__isNat#(length(V1)) -> a__isNatList#(V1)
p12: mark#(and(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p14: mark#(length(X)) -> mark#(X)
p15: mark#(U11(X1,X2)) -> mark#(X1)
p16: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{199, x1 + 70, x2 + 144}
        tt_A = 21
        a__length#_A(x1) = max{199, x1 + 75}
        mark_A(x1) = max{72, x1 + 44}
        cons_A(x1,x2) = max{x1 + 23, x2 + 70}
        a__and_A(x1,x2) = max{x1, x2 + 73}
        a__isNatList_A(x1) = x1 + 38
        isNat_A(x1) = max{1, x1 - 45}
        mark#_A(x1) = max{198, x1 + 143}
        s_A(x1) = max{196, x1}
        isNatList_A(x1) = max{2, x1 - 6}
        a__isNatList#_A(x1) = x1 + 136
        a__and#_A(x1,x2) = max{x1 - 73, x2 + 199}
        a__isNat_A(x1) = max{22, x1 - 1}
        a__isNat#_A(x1) = max{197, x1 + 12}
        length_A(x1) = max{152, x1 + 124}
        and_A(x1,x2) = max{x1, x2 + 72}
        U11_A(x1,x2) = max{x1 + 115, x2 + 152}
        a__zeros_A = 71
        |0|_A = 20
        zeros_A = 0
        a__U11_A(x1,x2) = max{196, x1 + 115, x2 + 193}
        a__length_A(x1) = max{196, x1 + 124}
        a__isNatIList_A(x1) = max{74, x1 + 39}
        isNatIList_A(x1) = max{31, x1 - 4}
        nil_A = 73
  
    precedence:
    
      tt > a__U11# = a__length# = mark# = nil > isNatList = isNatIList > mark > a__and = a__isNatList = isNat > a__isNat# = and > a__and# > a__isNatList# > cons = s = a__isNat = length = U11 = a__zeros = |0| = zeros = a__U11 = a__length = a__isNatIList
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = []
      pi(a__and) = [2]
      pi(a__isNatList) = [1]
      pi(isNat) = []
      pi(mark#) = []
      pi(s) = []
      pi(isNatList) = []
      pi(a__isNatList#) = []
      pi(a__and#) = []
      pi(a__isNat) = []
      pi(a__isNat#) = []
      pi(length) = [1]
      pi(and) = []
      pi(U11) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = [1]
      pi(a__isNatIList) = []
      pi(isNatIList) = []
      pi(nil) = []

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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(isNatList(X)) -> a__isNatList#(X)
p6: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(isNat(X)) -> a__isNat#(X)
p9: a__isNat#(s(V1)) -> a__isNat#(V1)
p10: a__isNat#(length(V1)) -> a__isNatList#(V1)
p11: mark#(and(X1,X2)) -> mark#(X1)
p12: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p13: mark#(length(X)) -> mark#(X)
p14: mark#(U11(X1,X2)) -> mark#(X1)
p15: 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 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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> mark#(X)
p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p8: a__and#(tt(),X) -> mark#(X)
p9: mark#(and(X1,X2)) -> mark#(X1)
p10: mark#(isNat(X)) -> a__isNat#(X)
p11: a__isNat#(length(V1)) -> a__isNatList#(V1)
p12: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p13: a__isNat#(s(V1)) -> a__isNat#(V1)
p14: mark#(isNatList(X)) -> a__isNatList#(X)
p15: 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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{29, x1 - 127, x2 + 9}
        tt_A = 149
        a__length#_A(x1) = max{29, x1 - 120}
        mark_A(x1) = max{149, x1 + 75}
        cons_A(x1,x2) = max{147, x2 + 143}
        a__and_A(x1,x2) = max{149, x1, x2 + 90}
        a__isNatList_A(x1) = 149
        isNat_A(x1) = 17
        mark#_A(x1) = max{8, x1 - 7}
        U11_A(x1,x2) = max{113, x1 + 39, x2 + 37}
        length_A(x1) = max{188, x1}
        and_A(x1,x2) = max{x1, x2 + 15}
        a__and#_A(x1,x2) = max{7, x1 - 141, x2 - 1}
        a__isNat#_A(x1) = 9
        a__isNatList#_A(x1) = 8
        a__isNat_A(x1) = 149
        isNatList_A(x1) = 8
        s_A(x1) = max{74, x1}
        a__zeros_A = 148
        |0|_A = 150
        zeros_A = 0
        a__U11_A(x1,x2) = max{113, x1 + 39, x2 + 76}
        a__length_A(x1) = max{188, x1}
        a__isNatIList_A(x1) = x1 + 219
        isNatIList_A(x1) = x1 + 144
        nil_A = 151
  
    precedence:
    
      |0| = zeros = nil > a__U11# = a__length# = mark = a__and = a__isNatList = isNat = U11 = a__isNat# = a__isNat = s = a__U11 = a__length = a__isNatIList = isNatIList > tt > mark# = a__and# = a__isNatList# = isNatList > cons = length = and = a__zeros
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = []
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = []
      pi(U11) = []
      pi(length) = []
      pi(and) = []
      pi(a__and#) = []
      pi(a__isNat#) = []
      pi(a__isNatList#) = []
      pi(a__isNat) = []
      pi(isNatList) = []
      pi(s) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = []
      pi(isNatIList) = []
      pi(nil) = []

The next rules are strictly ordered:

  p10

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__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(length(X)) -> mark#(X)
p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p8: a__and#(tt(),X) -> mark#(X)
p9: mark#(and(X1,X2)) -> mark#(X1)
p10: a__isNat#(length(V1)) -> a__isNatList#(V1)
p11: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p12: a__isNat#(s(V1)) -> a__isNat#(V1)
p13: mark#(isNatList(X)) -> a__isNatList#(X)
p14: 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:

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


-- Reduction pair.

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

p1: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__isNat#_A(x1) = x1 + 2
        s_A(x1) = x1 + 2
  
    precedence:
    
      a__isNat# = s
    
    partial status:
  
      pi(a__isNat#) = [1]
      pi(s) = [1]

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(isNatList(X)) -> a__isNatList#(X)
p6: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(and(X1,X2)) -> mark#(X1)
p9: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p10: mark#(length(X)) -> mark#(X)
p11: mark#(U11(X1,X2)) -> mark#(X1)
p12: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{x1 - 21, x2 + 5}
        tt_A = 27
        a__length#_A(x1) = max{6, x1 + 5}
        mark_A(x1) = x1
        cons_A(x1,x2) = max{32, x1 + 29, x2}
        a__and_A(x1,x2) = max{x1 + 23, x2}
        a__isNatList_A(x1) = max{26, x1 - 17}
        isNat_A(x1) = max{2, x1 - 12}
        mark#_A(x1) = max{4, x1 + 2}
        s_A(x1) = max{2, x1}
        isNatList_A(x1) = max{26, x1 - 17}
        a__isNatList#_A(x1) = max{28, x1 - 15}
        a__and#_A(x1,x2) = max{25, x1 + 24, x2 + 2}
        a__isNat_A(x1) = max{2, x1 - 12}
        and_A(x1,x2) = max{x1 + 23, x2}
        length_A(x1) = max{51, x1 + 20}
        U11_A(x1,x2) = max{52, x1 + 3, x2 + 20}
        a__zeros_A = 70
        |0|_A = 40
        zeros_A = 70
        a__U11_A(x1,x2) = max{52, x1 + 3, x2 + 20}
        a__length_A(x1) = max{51, x1 + 20}
        a__isNatIList_A(x1) = max{28, x1 - 16}
        isNatIList_A(x1) = max{28, x1 - 16}
        nil_A = 45
  
    precedence:
    
      a__U11# = a__length# > mark# = a__isNatList# = a__and# > mark = cons = a__and = a__isNatList = a__isNat = and = a__zeros = a__isNatIList = isNatIList > tt > isNat = s = isNatList = U11 = |0| = zeros = a__U11 = a__length > length = nil
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = []
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = []
      pi(s) = []
      pi(isNatList) = []
      pi(a__isNatList#) = []
      pi(a__and#) = []
      pi(a__isNat) = []
      pi(and) = []
      pi(length) = [1]
      pi(U11) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = []
      pi(isNatIList) = []
      pi(nil) = []

The next rules are strictly ordered:

  p10

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__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(isNatList(X)) -> a__isNatList#(X)
p6: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(and(X1,X2)) -> mark#(X1)
p9: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p10: mark#(U11(X1,X2)) -> mark#(X1)
p11: 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 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__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p5: mark#(U11(X1,X2)) -> mark#(X1)
p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(and(X1,X2)) -> mark#(X1)
p9: mark#(isNatList(X)) -> a__isNatList#(X)
p10: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p11: 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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{215, x1 - 20, x2 + 178}
        tt_A = 133
        a__length#_A(x1) = max{215, x1 + 85}
        mark_A(x1) = max{129, x1 + 92}
        cons_A(x1,x2) = max{127, x1 + 90, x2 + 124}
        a__and_A(x1,x2) = max{x1 + 79, x2 + 125}
        a__isNatList_A(x1) = max{130, x1 + 122}
        isNat_A(x1) = x1 + 41
        mark#_A(x1) = max{114, x1 + 79}
        U11_A(x1,x2) = max{x1 + 216, x2 + 416}
        and_A(x1,x2) = max{x1 + 79, x2 + 116}
        a__and#_A(x1,x2) = max{x1 - 14, x2 + 116}
        isNatList_A(x1) = max{123, x1 + 121}
        a__isNatList#_A(x1) = max{119, x1 + 116}
        a__isNat_A(x1) = max{132, x1 + 97}
        s_A(x1) = max{425, x1}
        a__zeros_A = 128
        |0|_A = 37
        zeros_A = 3
        a__U11_A(x1,x2) = max{425, x1 + 216, x2 + 416}
        a__length_A(x1) = max{425, x1 + 293}
        a__isNatIList_A(x1) = x1 + 131
        isNatIList_A(x1) = x1 + 124
        nil_A = 130
        length_A(x1) = max{423, x1 + 293}
  
    precedence:
    
      tt = mark = a__and = a__isNatList = isNat = U11 = and = isNatList = a__isNat = s = a__zeros = |0| = zeros = a__U11 = a__length > a__U11# = a__length# > cons > mark# = a__isNatList# = a__isNatIList > a__and# = isNatIList > nil = length
    
    partial status:
  
      pi(a__U11#) = []
      pi(tt) = []
      pi(a__length#) = []
      pi(mark) = []
      pi(cons) = [2]
      pi(a__and) = []
      pi(a__isNatList) = []
      pi(isNat) = []
      pi(mark#) = [1]
      pi(U11) = []
      pi(and) = []
      pi(a__and#) = []
      pi(isNatList) = []
      pi(a__isNatList#) = []
      pi(a__isNat) = []
      pi(s) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__isNatIList) = [1]
      pi(isNatIList) = []
      pi(nil) = []
      pi(length) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: a__U11#(tt(),L) -> a__length#(mark(L))
p2: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L)
p3: a__U11#(tt(),L) -> mark#(L)
p4: mark#(U11(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p6: a__and#(tt(),X) -> mark#(X)
p7: mark#(and(X1,X2)) -> mark#(X1)
p8: mark#(isNatList(X)) -> a__isNatList#(X)
p9: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p10: 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}
  {p4, p5, p6, p7, p8, p9, p10}


-- 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        a__U11#_A(x1,x2) = max{x1 + 4, x2 + 30}
        tt_A = 41
        a__length#_A(x1) = x1 + 4
        mark_A(x1) = max{41, x1}
        cons_A(x1,x2) = max{39, x1, x2 + 31}
        a__and_A(x1,x2) = max{32, x1, x2}
        a__isNatList_A(x1) = max{34, x1 + 11}
        isNat_A(x1) = max{0, x1 - 5}
        a__zeros_A = 40
        |0|_A = 39
        zeros_A = 8
        a__U11_A(x1,x2) = max{58, x2 + 30}
        s_A(x1) = max{31, x1}
        a__length_A(x1) = max{58, x1 + 16}
        a__isNat_A(x1) = max{41, x1 - 5}
        length_A(x1) = max{58, x1 + 16}
        a__isNatIList_A(x1) = x1 + 41
        isNatIList_A(x1) = x1 + 41
        nil_A = 42
        U11_A(x1,x2) = max{58, x2 + 30}
        isNatList_A(x1) = x1 + 11
        and_A(x1,x2) = max{x1, x2}
  
    precedence:
    
      a__zeros > a__length = length > a__isNatIList = isNatIList > a__U11 = U11 > tt = mark = a__and = a__isNatList = zeros = s = a__isNat > cons > a__U11# > a__length# > |0| > nil > isNat = and > isNatList
    
    partial status:
  
      pi(a__U11#) = [1]
      pi(tt) = []
      pi(a__length#) = [1]
      pi(mark) = [1]
      pi(cons) = []
      pi(a__and) = [2]
      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:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: 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 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#(s(X)) -> mark#(X)
p3: mark#(isNatList(X)) -> a__isNatList#(X)
p4: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(and(X1,X2)) -> mark#(X1)
p7: mark#(and(X1,X2)) -> a__and#(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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = x1 + 5
        U11_A(x1,x2) = max{x1 + 93, x2 + 138}
        s_A(x1) = max{106, x1 + 5}
        isNatList_A(x1) = max{5, x1}
        a__isNatList#_A(x1) = max{4, x1}
        cons_A(x1,x2) = max{101, x1 + 57, x2 + 64}
        a__and#_A(x1,x2) = max{x1 - 88, x2 + 64}
        a__isNat_A(x1) = max{91, x1 - 59}
        tt_A = 90
        and_A(x1,x2) = max{66, x1 + 21, x2 + 64}
        mark_A(x1) = max{102, x1 + 58}
        a__zeros_A = 102
        |0|_A = 44
        zeros_A = 37
        a__U11_A(x1,x2) = max{x1 + 93, x2 + 139}
        a__length_A(x1) = max{131, x1 + 76}
        a__and_A(x1,x2) = max{x1 + 21, x2 + 67}
        a__isNatIList_A(x1) = max{113, x1 + 67}
        a__isNatList_A(x1) = max{18, x1 + 16}
        isNatIList_A(x1) = x1 + 56
        nil_A = 103
        isNat_A(x1) = max{1, x1 - 59}
        length_A(x1) = max{121, x1 + 76}
  
    precedence:
    
      isNatIList = nil > U11 = s = isNatList = cons = a__isNat = mark = a__zeros = |0| = zeros = a__U11 = a__length = a__and = a__isNatIList = a__isNatList > a__isNatList# = a__and# = tt = and > mark# > isNat = length
    
    partial status:
  
      pi(mark#) = [1]
      pi(U11) = []
      pi(s) = []
      pi(isNatList) = [1]
      pi(a__isNatList#) = [1]
      pi(cons) = []
      pi(a__and#) = []
      pi(a__isNat) = []
      pi(tt) = []
      pi(and) = []
      pi(mark) = []
      pi(a__zeros) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__and) = []
      pi(a__isNatIList) = [1]
      pi(a__isNatList) = []
      pi(isNatIList) = [1]
      pi(nil) = []
      pi(isNat) = []
      pi(length) = [1]

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2))
p4: a__and#(tt(),X) -> mark#(X)
p5: mark#(and(X1,X2)) -> mark#(X1)
p6: mark#(and(X1,X2)) -> a__and#(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 estimated dependency graph contains the following SCCs:

  {p1, p2, p4, p5, p6}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p3: a__and#(tt(),X) -> mark#(X)
p4: mark#(and(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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = max{96, x1 + 2}
        U11_A(x1,x2) = max{96, x1 + 14, x2 + 65}
        and_A(x1,x2) = max{51, x1 + 1, x2 + 4}
        a__and#_A(x1,x2) = max{96, x1 - 12, x2 + 3}
        mark_A(x1) = max{52, x1 + 15}
        tt_A = 45
        s_A(x1) = max{97, x1}
        a__zeros_A = 51
        cons_A(x1,x2) = max{x1 - 1, x2 + 35}
        |0|_A = 50
        zeros_A = 0
        a__U11_A(x1,x2) = max{110, x1 + 14, x2 + 80}
        a__length_A(x1) = max{110, x1 + 57}
        a__and_A(x1,x2) = max{52, x1 + 1, x2 + 19}
        a__isNat_A(x1) = max{2, x1 - 4}
        length_A(x1) = max{96, x1 + 57}
        a__isNatList_A(x1) = max{52, x1 - 1}
        a__isNatIList_A(x1) = max{56, x1 + 54}
        isNatIList_A(x1) = max{42, x1 + 40}
        nil_A = 53
        isNatList_A(x1) = max{0, x1 - 2}
        isNat_A(x1) = max{1, x1 - 14}
  
    precedence:
    
      mark = s = a__zeros = cons = zeros = a__U11 = a__length = a__and = a__isNat = length = a__isNatList = a__isNatIList = nil = isNat > U11 > mark# = a__and# = tt > and > |0| = isNatIList = isNatList
    
    partial status:
  
      pi(mark#) = [1]
      pi(U11) = []
      pi(and) = []
      pi(a__and#) = [2]
      pi(mark) = []
      pi(tt) = []
      pi(s) = []
      pi(a__zeros) = []
      pi(cons) = []
      pi(|0|) = []
      pi(zeros) = []
      pi(a__U11) = []
      pi(a__length) = []
      pi(a__and) = []
      pi(a__isNat) = []
      pi(length) = []
      pi(a__isNatList) = []
      pi(a__isNatIList) = []
      pi(isNatIList) = [1]
      pi(nil) = []
      pi(isNatList) = []
      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: mark#(U11(X1,X2)) -> mark#(X1)
p2: a__and#(tt(),X) -> mark#(X)
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: 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, p3, p4}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(and(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 set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = max{3, x1 + 2}
        U11_A(x1,x2) = max{x1, x2 + 1}
        s_A(x1) = x1 + 2
        and_A(x1,x2) = max{x1 + 1, x2 + 1}
  
    precedence:
    
      mark# = U11 = s = and
    
    partial status:
  
      pi(mark#) = []
      pi(U11) = [2]
      pi(s) = [1]
      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: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(and(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, p2}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> mark#(X1)
p2: mark#(and(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 set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = x1 + 3
        U11_A(x1,x2) = max{x1, x2}
        and_A(x1,x2) = max{x1, x2 + 1}
  
    precedence:
    
      mark# = U11 = and
    
    partial status:
  
      pi(mark#) = [1]
      pi(U11) = [1, 2]
      pi(and) = [1, 2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(and(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}


-- Reduction pair.

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

p1: mark#(and(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 set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = x1 + 2
        and_A(x1,x2) = max{x1 + 1, x2 + 1}
  
    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.