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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
         [6]
   [0] = [6],
   
                       [1 1]          [0 ]
   [average](x0, x1) = [0 1]x0 + x1 + [12],
   
                  [2]
   [s](x0) = x0 + [1]
  orientation:
                     [1 1]        [3 ]    [1 1]        [2 ]                  
   average(s(x),y) = [0 1]x + y + [13] >= [0 1]x + y + [13] = average(x,s(y))
   
                           [1 1]        [6 ]    [1 1]        [5 ]                     
   average(x,s(s(s(y)))) = [0 1]x + y + [15] >= [0 1]x + y + [14] = s(average(s(x),y))
   
                      [18]    [6]      
   average(0(),0()) = [24] >= [6] = 0()
   
                         [20]    [6]      
   average(0(),s(0())) = [25] >= [6] = 0()
   
                            [22]    [8]         
   average(0(),s(s(0()))) = [26] >= [7] = s(0())
  problem:
   
  Qed