YES(?,O(n^2))

Problem:
 average(s(x),y) -> average(x,s(y))
 average(x,s(s(s(y)))) -> s(average(s(x),y))
 average(0(),0()) -> 0()
 average(0(),s(0())) -> 0()
 average(0(),s(s(0()))) -> s(0())

Proof:
 Complexity Transformation Processor:
  strict:
   average(s(x),y) -> average(x,s(y))
   average(x,s(s(s(y)))) -> s(average(s(x),y))
   average(0(),0()) -> 0()
   average(0(),s(0())) -> 0()
   average(0(),s(s(0()))) -> s(0())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 1,
     
     [average](x0, x1) = x0 + x1,
     
     [s](x0) = x0
    orientation:
     average(s(x),y) = x + y >= x + y = average(x,s(y))
     
     average(x,s(s(s(y)))) = x + y >= x + y = s(average(s(x),y))
     
     average(0(),0()) = 2 >= 1 = 0()
     
     average(0(),s(0())) = 2 >= 1 = 0()
     
     average(0(),s(s(0()))) = 2 >= 1 = s(0())
    problem:
     strict:
      average(s(x),y) -> average(x,s(y))
      average(x,s(s(s(y)))) -> s(average(s(x),y))
     weak:
      average(0(),0()) -> 0()
      average(0(),s(0())) -> 0()
      average(0(),s(s(0()))) -> s(0())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [0] = 0,
       
       [average](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1
      orientation:
       average(s(x),y) = x + y + 1 >= x + y + 1 = average(x,s(y))
       
       average(x,s(s(s(y)))) = x + y + 3 >= x + y + 2 = s(average(s(x),y))
       
       average(0(),0()) = 0 >= 0 = 0()
       
       average(0(),s(0())) = 1 >= 0 = 0()
       
       average(0(),s(s(0()))) = 2 >= 1 = s(0())
      problem:
       strict:
        average(s(x),y) -> average(x,s(y))
       weak:
        average(x,s(s(s(y)))) -> s(average(s(x),y))
        average(0(),0()) -> 0()
        average(0(),s(0())) -> 0()
        average(0(),s(s(0()))) -> s(0())
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
               [0]
         [0] = [0],
         
                             [1 1]       
         [average](x0, x1) = [0 1]x0 + x1,
         
                        [1]
         [s](x0) = x0 + [1]
        orientation:
                           [1 1]        [2]    [1 1]        [1]                  
         average(s(x),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = average(x,s(y))
         
                                 [1 1]        [3]    [1 1]        [3]                     
         average(x,s(s(s(y)))) = [0 1]x + y + [3] >= [0 1]x + y + [2] = s(average(s(x),y))
         
                            [0]    [0]      
         average(0(),0()) = [0] >= [0] = 0()
         
                               [1]    [0]      
         average(0(),s(0())) = [1] >= [0] = 0()
         
                                  [2]    [1]         
         average(0(),s(s(0()))) = [2] >= [1] = s(0())
        problem:
         strict:
          
         weak:
          average(s(x),y) -> average(x,s(y))
          average(x,s(s(s(y)))) -> s(average(s(x),y))
          average(0(),0()) -> 0()
          average(0(),s(0())) -> 0()
          average(0(),s(s(0()))) -> s(0())
        Qed