YES

TRS:

  a__zeros() -> cons(0(),zeros())
  a__U11(tt(),V1) -> a__U12(a__isNatList(V1))
  a__U12(tt()) -> tt()
  a__U21(tt(),V1) -> a__U22(a__isNat(V1))
  a__U22(tt()) -> tt()
  a__U31(tt(),V) -> a__U32(a__isNatList(V))
  a__U32(tt()) -> tt()
  a__U41(tt(),V1,V2) -> a__U42(a__isNat(V1),V2)
  a__U42(tt(),V2) -> a__U43(a__isNatIList(V2))
  a__U43(tt()) -> tt()
  a__U51(tt(),V1,V2) -> a__U52(a__isNat(V1),V2)
  a__U52(tt(),V2) -> a__U53(a__isNatList(V2))
  a__U53(tt()) -> tt()
  a__U61(tt(),L) -> s(a__length(mark(L)))
  a__and(tt(),X) -> mark(X)
  a__isNat(0()) -> tt()
  a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1),V1)
  a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1)
  a__isNatIList(V) -> a__U31(a__isNatIListKind(V),V)
  a__isNatIList(zeros()) -> tt()
  a__isNatIList(cons(V1,V2)) -> a__U41(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)
  a__isNatIListKind(nil()) -> tt()
  a__isNatIListKind(zeros()) -> tt()
  a__isNatIListKind(cons(V1,V2)) -> a__and(a__isNatKind(V1),isNatIListKind(V2))
  a__isNatKind(0()) -> tt()
  a__isNatKind(length(V1)) -> a__isNatIListKind(V1)
  a__isNatKind(s(V1)) -> a__isNatKind(V1)
  a__isNatList(nil()) -> tt()
  a__isNatList(cons(V1,V2)) -> a__U51(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)
  a__length(nil()) -> 0()
  a__length(cons(N,L)) -> a__U61(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)
  mark(zeros()) -> a__zeros()
  mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
  mark(U12(X)) -> a__U12(mark(X))
  mark(isNatList(X)) -> a__isNatList(X)
  mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
  mark(U22(X)) -> a__U22(mark(X))
  mark(isNat(X)) -> a__isNat(X)
  mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
  mark(U32(X)) -> a__U32(mark(X))
  mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
  mark(U42(X1,X2)) -> a__U42(mark(X1),X2)
  mark(U43(X)) -> a__U43(mark(X))
  mark(isNatIList(X)) -> a__isNatIList(X)
  mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
  mark(U52(X1,X2)) -> a__U52(mark(X1),X2)
  mark(U53(X)) -> a__U53(mark(X))
  mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
  mark(length(X)) -> a__length(mark(X))
  mark(and(X1,X2)) -> a__and(mark(X1),X2)
  mark(isNatIListKind(X)) -> a__isNatIListKind(X)
  mark(isNatKind(X)) -> a__isNatKind(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__U12(X) -> U12(X)
  a__isNatList(X) -> isNatList(X)
  a__U21(X1,X2) -> U21(X1,X2)
  a__U22(X) -> U22(X)
  a__isNat(X) -> isNat(X)
  a__U31(X1,X2) -> U31(X1,X2)
  a__U32(X) -> U32(X)
  a__U41(X1,X2,X3) -> U41(X1,X2,X3)
  a__U42(X1,X2) -> U42(X1,X2)
  a__U43(X) -> U43(X)
  a__isNatIList(X) -> isNatIList(X)
  a__U51(X1,X2,X3) -> U51(X1,X2,X3)
  a__U52(X1,X2) -> U52(X1,X2)
  a__U53(X) -> U53(X)
  a__U61(X1,X2) -> U61(X1,X2)
  a__length(X) -> length(X)
  a__and(X1,X2) -> and(X1,X2)
  a__isNatIListKind(X) -> isNatIListKind(X)
  a__isNatKind(X) -> isNatKind(X)

max/plus interpretations on N:

  a__zeros_A = 751
  a__zeros#_A = 754
  cons_A(x1,x2) = max{567, 464 + x1, 709 + x2}
  cons#_A(x1,x2) = max{739, 1 + x1, 753}
  0_A = 1
  0#_A = 632
  zeros_A = 42
  zeros#_A = 753
  a__U11_A(x1,x2) = max{752, 1 + x1, 758 + x2}
  a__U11#_A(x1,x2) = max{738, 172, 174 + x2}
  tt_A = 751
  tt#_A = 633
  a__U12_A(x1) = max{490, 245 + x1}
  a__U12#_A(x1) = max{171, 169}
  a__isNatList_A(x1) = max{513, 508 + x1}
  a__isNatList#_A(x1) = max{638, 173 + x1}
  a__U21_A(x1,x2) = max{752, x1, 268 + x2}
  a__U21#_A(x1,x2) = max{743, 730, 738}
  a__U22_A(x1) = max{752, 1 + x1}
  a__U22#_A(x1) = max{739, 630}
  a__isNat_A(x1) = max{751, 267 + x1}
  a__isNat#_A(x1) = max{635, 737}
  a__U31_A(x1,x2) = max{710, x1, 509 + x2}
  a__U31#_A(x1,x2) = max{639, 176, 174 + x2}
  a__U32_A(x1) = max{750, 1 + x1}
  a__U32#_A(x1) = max{632, 173}
  a__U41_A(x1,x2,x3) = max{1583, 831 + x1, 771 + x2, 1277 + x3}
  a__U41#_A(x1,x2,x3) = max{752, 750, 645, 738 + x3}
  a__U42_A(x1,x2) = max{1583, 21 + x1, 752 + x2}
  a__U42#_A(x1,x2) = max{751, 751, 182 + x2}
  a__U43_A(x1) = max{753, x1}
  a__U43#_A(x1) = max{181, 180}
  a__isNatIList_A(x1) = max{1583, 709 + x1}
  a__isNatIList#_A(x1) = max{644, 182 + x1}
  a__U51_A(x1,x2,x3) = max{997, 5 + x1, 513 + x2, 510 + x3}
  a__U51#_A(x1,x2,x3) = max{636, -13 + x1, 736, 733 + x3}
  a__U52_A(x1,x2) = max{509, 246 + x1, 510 + x2}
  a__U52#_A(x1,x2) = max{637, 630, 639 + x2}
  a__U53_A(x1) = max{750, 1 + x1}
  a__U53#_A(x1) = max{0, -2}
  a__U61_A(x1,x2) = max{1243, 508 + x1, 1200 + x2}
  a__U61#_A(x1,x2) = max{1279, 731 + x1, 1236 + x2}
  s_A(x1) = max{1244, 1 + x1}
  s#_A(x1) = max{742, 1237}
  a__length_A(x1) = max{1243, 491 + x1}
  a__length#_A(x1) = max{1465, 713 + x1}
  mark_A(x1) = max{751, 506 + x1}
  mark#_A(x1) = max{631, 729 + x1}
  a__and_A(x1,x2) = max{445, x1, 509 + x2}
  a__and#_A(x1,x2) = max{184, 754, 737 + x2}
  length_A(x1) = max{737, 491 + x1}
  length#_A(x1) = max{739, 174 + x1}
  a__isNatIListKind_A(x1) = max{751, -123 + x1}
  a__isNatIListKind#_A(x1) = max{183, 46 + x1}
  a__isNatKind_A(x1) = max{751, 13 + x1}
  a__isNatKind#_A(x1) = max{741, 634}
  isNatIListKind_A(x1) = max{0, -123 + x1}
  isNatIListKind#_A(x1) = max{0, 0}
  nil_A = 243
  nil#_A = 634
  and_A(x1,x2) = max{224, x1, 26 + x2}
  and#_A(x1,x2) = max{738, 738, 0}
  isNat_A(x1) = max{184, -95 + x1}
  isNat#_A(x1) = max{737, 0}
  isNatKind_A(x1) = max{13, -493 + x1}
  isNatKind#_A(x1) = max{633, 740}
  U11_A(x1,x2) = max{0, 1 + x1, 252 + x2}
  U11#_A(x1,x2) = max{174, 173, 171}
  U12_A(x1) = max{490, 245 + x1}
  U12#_A(x1) = max{170, 170}
  isNatList_A(x1) = max{0, 2 + x1}
  isNatList#_A(x1) = max{0, 172}
  U21_A(x1,x2) = max{269, x1, -1 + x2}
  U21#_A(x1,x2) = max{739, 731, 743}
  U22_A(x1) = max{246, 1 + x1}
  U22#_A(x1) = max{0, 729}
  U31_A(x1,x2) = max{3, x1, 203 + x2}
  U31#_A(x1,x2) = max{175, 173, 173}
  U32_A(x1) = max{246, 1 + x1}
  U32#_A(x1) = max{632, 630}
  U41_A(x1,x2,x3) = max{24, 831 + x1, 771 + x2, 1277 + x3}
  U41#_A(x1,x2,x3) = max{751, 630, 752, 751}
  U42_A(x1,x2) = max{1077, 21 + x1, 265 + x2}
  U42#_A(x1,x2) = max{0, 181, 181}
  U43_A(x1) = max{247, x1}
  U43#_A(x1) = max{181, 181}
  isNatIList_A(x1) = max{1077, 203 + x1}
  isNatIList#_A(x1) = max{0, 181}
  U51_A(x1,x2,x3) = max{6, 5 + x1, 491 + x2, 4 + x3}
  U51#_A(x1,x2,x3) = max{493, -14, -14, 493}
  U52_A(x1,x2) = max{510, 246 + x1, 245 + x2}
  U52#_A(x1,x2) = max{636, 629, 630}
  U53_A(x1) = max{246, 1 + x1}
  U53#_A(x1) = max{0, -1}
  U61_A(x1,x2) = max{0, 508 + x1, 754 + x2}
  U61#_A(x1,x2) = max{1235, 729 + x1, 730}

precedence:

  a__zeros > 0 > cons = tt > zeros = a__isNatKind > a__isNatIListKind = isNatKind = U52 > a__U52 = a__and = U51 = U61 > mark > a__U21 = a__U42 = a__U53 = nil > a__U22 = a__U43 = a__isNatIList = U21 = U42 = U53 > a__U31 = a__U41 = U22 = U43 = isNatIList > a__isNat = a__U32 = U31 = U41 > isNat = U32 > a__length > a__U61 = length = and > a__U11 = s = isNatList > a__U12 = a__isNatList = U11 > a__U51 = isNatIListKind = U12