YES

Problem:
 a__nats() -> cons(0(),incr(nats()))
 a__pairs() -> cons(0(),incr(odds()))
 a__odds() -> a__incr(a__pairs())
 a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
 a__head(cons(X,XS)) -> mark(X)
 a__tail(cons(X,XS)) -> mark(XS)
 mark(nats()) -> a__nats()
 mark(incr(X)) -> a__incr(mark(X))
 mark(pairs()) -> a__pairs()
 mark(odds()) -> a__odds()
 mark(head(X)) -> a__head(mark(X))
 mark(tail(X)) -> a__tail(mark(X))
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(0()) -> 0()
 mark(s(X)) -> s(mark(X))
 a__nats() -> nats()
 a__incr(X) -> incr(X)
 a__pairs() -> pairs()
 a__odds() -> odds()
 a__head(X) -> head(X)
 a__tail(X) -> tail(X)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [tail](x0) = 5x0 + 2,
   
   [head](x0) = 2x0,
   
   [pairs] = 0,
   
   [a__tail](x0) = 5x0 + 2,
   
   [a__head](x0) = 2x0,
   
   [s](x0) = x0,
   
   [mark](x0) = x0,
   
   [a__incr](x0) = x0,
   
   [a__odds] = 0,
   
   [odds] = 0,
   
   [a__pairs] = 0,
   
   [cons](x0, x1) = 4x0 + 2x1,
   
   [incr](x0) = x0,
   
   [nats] = 0,
   
   [0] = 0,
   
   [a__nats] = 0
  orientation:
   a__nats() = 0 >= 0 = cons(0(),incr(nats()))
   
   a__pairs() = 0 >= 0 = cons(0(),incr(odds()))
   
   a__odds() = 0 >= 0 = a__incr(a__pairs())
   
   a__incr(cons(X,XS)) = 4X + 2XS >= 4X + 2XS = cons(s(mark(X)),incr(XS))
   
   a__head(cons(X,XS)) = 8X + 4XS >= X = mark(X)
   
   a__tail(cons(X,XS)) = 20X + 10XS + 2 >= XS = mark(XS)
   
   mark(nats()) = 0 >= 0 = a__nats()
   
   mark(incr(X)) = X >= X = a__incr(mark(X))
   
   mark(pairs()) = 0 >= 0 = a__pairs()
   
   mark(odds()) = 0 >= 0 = a__odds()
   
   mark(head(X)) = 2X >= 2X = a__head(mark(X))
   
   mark(tail(X)) = 5X + 2 >= 5X + 2 = a__tail(mark(X))
   
   mark(cons(X1,X2)) = 4X1 + 2X2 >= 4X1 + 2X2 = cons(mark(X1),X2)
   
   mark(0()) = 0 >= 0 = 0()
   
   mark(s(X)) = X >= X = s(mark(X))
   
   a__nats() = 0 >= 0 = nats()
   
   a__incr(X) = X >= X = incr(X)
   
   a__pairs() = 0 >= 0 = pairs()
   
   a__odds() = 0 >= 0 = odds()
   
   a__head(X) = 2X >= 2X = head(X)
   
   a__tail(X) = 5X + 2 >= 5X + 2 = tail(X)
  problem:
   a__nats() -> cons(0(),incr(nats()))
   a__pairs() -> cons(0(),incr(odds()))
   a__odds() -> a__incr(a__pairs())
   a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
   a__head(cons(X,XS)) -> mark(X)
   mark(nats()) -> a__nats()
   mark(incr(X)) -> a__incr(mark(X))
   mark(pairs()) -> a__pairs()
   mark(odds()) -> a__odds()
   mark(head(X)) -> a__head(mark(X))
   mark(tail(X)) -> a__tail(mark(X))
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(0()) -> 0()
   mark(s(X)) -> s(mark(X))
   a__nats() -> nats()
   a__incr(X) -> incr(X)
   a__pairs() -> pairs()
   a__odds() -> odds()
   a__head(X) -> head(X)
   a__tail(X) -> tail(X)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [tail](x0) = 2x0,
    
    [head](x0) = 2x0 + 1,
    
    [pairs] = 0,
    
    [a__tail](x0) = 2x0,
    
    [a__head](x0) = 2x0 + 2,
    
    [s](x0) = x0,
    
    [mark](x0) = 2x0,
    
    [a__incr](x0) = 2x0,
    
    [a__odds] = 0,
    
    [odds] = 0,
    
    [a__pairs] = 0,
    
    [cons](x0, x1) = 4x0 + x1,
    
    [incr](x0) = 2x0,
    
    [nats] = 0,
    
    [0] = 0,
    
    [a__nats] = 0
   orientation:
    a__nats() = 0 >= 0 = cons(0(),incr(nats()))
    
    a__pairs() = 0 >= 0 = cons(0(),incr(odds()))
    
    a__odds() = 0 >= 0 = a__incr(a__pairs())
    
    a__incr(cons(X,XS)) = 8X + 2XS >= 8X + 2XS = cons(s(mark(X)),incr(XS))
    
    a__head(cons(X,XS)) = 8X + 2XS + 2 >= 2X = mark(X)
    
    mark(nats()) = 0 >= 0 = a__nats()
    
    mark(incr(X)) = 4X >= 4X = a__incr(mark(X))
    
    mark(pairs()) = 0 >= 0 = a__pairs()
    
    mark(odds()) = 0 >= 0 = a__odds()
    
    mark(head(X)) = 4X + 2 >= 4X + 2 = a__head(mark(X))
    
    mark(tail(X)) = 4X >= 4X = a__tail(mark(X))
    
    mark(cons(X1,X2)) = 8X1 + 2X2 >= 8X1 + X2 = cons(mark(X1),X2)
    
    mark(0()) = 0 >= 0 = 0()
    
    mark(s(X)) = 2X >= 2X = s(mark(X))
    
    a__nats() = 0 >= 0 = nats()
    
    a__incr(X) = 2X >= 2X = incr(X)
    
    a__pairs() = 0 >= 0 = pairs()
    
    a__odds() = 0 >= 0 = odds()
    
    a__head(X) = 2X + 2 >= 2X + 1 = head(X)
    
    a__tail(X) = 2X >= 2X = tail(X)
   problem:
    a__nats() -> cons(0(),incr(nats()))
    a__pairs() -> cons(0(),incr(odds()))
    a__odds() -> a__incr(a__pairs())
    a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
    mark(nats()) -> a__nats()
    mark(incr(X)) -> a__incr(mark(X))
    mark(pairs()) -> a__pairs()
    mark(odds()) -> a__odds()
    mark(head(X)) -> a__head(mark(X))
    mark(tail(X)) -> a__tail(mark(X))
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    mark(0()) -> 0()
    mark(s(X)) -> s(mark(X))
    a__nats() -> nats()
    a__incr(X) -> incr(X)
    a__pairs() -> pairs()
    a__odds() -> odds()
    a__tail(X) -> tail(X)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [tail](x0) = 2x0 + 2,
     
     [head](x0) = 4x0,
     
     [pairs] = 0,
     
     [a__tail](x0) = 2x0 + 4,
     
     [a__head](x0) = 2x0,
     
     [s](x0) = x0,
     
     [mark](x0) = 2x0,
     
     [a__incr](x0) = 2x0,
     
     [a__odds] = 0,
     
     [odds] = 0,
     
     [a__pairs] = 0,
     
     [cons](x0, x1) = x0 + 4x1,
     
     [incr](x0) = 2x0,
     
     [nats] = 0,
     
     [0] = 0,
     
     [a__nats] = 0
    orientation:
     a__nats() = 0 >= 0 = cons(0(),incr(nats()))
     
     a__pairs() = 0 >= 0 = cons(0(),incr(odds()))
     
     a__odds() = 0 >= 0 = a__incr(a__pairs())
     
     a__incr(cons(X,XS)) = 2X + 8XS >= 2X + 8XS = cons(s(mark(X)),incr(XS))
     
     mark(nats()) = 0 >= 0 = a__nats()
     
     mark(incr(X)) = 4X >= 4X = a__incr(mark(X))
     
     mark(pairs()) = 0 >= 0 = a__pairs()
     
     mark(odds()) = 0 >= 0 = a__odds()
     
     mark(head(X)) = 8X >= 4X = a__head(mark(X))
     
     mark(tail(X)) = 4X + 4 >= 4X + 4 = a__tail(mark(X))
     
     mark(cons(X1,X2)) = 2X1 + 8X2 >= 2X1 + 4X2 = cons(mark(X1),X2)
     
     mark(0()) = 0 >= 0 = 0()
     
     mark(s(X)) = 2X >= 2X = s(mark(X))
     
     a__nats() = 0 >= 0 = nats()
     
     a__incr(X) = 2X >= 2X = incr(X)
     
     a__pairs() = 0 >= 0 = pairs()
     
     a__odds() = 0 >= 0 = odds()
     
     a__tail(X) = 2X + 4 >= 2X + 2 = tail(X)
    problem:
     a__nats() -> cons(0(),incr(nats()))
     a__pairs() -> cons(0(),incr(odds()))
     a__odds() -> a__incr(a__pairs())
     a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
     mark(nats()) -> a__nats()
     mark(incr(X)) -> a__incr(mark(X))
     mark(pairs()) -> a__pairs()
     mark(odds()) -> a__odds()
     mark(head(X)) -> a__head(mark(X))
     mark(tail(X)) -> a__tail(mark(X))
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     a__nats() -> nats()
     a__incr(X) -> incr(X)
     a__pairs() -> pairs()
     a__odds() -> odds()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [tail](x0) = 6x0,
      
      [head](x0) = 7x0 + 4,
      
      [pairs] = 0,
      
      [a__tail](x0) = 6x0,
      
      [a__head](x0) = 4x0 + 2,
      
      [s](x0) = 2x0,
      
      [mark](x0) = x0,
      
      [a__incr](x0) = 2x0,
      
      [a__odds] = 0,
      
      [odds] = 0,
      
      [a__pairs] = 0,
      
      [cons](x0, x1) = 4x0 + 2x1,
      
      [incr](x0) = 2x0,
      
      [nats] = 0,
      
      [0] = 0,
      
      [a__nats] = 0
     orientation:
      a__nats() = 0 >= 0 = cons(0(),incr(nats()))
      
      a__pairs() = 0 >= 0 = cons(0(),incr(odds()))
      
      a__odds() = 0 >= 0 = a__incr(a__pairs())
      
      a__incr(cons(X,XS)) = 8X + 4XS >= 8X + 4XS = cons(s(mark(X)),incr(XS))
      
      mark(nats()) = 0 >= 0 = a__nats()
      
      mark(incr(X)) = 2X >= 2X = a__incr(mark(X))
      
      mark(pairs()) = 0 >= 0 = a__pairs()
      
      mark(odds()) = 0 >= 0 = a__odds()
      
      mark(head(X)) = 7X + 4 >= 4X + 2 = a__head(mark(X))
      
      mark(tail(X)) = 6X >= 6X = a__tail(mark(X))
      
      mark(cons(X1,X2)) = 4X1 + 2X2 >= 4X1 + 2X2 = cons(mark(X1),X2)
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = 2X >= 2X = s(mark(X))
      
      a__nats() = 0 >= 0 = nats()
      
      a__incr(X) = 2X >= 2X = incr(X)
      
      a__pairs() = 0 >= 0 = pairs()
      
      a__odds() = 0 >= 0 = odds()
     problem:
      a__nats() -> cons(0(),incr(nats()))
      a__pairs() -> cons(0(),incr(odds()))
      a__odds() -> a__incr(a__pairs())
      a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
      mark(nats()) -> a__nats()
      mark(incr(X)) -> a__incr(mark(X))
      mark(pairs()) -> a__pairs()
      mark(odds()) -> a__odds()
      mark(tail(X)) -> a__tail(mark(X))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(0()) -> 0()
      mark(s(X)) -> s(mark(X))
      a__nats() -> nats()
      a__incr(X) -> incr(X)
      a__pairs() -> pairs()
      a__odds() -> odds()
     DP Processor:
      DPs:
       a__odds#() -> a__pairs#()
       a__odds#() -> a__incr#(a__pairs())
       a__incr#(cons(X,XS)) -> mark#(X)
       mark#(nats()) -> a__nats#()
       mark#(incr(X)) -> mark#(X)
       mark#(incr(X)) -> a__incr#(mark(X))
       mark#(pairs()) -> a__pairs#()
       mark#(odds()) -> a__odds#()
       mark#(tail(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X)
      TRS:
       a__nats() -> cons(0(),incr(nats()))
       a__pairs() -> cons(0(),incr(odds()))
       a__odds() -> a__incr(a__pairs())
       a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
       mark(nats()) -> a__nats()
       mark(incr(X)) -> a__incr(mark(X))
       mark(pairs()) -> a__pairs()
       mark(odds()) -> a__odds()
       mark(tail(X)) -> a__tail(mark(X))
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(0()) -> 0()
       mark(s(X)) -> s(mark(X))
       a__nats() -> nats()
       a__incr(X) -> incr(X)
       a__pairs() -> pairs()
       a__odds() -> odds()
      TDG Processor:
       DPs:
        a__odds#() -> a__pairs#()
        a__odds#() -> a__incr#(a__pairs())
        a__incr#(cons(X,XS)) -> mark#(X)
        mark#(nats()) -> a__nats#()
        mark#(incr(X)) -> mark#(X)
        mark#(incr(X)) -> a__incr#(mark(X))
        mark#(pairs()) -> a__pairs#()
        mark#(odds()) -> a__odds#()
        mark#(tail(X)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(s(X)) -> mark#(X)
       TRS:
        a__nats() -> cons(0(),incr(nats()))
        a__pairs() -> cons(0(),incr(odds()))
        a__odds() -> a__incr(a__pairs())
        a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
        mark(nats()) -> a__nats()
        mark(incr(X)) -> a__incr(mark(X))
        mark(pairs()) -> a__pairs()
        mark(odds()) -> a__odds()
        mark(tail(X)) -> a__tail(mark(X))
        mark(cons(X1,X2)) -> cons(mark(X1),X2)
        mark(0()) -> 0()
        mark(s(X)) -> s(mark(X))
        a__nats() -> nats()
        a__incr(X) -> incr(X)
        a__pairs() -> pairs()
        a__odds() -> odds()
       graph:
        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)) -> mark#(X)
        mark#(tail(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
        mark#(tail(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
        mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
        mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
        mark#(tail(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
        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)) -> mark#(X)
        mark#(s(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
        mark#(s(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
        mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
        mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
        mark#(s(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
        mark#(odds()) -> a__odds#() ->
        a__odds#() -> a__incr#(a__pairs())
        mark#(odds()) -> a__odds#() -> a__odds#() -> a__pairs#()
        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)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(odds()) -> a__odds#()
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(pairs()) -> a__pairs#()
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(incr(X)) -> a__incr#(mark(X))
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(incr(X)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1) -> mark#(nats()) -> a__nats#()
        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)) -> mark#(X)
        mark#(incr(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
        mark#(incr(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
        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)) -> mark#(X) ->
        mark#(nats()) -> a__nats#()
        mark#(incr(X)) -> a__incr#(mark(X)) ->
        a__incr#(cons(X,XS)) -> mark#(X)
        a__incr#(cons(X,XS)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(cons(X1,X2)) -> mark#(X1)
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(tail(X)) -> mark#(X)
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(odds()) -> a__odds#()
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(pairs()) -> a__pairs#()
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(incr(X)) -> a__incr#(mark(X))
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(incr(X)) -> mark#(X)
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(nats()) -> a__nats#()
        a__odds#() -> a__incr#(a__pairs()) -> a__incr#(cons(X,XS)) -> mark#(X)
       SCC Processor:
        #sccs: 1
        #rules: 8
        #arcs: 44/121
        DPs:
         mark#(tail(X)) -> mark#(X)
         mark#(incr(X)) -> mark#(X)
         mark#(incr(X)) -> a__incr#(mark(X))
         a__incr#(cons(X,XS)) -> mark#(X)
         mark#(odds()) -> a__odds#()
         a__odds#() -> a__incr#(a__pairs())
         mark#(cons(X1,X2)) -> mark#(X1)
         mark#(s(X)) -> mark#(X)
        TRS:
         a__nats() -> cons(0(),incr(nats()))
         a__pairs() -> cons(0(),incr(odds()))
         a__odds() -> a__incr(a__pairs())
         a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
         mark(nats()) -> a__nats()
         mark(incr(X)) -> a__incr(mark(X))
         mark(pairs()) -> a__pairs()
         mark(odds()) -> a__odds()
         mark(tail(X)) -> a__tail(mark(X))
         mark(cons(X1,X2)) -> cons(mark(X1),X2)
         mark(0()) -> 0()
         mark(s(X)) -> s(mark(X))
         a__nats() -> nats()
         a__incr(X) -> incr(X)
         a__pairs() -> pairs()
         a__odds() -> odds()
        Bounds Processor:
         bound: 0
         enrichment: match-dp
         automaton:
          final states: {11}
          transitions:
           incr0(21) -> 22*
           a__incr{#,0}(12) -> 11*
           00() -> 23*
           odds0() -> 21*
           cons0(23,22) -> 12*
           mark{#,0}(23) -> 11*
           pairs0() -> 12*
           a__pairs0() -> 12*
         problem:
          DPs:
           mark#(tail(X)) -> mark#(X)
           mark#(incr(X)) -> mark#(X)
           mark#(incr(X)) -> a__incr#(mark(X))
           a__incr#(cons(X,XS)) -> mark#(X)
           mark#(odds()) -> a__odds#()
           mark#(cons(X1,X2)) -> mark#(X1)
           mark#(s(X)) -> mark#(X)
          TRS:
           a__nats() -> cons(0(),incr(nats()))
           a__pairs() -> cons(0(),incr(odds()))
           a__odds() -> a__incr(a__pairs())
           a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
           mark(nats()) -> a__nats()
           mark(incr(X)) -> a__incr(mark(X))
           mark(pairs()) -> a__pairs()
           mark(odds()) -> a__odds()
           mark(tail(X)) -> a__tail(mark(X))
           mark(cons(X1,X2)) -> cons(mark(X1),X2)
           mark(0()) -> 0()
           mark(s(X)) -> s(mark(X))
           a__nats() -> nats()
           a__incr(X) -> incr(X)
           a__pairs() -> pairs()
           a__odds() -> odds()
         SCC Processor:
          #sccs: 1
          #rules: 6
          #arcs: 33/49
          DPs:
           mark#(tail(X)) -> mark#(X)
           mark#(incr(X)) -> mark#(X)
           mark#(incr(X)) -> a__incr#(mark(X))
           a__incr#(cons(X,XS)) -> mark#(X)
           mark#(cons(X1,X2)) -> mark#(X1)
           mark#(s(X)) -> mark#(X)
          TRS:
           a__nats() -> cons(0(),incr(nats()))
           a__pairs() -> cons(0(),incr(odds()))
           a__odds() -> a__incr(a__pairs())
           a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
           mark(nats()) -> a__nats()
           mark(incr(X)) -> a__incr(mark(X))
           mark(pairs()) -> a__pairs()
           mark(odds()) -> a__odds()
           mark(tail(X)) -> a__tail(mark(X))
           mark(cons(X1,X2)) -> cons(mark(X1),X2)
           mark(0()) -> 0()
           mark(s(X)) -> s(mark(X))
           a__nats() -> nats()
           a__incr(X) -> incr(X)
           a__pairs() -> pairs()
           a__odds() -> odds()
          Semantic Labeling Processor:
           dimension: 1
           usable rules:
            
           interpretation:
            [tail](x0) = x0 + 1,
            
            [pairs] = 0,
            
            [a__tail](x0) = 1,
            
            [s](x0) = x0,
            
            [mark](x0) = x0,
            
            [a__incr](x0) = x0 + 1,
            
            [a__odds] = 1,
            
            [odds] = 1,
            
            [a__pairs] = 0,
            
            [cons](x0, x1) = x0,
            
            [incr](x0) = x0 + 1,
            
            [nats] = 1,
            
            [0] = 0,
            
            [a__nats] = 1
            labeled:
             mark#
             a__incr#
            usable (for model):
             mark#
             tail
             incr
             a__incr#
             mark
             cons
             s
             a__nats
             0
             nats
             a__pairs
             odds
             a__odds
             a__incr
             pairs
             a__tail
            argument filtering:
             pi(a__nats) = []
             pi(0) = []
             pi(nats) = []
             pi(incr) = 0
             pi(cons) = 1
             pi(a__pairs) = []
             pi(odds) = []
             pi(a__odds) = []
             pi(a__incr) = 0
             pi(mark) = []
             pi(s) = []
             pi(a__tail) = 0
             pi(pairs) = []
             pi(tail) = 0
             pi(a__incr#) = []
             pi(mark#) = []
           precedence:
            a__incr# > mark# ~ tail ~ pairs ~ a__tail ~ s ~ mark ~ a__incr ~ 
            a__odds ~ odds ~ a__pairs ~ cons ~ incr ~ nats ~ 0 ~ a__nats
           problem:
            DPs:
             mark#(cons(X1,X2)) -> mark#(X1)
             mark#(s(X)) -> mark#(X)
            TRS:
             a__nats() -> cons(0(),incr(nats()))
             a__pairs() -> cons(0(),incr(odds()))
             a__odds() -> a__incr(a__pairs())
             a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
             mark(nats()) -> a__nats()
             mark(incr(X)) -> a__incr(mark(X))
             mark(pairs()) -> a__pairs()
             mark(odds()) -> a__odds()
             mark(tail(X)) -> a__tail(mark(X))
             mark(cons(X1,X2)) -> cons(mark(X1),X2)
             mark(0()) -> 0()
             mark(s(X)) -> s(mark(X))
             a__nats() -> nats()
             a__incr(X) -> incr(X)
             a__pairs() -> pairs()
             a__odds() -> odds()
           Restore Modifier:
            DPs:
             mark#(cons(X1,X2)) -> mark#(X1)
             mark#(s(X)) -> mark#(X)
            TRS:
             a__nats() -> cons(0(),incr(nats()))
             a__pairs() -> cons(0(),incr(odds()))
             a__odds() -> a__incr(a__pairs())
             a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
             mark(nats()) -> a__nats()
             mark(incr(X)) -> a__incr(mark(X))
             mark(pairs()) -> a__pairs()
             mark(odds()) -> a__odds()
             mark(tail(X)) -> a__tail(mark(X))
             mark(cons(X1,X2)) -> cons(mark(X1),X2)
             mark(0()) -> 0()
             mark(s(X)) -> s(mark(X))
             a__nats() -> nats()
             a__incr(X) -> incr(X)
             a__pairs() -> pairs()
             a__odds() -> odds()
            Bounds Processor:
             bound: 0
             enrichment: match-dp
             automaton:
              final states: {3}
              transitions:
               f830() -> 4*
               mark{#,0}(4) -> 3*
             problem:
              DPs:
               mark#(cons(X1,X2)) -> mark#(X1)
              TRS:
               a__nats() -> cons(0(),incr(nats()))
               a__pairs() -> cons(0(),incr(odds()))
               a__odds() -> a__incr(a__pairs())
               a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
               mark(nats()) -> a__nats()
               mark(incr(X)) -> a__incr(mark(X))
               mark(pairs()) -> a__pairs()
               mark(odds()) -> a__odds()
               mark(tail(X)) -> a__tail(mark(X))
               mark(cons(X1,X2)) -> cons(mark(X1),X2)
               mark(0()) -> 0()
               mark(s(X)) -> s(mark(X))
               a__nats() -> nats()
               a__incr(X) -> incr(X)
               a__pairs() -> pairs()
               a__odds() -> odds()
             Bounds Processor:
              bound: 0
              enrichment: match-dp
              automaton:
               final states: {1}
               transitions:
                mark{#,0}(2) -> 1*
                f850() -> 2*
              problem:
               DPs:
                
               TRS:
                a__nats() -> cons(0(),incr(nats()))
                a__pairs() -> cons(0(),incr(odds()))
                a__odds() -> a__incr(a__pairs())
                a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
                mark(nats()) -> a__nats()
                mark(incr(X)) -> a__incr(mark(X))
                mark(pairs()) -> a__pairs()
                mark(odds()) -> a__odds()
                mark(tail(X)) -> a__tail(mark(X))
                mark(cons(X1,X2)) -> cons(mark(X1),X2)
                mark(0()) -> 0()
                mark(s(X)) -> s(mark(X))
                a__nats() -> nats()
                a__incr(X) -> incr(X)
                a__pairs() -> pairs()
                a__odds() -> odds()
              Qed