YES

Problem:
 a__incr(nil()) -> nil()
 a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
 a__adx(nil()) -> nil()
 a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
 a__nats() -> a__adx(a__zeros())
 a__zeros() -> cons(0(),zeros())
 a__head(cons(X,L)) -> mark(X)
 a__tail(cons(X,L)) -> mark(L)
 mark(incr(X)) -> a__incr(mark(X))
 mark(adx(X)) -> a__adx(mark(X))
 mark(nats()) -> a__nats()
 mark(zeros()) -> a__zeros()
 mark(head(X)) -> a__head(mark(X))
 mark(tail(X)) -> a__tail(mark(X))
 mark(nil()) -> nil()
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(s(X)) -> s(mark(X))
 mark(0()) -> 0()
 a__incr(X) -> incr(X)
 a__adx(X) -> adx(X)
 a__nats() -> nats()
 a__zeros() -> zeros()
 a__head(X) -> head(X)
 a__tail(X) -> tail(X)

Proof:
 DP Processor:
  DPs:
   a__incr#(cons(X,L)) -> mark#(X)
   a__adx#(cons(X,L)) -> mark#(X)
   a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
   a__nats#() -> a__zeros#()
   a__nats#() -> a__adx#(a__zeros())
   a__head#(cons(X,L)) -> mark#(X)
   a__tail#(cons(X,L)) -> mark#(L)
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> a__incr#(mark(X))
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> a__adx#(mark(X))
   mark#(nats()) -> a__nats#()
   mark#(zeros()) -> a__zeros#()
   mark#(head(X)) -> mark#(X)
   mark#(head(X)) -> a__head#(mark(X))
   mark#(tail(X)) -> mark#(X)
   mark#(tail(X)) -> a__tail#(mark(X))
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(s(X)) -> mark#(X)
  TRS:
   a__incr(nil()) -> nil()
   a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
   a__adx(nil()) -> nil()
   a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
   a__nats() -> a__adx(a__zeros())
   a__zeros() -> cons(0(),zeros())
   a__head(cons(X,L)) -> mark(X)
   a__tail(cons(X,L)) -> mark(L)
   mark(incr(X)) -> a__incr(mark(X))
   mark(adx(X)) -> a__adx(mark(X))
   mark(nats()) -> a__nats()
   mark(zeros()) -> a__zeros()
   mark(head(X)) -> a__head(mark(X))
   mark(tail(X)) -> a__tail(mark(X))
   mark(nil()) -> nil()
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(s(X)) -> s(mark(X))
   mark(0()) -> 0()
   a__incr(X) -> incr(X)
   a__adx(X) -> adx(X)
   a__nats() -> nats()
   a__zeros() -> zeros()
   a__head(X) -> head(X)
   a__tail(X) -> tail(X)
  TDG Processor:
   DPs:
    a__incr#(cons(X,L)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X)
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    a__nats#() -> a__zeros#()
    a__nats#() -> a__adx#(a__zeros())
    a__head#(cons(X,L)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L)
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> a__adx#(mark(X))
    mark#(nats()) -> a__nats#()
    mark#(zeros()) -> a__zeros#()
    mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> a__head#(mark(X))
    mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> a__tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X)
   TRS:
    a__incr(nil()) -> nil()
    a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
    a__adx(nil()) -> nil()
    a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
    a__nats() -> a__adx(a__zeros())
    a__zeros() -> cons(0(),zeros())
    a__head(cons(X,L)) -> mark(X)
    a__tail(cons(X,L)) -> mark(L)
    mark(incr(X)) -> a__incr(mark(X))
    mark(adx(X)) -> a__adx(mark(X))
    mark(nats()) -> a__nats()
    mark(zeros()) -> a__zeros()
    mark(head(X)) -> a__head(mark(X))
    mark(tail(X)) -> a__tail(mark(X))
    mark(nil()) -> nil()
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    mark(s(X)) -> s(mark(X))
    mark(0()) -> 0()
    a__incr(X) -> incr(X)
    a__adx(X) -> adx(X)
    a__nats() -> nats()
    a__zeros() -> zeros()
    a__head(X) -> head(X)
    a__tail(X) -> tail(X)
   graph:
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(s(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(tail(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(head(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(zeros()) -> a__zeros#()
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(nats()) -> a__nats#()
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(adx(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(incr(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__head#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__nats#() -> a__adx#(a__zeros()) ->
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    a__nats#() -> a__adx#(a__zeros()) ->
    a__adx#(cons(X,L)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L))) ->
    a__incr#(cons(X,L)) -> mark#(X)
    mark#(tail(X)) -> a__tail#(mark(X)) ->
    a__tail#(cons(X,L)) -> mark#(L)
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(tail(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(head(X)) -> a__head#(mark(X)) ->
    a__head#(cons(X,L)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(head(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(nats()) -> a__nats#() -> a__nats#() -> a__adx#(a__zeros())
    mark#(nats()) -> a__nats#() -> a__nats#() -> a__zeros#()
    mark#(adx(X)) -> a__adx#(mark(X)) ->
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    mark#(adx(X)) -> a__adx#(mark(X)) -> a__adx#(cons(X,L)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(adx(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X)) -> a__incr#(cons(X,L)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(s(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(head(X)) -> a__head#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(head(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> a__zeros#()
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(nats()) -> a__nats#()
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(adx(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(incr(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
   SCC Processor:
    #sccs: 1
    #rules: 17
    #arcs: 130/361
    DPs:
     a__tail#(cons(X,L)) -> mark#(L)
     mark#(incr(X)) -> mark#(X)
     mark#(incr(X)) -> a__incr#(mark(X))
     a__incr#(cons(X,L)) -> mark#(X)
     mark#(adx(X)) -> mark#(X)
     mark#(adx(X)) -> a__adx#(mark(X))
     a__adx#(cons(X,L)) -> mark#(X)
     mark#(nats()) -> a__nats#()
     a__nats#() -> a__adx#(a__zeros())
     a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
     mark#(head(X)) -> mark#(X)
     mark#(head(X)) -> a__head#(mark(X))
     a__head#(cons(X,L)) -> mark#(X)
     mark#(tail(X)) -> mark#(X)
     mark#(tail(X)) -> a__tail#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X)
    TRS:
     a__incr(nil()) -> nil()
     a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
     a__adx(nil()) -> nil()
     a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
     a__nats() -> a__adx(a__zeros())
     a__zeros() -> cons(0(),zeros())
     a__head(cons(X,L)) -> mark(X)
     a__tail(cons(X,L)) -> mark(L)
     mark(incr(X)) -> a__incr(mark(X))
     mark(adx(X)) -> a__adx(mark(X))
     mark(nats()) -> a__nats()
     mark(zeros()) -> a__zeros()
     mark(head(X)) -> a__head(mark(X))
     mark(tail(X)) -> a__tail(mark(X))
     mark(nil()) -> nil()
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     mark(s(X)) -> s(mark(X))
     mark(0()) -> 0()
     a__incr(X) -> incr(X)
     a__adx(X) -> adx(X)
     a__nats() -> nats()
     a__zeros() -> zeros()
     a__head(X) -> head(X)
     a__tail(X) -> tail(X)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [a__tail#](x0) = 3x0 + 1,
      
      [a__head#](x0) = x0 + 1,
      
      [a__nats#] = 3,
      
      [a__adx#](x0) = 2x0 + 1/2,
      
      [mark#](x0) = x0,
      
      [a__incr#](x0) = x0,
      
      [tail](x0) = 3x0 + 2,
      
      [head](x0) = 2x0 + 2,
      
      [nats] = 7/2,
      
      [a__tail](x0) = 3x0 + 2,
      
      [a__head](x0) = 2x0 + 2,
      
      [zeros] = 1,
      
      [0] = 0,
      
      [a__zeros] = 1,
      
      [a__nats] = 7/2,
      
      [adx](x0) = 2x0 + 1,
      
      [a__adx](x0) = 2x0 + 1,
      
      [incr](x0) = x0 + 1,
      
      [s](x0) = x0 + 1/2,
      
      [mark](x0) = x0,
      
      [cons](x0, x1) = x0 + 1/2x1 + 1/2,
      
      [a__incr](x0) = x0 + 1,
      
      [nil] = 0
     orientation:
      a__tail#(cons(X,L)) = 3/2L + 3X + 5/2 >= L = mark#(L)
      
      mark#(incr(X)) = X + 1 >= X = mark#(X)
      
      mark#(incr(X)) = X + 1 >= X = a__incr#(mark(X))
      
      a__incr#(cons(X,L)) = 1/2L + X + 1/2 >= X = mark#(X)
      
      mark#(adx(X)) = 2X + 1 >= X = mark#(X)
      
      mark#(adx(X)) = 2X + 1 >= 2X + 1/2 = a__adx#(mark(X))
      
      a__adx#(cons(X,L)) = L + 2X + 3/2 >= X = mark#(X)
      
      mark#(nats()) = 7/2 >= 3 = a__nats#()
      
      a__nats#() = 3 >= 5/2 = a__adx#(a__zeros())
      
      a__adx#(cons(X,L)) = L + 2X + 3/2 >= L + X + 1 = a__incr#(cons(mark(X),adx(L)))
      
      mark#(head(X)) = 2X + 2 >= X = mark#(X)
      
      mark#(head(X)) = 2X + 2 >= X + 1 = a__head#(mark(X))
      
      a__head#(cons(X,L)) = 1/2L + X + 3/2 >= X = mark#(X)
      
      mark#(tail(X)) = 3X + 2 >= X = mark#(X)
      
      mark#(tail(X)) = 3X + 2 >= 3X + 1 = a__tail#(mark(X))
      
      mark#(cons(X1,X2)) = X1 + 1/2X2 + 1/2 >= X1 = mark#(X1)
      
      mark#(s(X)) = X + 1/2 >= X = mark#(X)
      
      a__incr(nil()) = 1 >= 0 = nil()
      
      a__incr(cons(X,L)) = 1/2L + X + 3/2 >= 1/2L + X + 3/2 = cons(s(mark(X)),incr(L))
      
      a__adx(nil()) = 1 >= 0 = nil()
      
      a__adx(cons(X,L)) = L + 2X + 2 >= L + X + 2 = a__incr(cons(mark(X),adx(L)))
      
      a__nats() = 7/2 >= 3 = a__adx(a__zeros())
      
      a__zeros() = 1 >= 1 = cons(0(),zeros())
      
      a__head(cons(X,L)) = L + 2X + 3 >= X = mark(X)
      
      a__tail(cons(X,L)) = 3/2L + 3X + 7/2 >= L = mark(L)
      
      mark(incr(X)) = X + 1 >= X + 1 = a__incr(mark(X))
      
      mark(adx(X)) = 2X + 1 >= 2X + 1 = a__adx(mark(X))
      
      mark(nats()) = 7/2 >= 7/2 = a__nats()
      
      mark(zeros()) = 1 >= 1 = a__zeros()
      
      mark(head(X)) = 2X + 2 >= 2X + 2 = a__head(mark(X))
      
      mark(tail(X)) = 3X + 2 >= 3X + 2 = a__tail(mark(X))
      
      mark(nil()) = 0 >= 0 = nil()
      
      mark(cons(X1,X2)) = X1 + 1/2X2 + 1/2 >= X1 + 1/2X2 + 1/2 = cons(mark(X1),X2)
      
      mark(s(X)) = X + 1/2 >= X + 1/2 = s(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      a__incr(X) = X + 1 >= X + 1 = incr(X)
      
      a__adx(X) = 2X + 1 >= 2X + 1 = adx(X)
      
      a__nats() = 7/2 >= 7/2 = nats()
      
      a__zeros() = 1 >= 1 = zeros()
      
      a__head(X) = 2X + 2 >= 2X + 2 = head(X)
      
      a__tail(X) = 3X + 2 >= 3X + 2 = tail(X)
     problem:
      DPs:
       
      TRS:
       a__incr(nil()) -> nil()
       a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
       a__adx(nil()) -> nil()
       a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
       a__nats() -> a__adx(a__zeros())
       a__zeros() -> cons(0(),zeros())
       a__head(cons(X,L)) -> mark(X)
       a__tail(cons(X,L)) -> mark(L)
       mark(incr(X)) -> a__incr(mark(X))
       mark(adx(X)) -> a__adx(mark(X))
       mark(nats()) -> a__nats()
       mark(zeros()) -> a__zeros()
       mark(head(X)) -> a__head(mark(X))
       mark(tail(X)) -> a__tail(mark(X))
       mark(nil()) -> nil()
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(s(X)) -> s(mark(X))
       mark(0()) -> 0()
       a__incr(X) -> incr(X)
       a__adx(X) -> adx(X)
       a__nats() -> nats()
       a__zeros() -> zeros()
       a__head(X) -> head(X)
       a__tail(X) -> tail(X)
     Qed