YES

Problem:
 a__nats() -> a__adx(a__zeros())
 a__zeros() -> cons(0(),zeros())
 a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
 a__hd(cons(X,Y)) -> mark(X)
 a__tl(cons(X,Y)) -> mark(Y)
 mark(nats()) -> a__nats()
 mark(adx(X)) -> a__adx(mark(X))
 mark(zeros()) -> a__zeros()
 mark(incr(X)) -> a__incr(mark(X))
 mark(hd(X)) -> a__hd(mark(X))
 mark(tl(X)) -> a__tl(mark(X))
 mark(cons(X1,X2)) -> cons(X1,X2)
 mark(0()) -> 0()
 mark(s(X)) -> s(X)
 a__nats() -> nats()
 a__adx(X) -> adx(X)
 a__zeros() -> zeros()
 a__incr(X) -> incr(X)
 a__hd(X) -> hd(X)
 a__tl(X) -> tl(X)

Proof:
 DP Processor:
  DPs:
   a__nats#() -> a__zeros#()
   a__nats#() -> a__adx#(a__zeros())
   a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
   a__hd#(cons(X,Y)) -> mark#(X)
   a__tl#(cons(X,Y)) -> mark#(Y)
   mark#(nats()) -> a__nats#()
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> a__adx#(mark(X))
   mark#(zeros()) -> a__zeros#()
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> a__incr#(mark(X))
   mark#(hd(X)) -> mark#(X)
   mark#(hd(X)) -> a__hd#(mark(X))
   mark#(tl(X)) -> mark#(X)
   mark#(tl(X)) -> a__tl#(mark(X))
  TRS:
   a__nats() -> a__adx(a__zeros())
   a__zeros() -> cons(0(),zeros())
   a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
   a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
   a__hd(cons(X,Y)) -> mark(X)
   a__tl(cons(X,Y)) -> mark(Y)
   mark(nats()) -> a__nats()
   mark(adx(X)) -> a__adx(mark(X))
   mark(zeros()) -> a__zeros()
   mark(incr(X)) -> a__incr(mark(X))
   mark(hd(X)) -> a__hd(mark(X))
   mark(tl(X)) -> a__tl(mark(X))
   mark(cons(X1,X2)) -> cons(X1,X2)
   mark(0()) -> 0()
   mark(s(X)) -> s(X)
   a__nats() -> nats()
   a__adx(X) -> adx(X)
   a__zeros() -> zeros()
   a__incr(X) -> incr(X)
   a__hd(X) -> hd(X)
   a__tl(X) -> tl(X)
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    a__nats() -> a__adx(a__zeros())
    a__zeros() -> cons(0(),zeros())
    a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
    a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
    a__hd(cons(X,Y)) -> mark(X)
    a__tl(cons(X,Y)) -> mark(Y)
    mark(nats()) -> a__nats()
    mark(adx(X)) -> a__adx(mark(X))
    mark(zeros()) -> a__zeros()
    mark(incr(X)) -> a__incr(mark(X))
    mark(hd(X)) -> a__hd(mark(X))
    mark(tl(X)) -> a__tl(mark(X))
    mark(cons(X1,X2)) -> cons(X1,X2)
    mark(0()) -> 0()
    mark(s(X)) -> s(X)
    a__nats() -> nats()
    a__adx(X) -> adx(X)
    a__zeros() -> zeros()
    a__incr(X) -> incr(X)
    a__hd(X) -> hd(X)
    a__tl(X) -> tl(X)
   interpretation:
    [a__tl#](x0) = x0 + 5,
    
    [mark#](x0) = x0 + 4,
    
    [a__hd#](x0) = x0 + 4,
    
    [a__incr#](x0) = 0,
    
    [a__adx#](x0) = 2,
    
    [a__zeros#] = 0,
    
    [a__nats#] = 6,
    
    [tl](x0) = 2x0 + 3,
    
    [hd](x0) = 4x0 + 4,
    
    [nats] = 4,
    
    [a__tl](x0) = 2x0 + 5,
    
    [mark](x0) = 2x0 + 1,
    
    [a__hd](x0) = 4x0 + 5,
    
    [adx](x0) = 2x0 + 1,
    
    [incr](x0) = x0 + 1,
    
    [s](x0) = 0,
    
    [a__incr](x0) = x0 + 1,
    
    [cons](x0, x1) = 4x0 + x1 + 2,
    
    [zeros] = 1,
    
    [0] = 0,
    
    [a__adx](x0) = 2x0 + 1,
    
    [a__zeros] = 3,
    
    [a__nats] = 7
   orientation:
    a__nats#() = 6 >= 0 = a__zeros#()
    
    a__nats#() = 6 >= 2 = a__adx#(a__zeros())
    
    a__adx#(cons(X,Y)) = 2 >= 0 = a__incr#(cons(X,adx(Y)))
    
    a__hd#(cons(X,Y)) = 4X + Y + 6 >= X + 4 = mark#(X)
    
    a__tl#(cons(X,Y)) = 4X + Y + 7 >= Y + 4 = mark#(Y)
    
    mark#(nats()) = 8 >= 6 = a__nats#()
    
    mark#(adx(X)) = 2X + 5 >= X + 4 = mark#(X)
    
    mark#(adx(X)) = 2X + 5 >= 2 = a__adx#(mark(X))
    
    mark#(zeros()) = 5 >= 0 = a__zeros#()
    
    mark#(incr(X)) = X + 5 >= X + 4 = mark#(X)
    
    mark#(incr(X)) = X + 5 >= 0 = a__incr#(mark(X))
    
    mark#(hd(X)) = 4X + 8 >= X + 4 = mark#(X)
    
    mark#(hd(X)) = 4X + 8 >= 2X + 5 = a__hd#(mark(X))
    
    mark#(tl(X)) = 2X + 7 >= X + 4 = mark#(X)
    
    mark#(tl(X)) = 2X + 7 >= 2X + 6 = a__tl#(mark(X))
    
    a__nats() = 7 >= 7 = a__adx(a__zeros())
    
    a__zeros() = 3 >= 3 = cons(0(),zeros())
    
    a__incr(cons(X,Y)) = 4X + Y + 3 >= Y + 3 = cons(s(X),incr(Y))
    
    a__adx(cons(X,Y)) = 8X + 2Y + 5 >= 4X + 2Y + 4 = a__incr(cons(X,adx(Y)))
    
    a__hd(cons(X,Y)) = 16X + 4Y + 13 >= 2X + 1 = mark(X)
    
    a__tl(cons(X,Y)) = 8X + 2Y + 9 >= 2Y + 1 = mark(Y)
    
    mark(nats()) = 9 >= 7 = a__nats()
    
    mark(adx(X)) = 4X + 3 >= 4X + 3 = a__adx(mark(X))
    
    mark(zeros()) = 3 >= 3 = a__zeros()
    
    mark(incr(X)) = 2X + 3 >= 2X + 2 = a__incr(mark(X))
    
    mark(hd(X)) = 8X + 9 >= 8X + 9 = a__hd(mark(X))
    
    mark(tl(X)) = 4X + 7 >= 4X + 7 = a__tl(mark(X))
    
    mark(cons(X1,X2)) = 8X1 + 2X2 + 5 >= 4X1 + X2 + 2 = cons(X1,X2)
    
    mark(0()) = 1 >= 0 = 0()
    
    mark(s(X)) = 1 >= 0 = s(X)
    
    a__nats() = 7 >= 4 = nats()
    
    a__adx(X) = 2X + 1 >= 2X + 1 = adx(X)
    
    a__zeros() = 3 >= 1 = zeros()
    
    a__incr(X) = X + 1 >= X + 1 = incr(X)
    
    a__hd(X) = 4X + 5 >= 4X + 4 = hd(X)
    
    a__tl(X) = 2X + 5 >= 2X + 3 = tl(X)
   problem:
    DPs:
     
    TRS:
     a__nats() -> a__adx(a__zeros())
     a__zeros() -> cons(0(),zeros())
     a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
     a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
     a__hd(cons(X,Y)) -> mark(X)
     a__tl(cons(X,Y)) -> mark(Y)
     mark(nats()) -> a__nats()
     mark(adx(X)) -> a__adx(mark(X))
     mark(zeros()) -> a__zeros()
     mark(incr(X)) -> a__incr(mark(X))
     mark(hd(X)) -> a__hd(mark(X))
     mark(tl(X)) -> a__tl(mark(X))
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(0()) -> 0()
     mark(s(X)) -> s(X)
     a__nats() -> nats()
     a__adx(X) -> adx(X)
     a__zeros() -> zeros()
     a__incr(X) -> incr(X)
     a__hd(X) -> hd(X)
     a__tl(X) -> tl(X)
   Qed