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:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [tail](x0) = 6x0,
   
   [head](x0) = x0 + 4,
   
   [nats] = 0,
   
   [a__tail](x0) = 6x0,
   
   [a__head](x0) = x0 + 4,
   
   [zeros] = 0,
   
   [0] = 0,
   
   [a__zeros] = 0,
   
   [a__nats] = 0,
   
   [adx](x0) = 2x0,
   
   [a__adx](x0) = 2x0,
   
   [incr](x0) = x0,
   
   [s](x0) = x0,
   
   [mark](x0) = x0,
   
   [cons](x0, x1) = x0 + x1,
   
   [a__incr](x0) = x0,
   
   [nil] = 0
  orientation:
   a__incr(nil()) = 0 >= 0 = nil()
   
   a__incr(cons(X,L)) = L + X >= L + X = cons(s(mark(X)),incr(L))
   
   a__adx(nil()) = 0 >= 0 = nil()
   
   a__adx(cons(X,L)) = 2L + 2X >= 2L + X = a__incr(cons(mark(X),adx(L)))
   
   a__nats() = 0 >= 0 = a__adx(a__zeros())
   
   a__zeros() = 0 >= 0 = cons(0(),zeros())
   
   a__head(cons(X,L)) = L + X + 4 >= X = mark(X)
   
   a__tail(cons(X,L)) = 6L + 6X >= L = mark(L)
   
   mark(incr(X)) = X >= X = a__incr(mark(X))
   
   mark(adx(X)) = 2X >= 2X = a__adx(mark(X))
   
   mark(nats()) = 0 >= 0 = a__nats()
   
   mark(zeros()) = 0 >= 0 = a__zeros()
   
   mark(head(X)) = X + 4 >= X + 4 = a__head(mark(X))
   
   mark(tail(X)) = 6X >= 6X = a__tail(mark(X))
   
   mark(nil()) = 0 >= 0 = nil()
   
   mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(mark(X1),X2)
   
   mark(s(X)) = X >= X = s(mark(X))
   
   mark(0()) = 0 >= 0 = 0()
   
   a__incr(X) = X >= X = incr(X)
   
   a__adx(X) = 2X >= 2X = adx(X)
   
   a__nats() = 0 >= 0 = nats()
   
   a__zeros() = 0 >= 0 = zeros()
   
   a__head(X) = X + 4 >= X + 4 = head(X)
   
   a__tail(X) = 6X >= 6X = tail(X)
  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__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:
    [tail](x0) = 4x0 + 4,
    
    [head](x0) = 5x0 + 1,
    
    [nats] = 1,
    
    [a__tail](x0) = 4x0 + 4,
    
    [a__head](x0) = 5x0 + 1,
    
    [zeros] = 0,
    
    [0] = 0,
    
    [a__zeros] = 0,
    
    [a__nats] = 1,
    
    [adx](x0) = 2x0,
    
    [a__adx](x0) = 2x0,
    
    [incr](x0) = x0,
    
    [s](x0) = x0,
    
    [mark](x0) = x0,
    
    [cons](x0, x1) = 2x0 + 2x1,
    
    [a__incr](x0) = x0,
    
    [nil] = 0
   orientation:
    a__incr(nil()) = 0 >= 0 = nil()
    
    a__incr(cons(X,L)) = 2L + 2X >= 2L + 2X = cons(s(mark(X)),incr(L))
    
    a__adx(nil()) = 0 >= 0 = nil()
    
    a__adx(cons(X,L)) = 4L + 4X >= 4L + 2X = a__incr(cons(mark(X),adx(L)))
    
    a__nats() = 1 >= 0 = a__adx(a__zeros())
    
    a__zeros() = 0 >= 0 = cons(0(),zeros())
    
    a__tail(cons(X,L)) = 8L + 8X + 4 >= L = mark(L)
    
    mark(incr(X)) = X >= X = a__incr(mark(X))
    
    mark(adx(X)) = 2X >= 2X = a__adx(mark(X))
    
    mark(nats()) = 1 >= 1 = a__nats()
    
    mark(zeros()) = 0 >= 0 = a__zeros()
    
    mark(head(X)) = 5X + 1 >= 5X + 1 = a__head(mark(X))
    
    mark(tail(X)) = 4X + 4 >= 4X + 4 = a__tail(mark(X))
    
    mark(nil()) = 0 >= 0 = nil()
    
    mark(cons(X1,X2)) = 2X1 + 2X2 >= 2X1 + 2X2 = cons(mark(X1),X2)
    
    mark(s(X)) = X >= X = s(mark(X))
    
    mark(0()) = 0 >= 0 = 0()
    
    a__incr(X) = X >= X = incr(X)
    
    a__adx(X) = 2X >= 2X = adx(X)
    
    a__nats() = 1 >= 1 = nats()
    
    a__zeros() = 0 >= 0 = zeros()
    
    a__head(X) = 5X + 1 >= 5X + 1 = head(X)
    
    a__tail(X) = 4X + 4 >= 4X + 4 = tail(X)
   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__zeros() -> cons(0(),zeros())
    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:
     [tail](x0) = 4x0 + 2,
     
     [head](x0) = 4x0 + 4,
     
     [nats] = 0,
     
     [a__tail](x0) = 4x0 + 2,
     
     [a__head](x0) = 4x0 + 4,
     
     [zeros] = 0,
     
     [0] = 0,
     
     [a__zeros] = 0,
     
     [a__nats] = 0,
     
     [adx](x0) = x0 + 2,
     
     [a__adx](x0) = x0 + 2,
     
     [incr](x0) = x0,
     
     [s](x0) = x0,
     
     [mark](x0) = x0,
     
     [cons](x0, x1) = 2x0 + x1,
     
     [a__incr](x0) = x0,
     
     [nil] = 0
    orientation:
     a__incr(nil()) = 0 >= 0 = nil()
     
     a__incr(cons(X,L)) = L + 2X >= L + 2X = cons(s(mark(X)),incr(L))
     
     a__adx(nil()) = 2 >= 0 = nil()
     
     a__adx(cons(X,L)) = L + 2X + 2 >= L + 2X + 2 = a__incr(cons(mark(X),adx(L)))
     
     a__zeros() = 0 >= 0 = cons(0(),zeros())
     
     mark(incr(X)) = X >= X = a__incr(mark(X))
     
     mark(adx(X)) = X + 2 >= X + 2 = a__adx(mark(X))
     
     mark(nats()) = 0 >= 0 = a__nats()
     
     mark(zeros()) = 0 >= 0 = a__zeros()
     
     mark(head(X)) = 4X + 4 >= 4X + 4 = a__head(mark(X))
     
     mark(tail(X)) = 4X + 2 >= 4X + 2 = a__tail(mark(X))
     
     mark(nil()) = 0 >= 0 = nil()
     
     mark(cons(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = cons(mark(X1),X2)
     
     mark(s(X)) = X >= X = s(mark(X))
     
     mark(0()) = 0 >= 0 = 0()
     
     a__incr(X) = X >= X = incr(X)
     
     a__adx(X) = X + 2 >= X + 2 = adx(X)
     
     a__nats() = 0 >= 0 = nats()
     
     a__zeros() = 0 >= 0 = zeros()
     
     a__head(X) = 4X + 4 >= 4X + 4 = head(X)
     
     a__tail(X) = 4X + 2 >= 4X + 2 = tail(X)
    problem:
     a__incr(nil()) -> nil()
     a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
     a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
     a__zeros() -> cons(0(),zeros())
     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)
    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)))
      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(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
      a__zeros() -> cons(0(),zeros())
      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)))
       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(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
       a__zeros() -> cons(0(),zeros())
       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__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)) -> 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)) -> 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#(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: 11
       #arcs: 100/225
       DPs:
        a__adx#(cons(X,L)) -> mark#(X)
        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)) -> a__incr#(cons(mark(X),adx(L)))
        mark#(head(X)) -> mark#(X)
        mark#(tail(X)) -> 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(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
        a__zeros() -> cons(0(),zeros())
        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)
       Semantic Labeling Processor:
        dimension: 1
        usable rules:
         
        interpretation:
         [tail](x0) = x0,
         
         [head](x0) = x0,
         
         [nats] = 0,
         
         [a__tail](x0) = x0,
         
         [a__head](x0) = x0,
         
         [zeros] = 0,
         
         [0] = 0,
         
         [a__zeros] = 0,
         
         [a__nats] = 0,
         
         [adx](x0) = x0 + 1,
         
         [a__adx](x0) = x0 + 1,
         
         [incr](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [mark](x0) = x0,
         
         [cons](x0, x1) = x0,
         
         [a__incr](x0) = x0 + 1,
         
         [nil] = 1
         labeled:
          a__adx#
          cons
          mark#
          a__incr#
         usable (for model):
          a__adx#
          cons
          mark#
          incr
          a__incr#
          mark
          adx
          head
          tail
          s
          a__incr
          nil
          a__adx
          a__zeros
          0
          zeros
          nats
          a__nats
          a__head
          a__tail
         argument filtering:
          pi(nil) = []
          pi(a__incr) = 0
          pi(cons) = 1
          pi(mark) = 0
          pi(s) = []
          pi(incr) = 0
          pi(a__adx) = 0
          pi(adx) = []
          pi(a__nats) = []
          pi(a__zeros) = []
          pi(0) = []
          pi(zeros) = []
          pi(a__head) = []
          pi(a__tail) = 0
          pi(nats) = []
          pi(head) = []
          pi(tail) = 0
          pi(a__incr#) = []
          pi(mark#) = []
          pi(a__adx#) = []
        precedence:
         a__adx# > a__incr# > mark# ~ tail ~ head ~ nats ~ a__tail ~ 
         a__head ~ zeros ~ 0 ~ a__zeros ~ a__nats ~ adx ~ a__adx ~ incr ~ 
         s ~ mark ~ cons ~ a__incr ~ nil
        problem:
         DPs:
          mark#(head(X)) -> mark#(X)
          mark#(tail(X)) -> mark#(X)
          mark#(cons(X1,X2)) -> mark#(X1)
         TRS:
          a__incr(nil()) -> nil()
          a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
          a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
          a__zeros() -> cons(0(),zeros())
          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)
        Restore Modifier:
         DPs:
          mark#(head(X)) -> mark#(X)
          mark#(tail(X)) -> mark#(X)
          mark#(cons(X1,X2)) -> mark#(X1)
         TRS:
          a__incr(nil()) -> nil()
          a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
          a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
          a__zeros() -> cons(0(),zeros())
          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)
         Bounds Processor:
          bound: 0
          enrichment: match-dp
          automaton:
           final states: {5}
           transitions:
            mark{#,0}(6) -> 5*
            f820() -> 6*
          problem:
           DPs:
            mark#(head(X)) -> mark#(X)
            mark#(tail(X)) -> mark#(X)
           TRS:
            a__incr(nil()) -> nil()
            a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
            a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
            a__zeros() -> cons(0(),zeros())
            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)
          Bounds Processor:
           bound: 0
           enrichment: match-dp
           automaton:
            final states: {3}
            transitions:
             mark{#,0}(4) -> 3*
             f850() -> 4*
           problem:
            DPs:
             mark#(head(X)) -> mark#(X)
            TRS:
             a__incr(nil()) -> nil()
             a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
             a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
             a__zeros() -> cons(0(),zeros())
             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)
           Bounds Processor:
            bound: 0
            enrichment: match-dp
            automaton:
             final states: {1}
             transitions:
              mark{#,0}(2) -> 1*
              f870() -> 2*
            problem:
             DPs:
              
             TRS:
              a__incr(nil()) -> nil()
              a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
              a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
              a__zeros() -> cons(0(),zeros())
              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