YES(?,O(n^3))

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:
 Matrix Interpretation Processor:
  dimension: 3
  interpretation:
              [1 2 3]     [0]
   [tl](x0) = [0 1 2]x0 + [0]
              [0 0 1]     [4],
   
              [1 0 4]     [0]
   [hd](x0) = [0 1 2]x0 + [2]
              [0 0 1]     [2],
   
            [2]
   [nats] = [2]
            [3],
   
                 [1 2 3]     [4]
   [a__tl](x0) = [0 1 2]x0 + [2]
                 [0 0 1]     [4],
   
                [1 2 2]     [1]
   [mark](x0) = [0 1 1]x0 + [0]
                [0 0 1]     [1],
   
                 [1 0 5]     [2]
   [a__hd](x0) = [0 1 2]x0 + [2]
                 [0 0 1]     [2],
   
               [1 0 2]     [0]
   [adx](x0) = [0 1 0]x0 + [0]
               [0 0 1]     [4],
   
                     [1]
   [incr](x0) = x0 + [1]
                     [0],
   
             [1 0 2]  
   [s](x0) = [0 0 1]x0
             [0 0 0]  ,
   
                        [2]
   [a__incr](x0) = x0 + [1]
                        [0],
   
                    [1 2 4]       
   [cons](x0, x1) = [0 1 2]x0 + x1
                    [0 0 1]       ,
   
             [0]
   [zeros] = [1]
             [0],
   
         [0]
   [0] = [0]
         [0],
   
                  [1 0 2]     [5]
   [a__adx](x0) = [0 1 0]x0 + [1]
                  [0 0 1]     [4],
   
                [1]
   [a__zeros] = [1]
                [0],
   
               [7]
   [a__nats] = [4]
               [4]
  orientation:
               [7]    [6]                     
   a__nats() = [4] >= [2] = a__adx(a__zeros())
               [4]    [4]                     
   
                [1]    [0]                    
   a__zeros() = [1] >= [1] = cons(0(),zeros())
                [0]    [0]                    
   
                        [1 2 4]        [2]    [1 0 4]        [1]                     
   a__incr(cons(X,Y)) = [0 1 2]X + Y + [1] >= [0 0 1]X + Y + [1] = cons(s(X),incr(Y))
                        [0 0 1]        [0]    [0 0 0]        [0]                     
   
                       [1 2 6]    [1 0 2]    [5]    [1 2 4]    [1 0 2]    [2]                          
   a__adx(cons(X,Y)) = [0 1 2]X + [0 1 0]Y + [1] >= [0 1 2]X + [0 1 0]Y + [1] = a__incr(cons(X,adx(Y)))
                       [0 0 1]    [0 0 1]    [4]    [0 0 1]    [0 0 1]    [4]                          
   
                      [1 2 9]    [1 0 5]    [2]    [1 2 2]    [1]          
   a__hd(cons(X,Y)) = [0 1 4]X + [0 1 2]Y + [2] >= [0 1 1]X + [0] = mark(X)
                      [0 0 1]    [0 0 1]    [2]    [0 0 1]    [1]          
   
                      [1  4  11]    [1 2 3]    [4]    [1 2 2]    [1]          
   a__tl(cons(X,Y)) = [0  1  4 ]X + [0 1 2]Y + [2] >= [0 1 1]Y + [0] = mark(Y)
                      [0  0  1 ]    [0 0 1]    [4]    [0 0 1]    [1]          
   
                  [13]    [7]            
   mark(nats()) = [5 ] >= [4] = a__nats()
                  [4 ]    [4]            
   
                  [1 2 4]    [9]    [1 2 4]    [8]                  
   mark(adx(X)) = [0 1 1]X + [4] >= [0 1 1]X + [1] = a__adx(mark(X))
                  [0 0 1]    [5]    [0 0 1]    [5]                  
   
                   [3]    [1]             
   mark(zeros()) = [1] >= [1] = a__zeros()
                   [1]    [0]             
   
                   [1 2 2]    [4]    [1 2 2]    [3]                   
   mark(incr(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = a__incr(mark(X))
                   [0 0 1]    [1]    [0 0 1]    [1]                   
   
                 [1  2  10]    [9]    [1 2 7]    [8]                 
   mark(hd(X)) = [0  1  3 ]X + [4] >= [0 1 3]X + [4] = a__hd(mark(X))
                 [0  0  1 ]    [3]    [0 0 1]    [3]                 
   
                 [1 4 9]    [9]    [1 4 7]    [8]                 
   mark(tl(X)) = [0 1 3]X + [4] >= [0 1 3]X + [4] = a__tl(mark(X))
                 [0 0 1]    [5]    [0 0 1]    [5]                 
   
                       [1  4  10]     [1 2 2]     [1]    [1 2 4]                     
   mark(cons(X1,X2)) = [0  1  3 ]X1 + [0 1 1]X2 + [0] >= [0 1 2]X1 + X2 = cons(X1,X2)
                       [0  0  1 ]     [0 0 1]     [1]    [0 0 1]                     
   
               [1]    [0]      
   mark(0()) = [0] >= [0] = 0()
               [1]    [0]      
   
                [1 0 4]    [1]    [1 0 2]        
   mark(s(X)) = [0 0 1]X + [0] >= [0 0 1]X = s(X)
                [0 0 0]    [1]    [0 0 0]        
   
               [7]    [2]         
   a__nats() = [4] >= [2] = nats()
               [4]    [3]         
   
               [1 0 2]    [5]    [1 0 2]    [0]         
   a__adx(X) = [0 1 0]X + [1] >= [0 1 0]X + [0] = adx(X)
               [0 0 1]    [4]    [0 0 1]    [4]         
   
                [1]    [0]          
   a__zeros() = [1] >= [1] = zeros()
                [0]    [0]          
   
                    [2]        [1]          
   a__incr(X) = X + [1] >= X + [1] = incr(X)
                    [0]        [0]          
   
              [1 0 5]    [2]    [1 0 4]    [0]        
   a__hd(X) = [0 1 2]X + [2] >= [0 1 2]X + [2] = hd(X)
              [0 0 1]    [2]    [0 0 1]    [2]        
   
              [1 2 3]    [4]    [1 2 3]    [0]        
   a__tl(X) = [0 1 2]X + [2] >= [0 1 2]X + [0] = tl(X)
              [0 0 1]    [4]    [0 0 1]    [4]        
  problem:
   
  Qed