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(pairs()) -> a__pairs()
 mark(odds()) -> a__odds()
 mark(incr(X)) -> a__incr(mark(X))
 mark(head(X)) -> a__head(mark(X))
 mark(tail(X)) -> a__tail(mark(X))
 mark(0()) -> 0()
 mark(s(X)) -> s(mark(X))
 mark(nil()) -> nil()
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 a__nats() -> nats()
 a__pairs() -> pairs()
 a__odds() -> odds()
 a__incr(X) -> incr(X)
 a__head(X) -> head(X)
 a__tail(X) -> tail(X)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [nil] = 0,
   
   [tail](x0) = 2x0 + 2,
   
   [head](x0) = 3x0 + 4,
   
   [pairs] = 0,
   
   [a__tail](x0) = 2x0 + 2,
   
   [a__head](x0) = 3x0 + 5,
   
   [s](x0) = x0,
   
   [mark](x0) = 4x0,
   
   [a__incr](x0) = 6x0,
   
   [a__odds] = 0,
   
   [odds] = 0,
   
   [a__pairs] = 0,
   
   [cons](x0, x1) = 3x0 + 2x1,
   
   [incr](x0) = 6x0,
   
   [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)) = 18X + 12XS >= 12X + 12XS = cons(s(mark(X)),incr(XS))
   
   a__head(cons(X,XS)) = 9X + 6XS + 5 >= 4X = mark(X)
   
   a__tail(cons(X,XS)) = 6X + 4XS + 2 >= 4XS = mark(XS)
   
   mark(nats()) = 0 >= 0 = a__nats()
   
   mark(pairs()) = 0 >= 0 = a__pairs()
   
   mark(odds()) = 0 >= 0 = a__odds()
   
   mark(incr(X)) = 24X >= 24X = a__incr(mark(X))
   
   mark(head(X)) = 12X + 16 >= 12X + 5 = a__head(mark(X))
   
   mark(tail(X)) = 8X + 8 >= 8X + 2 = a__tail(mark(X))
   
   mark(0()) = 0 >= 0 = 0()
   
   mark(s(X)) = 4X >= 4X = s(mark(X))
   
   mark(nil()) = 0 >= 0 = nil()
   
   mark(cons(X1,X2)) = 12X1 + 8X2 >= 12X1 + 2X2 = cons(mark(X1),X2)
   
   a__nats() = 0 >= 0 = nats()
   
   a__pairs() = 0 >= 0 = pairs()
   
   a__odds() = 0 >= 0 = odds()
   
   a__incr(X) = 6X >= 6X = incr(X)
   
   a__head(X) = 3X + 5 >= 3X + 4 = head(X)
   
   a__tail(X) = 2X + 2 >= 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(pairs()) -> a__pairs()
   mark(odds()) -> a__odds()
   mark(incr(X)) -> a__incr(mark(X))
   mark(0()) -> 0()
   mark(s(X)) -> s(mark(X))
   mark(nil()) -> nil()
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   a__nats() -> nats()
   a__pairs() -> pairs()
   a__odds() -> odds()
   a__incr(X) -> incr(X)
   a__tail(X) -> tail(X)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [nil] = 4,
    
    [tail](x0) = 2x0,
    
    [pairs] = 0,
    
    [a__tail](x0) = 2x0 + 4,
    
    [s](x0) = 4x0,
    
    [mark](x0) = x0,
    
    [a__incr](x0) = 4x0,
    
    [a__odds] = 0,
    
    [odds] = 0,
    
    [a__pairs] = 0,
    
    [cons](x0, x1) = 4x0 + x1,
    
    [incr](x0) = 4x0,
    
    [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)) = 16X + 4XS >= 16X + 4XS = cons(s(mark(X)),incr(XS))
    
    mark(nats()) = 0 >= 0 = a__nats()
    
    mark(pairs()) = 0 >= 0 = a__pairs()
    
    mark(odds()) = 0 >= 0 = a__odds()
    
    mark(incr(X)) = 4X >= 4X = a__incr(mark(X))
    
    mark(0()) = 0 >= 0 = 0()
    
    mark(s(X)) = 4X >= 4X = s(mark(X))
    
    mark(nil()) = 4 >= 4 = nil()
    
    mark(cons(X1,X2)) = 4X1 + X2 >= 4X1 + X2 = cons(mark(X1),X2)
    
    a__nats() = 0 >= 0 = nats()
    
    a__pairs() = 0 >= 0 = pairs()
    
    a__odds() = 0 >= 0 = odds()
    
    a__incr(X) = 4X >= 4X = incr(X)
    
    a__tail(X) = 2X + 4 >= 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(pairs()) -> a__pairs()
    mark(odds()) -> a__odds()
    mark(incr(X)) -> a__incr(mark(X))
    mark(0()) -> 0()
    mark(s(X)) -> s(mark(X))
    mark(nil()) -> nil()
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    a__nats() -> nats()
    a__pairs() -> pairs()
    a__odds() -> odds()
    a__incr(X) -> incr(X)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [nil] = 3,
     
     [pairs] = 0,
     
     [s](x0) = 2x0,
     
     [mark](x0) = 2x0,
     
     [a__incr](x0) = 4x0,
     
     [a__odds] = 0,
     
     [odds] = 0,
     
     [a__pairs] = 0,
     
     [cons](x0, x1) = x0 + 4x1,
     
     [incr](x0) = 4x0,
     
     [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 + 16XS >= 4X + 16XS = cons(s(mark(X)),incr(XS))
     
     mark(nats()) = 0 >= 0 = a__nats()
     
     mark(pairs()) = 0 >= 0 = a__pairs()
     
     mark(odds()) = 0 >= 0 = a__odds()
     
     mark(incr(X)) = 8X >= 8X = a__incr(mark(X))
     
     mark(0()) = 0 >= 0 = 0()
     
     mark(s(X)) = 4X >= 4X = s(mark(X))
     
     mark(nil()) = 6 >= 3 = nil()
     
     mark(cons(X1,X2)) = 2X1 + 8X2 >= 2X1 + 4X2 = cons(mark(X1),X2)
     
     a__nats() = 0 >= 0 = nats()
     
     a__pairs() = 0 >= 0 = pairs()
     
     a__odds() = 0 >= 0 = odds()
     
     a__incr(X) = 4X >= 4X = incr(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(pairs()) -> a__pairs()
     mark(odds()) -> a__odds()
     mark(incr(X)) -> a__incr(mark(X))
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     a__nats() -> nats()
     a__pairs() -> pairs()
     a__odds() -> odds()
     a__incr(X) -> incr(X)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [pairs] = 0,
      
      [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] = 2,
      
      [0] = 0,
      
      [a__nats] = 4
     orientation:
      a__nats() = 4 >= 4 = 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))
      
      mark(nats()) = 4 >= 4 = a__nats()
      
      mark(pairs()) = 0 >= 0 = a__pairs()
      
      mark(odds()) = 0 >= 0 = a__odds()
      
      mark(incr(X)) = 4X >= 4X = a__incr(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = 2X >= 2X = s(mark(X))
      
      mark(cons(X1,X2)) = 8X1 + 2X2 >= 8X1 + X2 = cons(mark(X1),X2)
      
      a__nats() = 4 >= 2 = nats()
      
      a__pairs() = 0 >= 0 = pairs()
      
      a__odds() = 0 >= 0 = odds()
      
      a__incr(X) = 2X >= 2X = incr(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(pairs()) -> a__pairs()
      mark(odds()) -> a__odds()
      mark(incr(X)) -> a__incr(mark(X))
      mark(0()) -> 0()
      mark(s(X)) -> s(mark(X))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      a__pairs() -> pairs()
      a__odds() -> odds()
      a__incr(X) -> incr(X)
     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#(pairs()) -> a__pairs#()
       mark#(odds()) -> a__odds#()
       mark#(incr(X)) -> mark#(X)
       mark#(incr(X)) -> a__incr#(mark(X))
       mark#(s(X)) -> mark#(X)
       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(pairs()) -> a__pairs()
       mark(odds()) -> a__odds()
       mark(incr(X)) -> a__incr(mark(X))
       mark(0()) -> 0()
       mark(s(X)) -> s(mark(X))
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       a__pairs() -> pairs()
       a__odds() -> odds()
       a__incr(X) -> incr(X)
      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#(pairs()) -> a__pairs#()
        mark#(odds()) -> a__odds#()
        mark#(incr(X)) -> mark#(X)
        mark#(incr(X)) -> a__incr#(mark(X))
        mark#(s(X)) -> mark#(X)
        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(pairs()) -> a__pairs()
        mark(odds()) -> a__odds()
        mark(incr(X)) -> a__incr(mark(X))
        mark(0()) -> 0()
        mark(s(X)) -> s(mark(X))
        mark(cons(X1,X2)) -> cons(mark(X1),X2)
        a__pairs() -> pairs()
        a__odds() -> odds()
        a__incr(X) -> incr(X)
       graph:
        mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
        mark#(s(X)) -> mark#(X) -> mark#(s(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#(s(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
        mark#(s(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
        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#(cons(X1,X2)) -> mark#(X1)
        mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(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)
        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#(nats()) -> a__nats#()
        mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
        mark#(incr(X)) -> mark#(X) -> mark#(s(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)) -> mark#(X) -> mark#(odds()) -> a__odds#()
        mark#(incr(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
        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#(cons(X1,X2)) -> mark#(X1)
        a__incr#(cons(X,XS)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
        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#(odds()) -> a__odds#()
        a__incr#(cons(X,XS)) -> mark#(X) ->
        mark#(pairs()) -> a__pairs#()
        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: 7
        #arcs: 32/100
        DPs:
         mark#(s(X)) -> mark#(X)
         mark#(odds()) -> a__odds#()
         a__odds#() -> a__incr#(a__pairs())
         a__incr#(cons(X,XS)) -> mark#(X)
         mark#(incr(X)) -> mark#(X)
         mark#(incr(X)) -> a__incr#(mark(X))
         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(pairs()) -> a__pairs()
         mark(odds()) -> a__odds()
         mark(incr(X)) -> a__incr(mark(X))
         mark(0()) -> 0()
         mark(s(X)) -> s(mark(X))
         mark(cons(X1,X2)) -> cons(mark(X1),X2)
         a__pairs() -> pairs()
         a__odds() -> odds()
         a__incr(X) -> incr(X)
        Bounds Processor:
         bound: 0
         enrichment: match-dp
         automaton:
          final states: {4}
          transitions:
           mark{#,0}(18) -> 4*
           incr0(16) -> 17*
           pairs0() -> 5*
           odds0() -> 16*
           cons0(18,17) -> 5*
           a__incr{#,0}(5) -> 4*
           00() -> 18*
           a__pairs0() -> 5*
         problem:
          DPs:
           mark#(s(X)) -> mark#(X)
           mark#(odds()) -> a__odds#()
           a__incr#(cons(X,XS)) -> mark#(X)
           mark#(incr(X)) -> mark#(X)
           mark#(incr(X)) -> a__incr#(mark(X))
           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(pairs()) -> a__pairs()
           mark(odds()) -> a__odds()
           mark(incr(X)) -> a__incr(mark(X))
           mark(0()) -> 0()
           mark(s(X)) -> s(mark(X))
           mark(cons(X1,X2)) -> cons(mark(X1),X2)
           a__pairs() -> pairs()
           a__odds() -> odds()
           a__incr(X) -> incr(X)
         SCC Processor:
          #sccs: 1
          #rules: 5
          #arcs: 23/36
          DPs:
           mark#(s(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)
          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(pairs()) -> a__pairs()
           mark(odds()) -> a__odds()
           mark(incr(X)) -> a__incr(mark(X))
           mark(0()) -> 0()
           mark(s(X)) -> s(mark(X))
           mark(cons(X1,X2)) -> cons(mark(X1),X2)
           a__pairs() -> pairs()
           a__odds() -> odds()
           a__incr(X) -> incr(X)
          Semantic Labeling Processor:
           dimension: 1
           usable rules:
            
           interpretation:
            [pairs] = 0,
            
            [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#
             s
             incr
             a__incr#
             mark
             cons
             a__nats
             0
             nats
             a__pairs
             odds
             a__odds
             a__incr
             pairs
            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) = 0
             pi(s) = []
             pi(pairs) = []
             pi(a__incr#) = []
             pi(mark#) = []
           precedence:
            mark# > a__incr# ~ pairs ~ s ~ mark ~ a__incr ~ a__odds ~ 
            odds ~ a__pairs ~ cons ~ incr ~ nats ~ 0 ~ a__nats
           problem:
            DPs:
             mark#(s(X)) -> mark#(X)
             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(pairs()) -> a__pairs()
             mark(odds()) -> a__odds()
             mark(incr(X)) -> a__incr(mark(X))
             mark(0()) -> 0()
             mark(s(X)) -> s(mark(X))
             mark(cons(X1,X2)) -> cons(mark(X1),X2)
             a__pairs() -> pairs()
             a__odds() -> odds()
             a__incr(X) -> incr(X)
           Restore Modifier:
            DPs:
             mark#(s(X)) -> mark#(X)
             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(pairs()) -> a__pairs()
             mark(odds()) -> a__odds()
             mark(incr(X)) -> a__incr(mark(X))
             mark(0()) -> 0()
             mark(s(X)) -> s(mark(X))
             mark(cons(X1,X2)) -> cons(mark(X1),X2)
             a__pairs() -> pairs()
             a__odds() -> odds()
             a__incr(X) -> incr(X)
            Bounds Processor:
             bound: 0
             enrichment: match-dp
             automaton:
              final states: {3}
              transitions:
               f790() -> 4*
               mark{#,0}(4) -> 3*
             problem:
              DPs:
               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(pairs()) -> a__pairs()
               mark(odds()) -> a__odds()
               mark(incr(X)) -> a__incr(mark(X))
               mark(0()) -> 0()
               mark(s(X)) -> s(mark(X))
               mark(cons(X1,X2)) -> cons(mark(X1),X2)
               a__pairs() -> pairs()
               a__odds() -> odds()
               a__incr(X) -> incr(X)
             Bounds Processor:
              bound: 0
              enrichment: match-dp
              automaton:
               final states: {1}
               transitions:
                mark{#,0}(2) -> 1*
                f810() -> 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(pairs()) -> a__pairs()
                mark(odds()) -> a__odds()
                mark(incr(X)) -> a__incr(mark(X))
                mark(0()) -> 0()
                mark(s(X)) -> s(mark(X))
                mark(cons(X1,X2)) -> cons(mark(X1),X2)
                a__pairs() -> pairs()
                a__odds() -> odds()
                a__incr(X) -> incr(X)
              Qed