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:
 RT 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
   interpretation:
    [0] = 1,
    
    [average](x0, x1) = x0 + x1 + 31,
    
    [s](x0) = x0 + 1
   orientation:
    average(s(x),y) = x + y + 32 >= x + y + 32 = average(x,s(y))
    
    average(x,s(s(s(y)))) = x + y + 34 >= x + y + 33 = s(average(s(x),y))
    
    average(0(),0()) = 33 >= 1 = 0()
    
    average(0(),s(0())) = 34 >= 1 = 0()
    
    average(0(),s(s(0()))) = 35 >= 2 = 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
    interpretation:
           [1]
     [0] = [4],
     
                         [1 2]          [0]
     [average](x0, x1) = [0 1]x0 + x1 + [2],
     
                    [8]
     [s](x0) = x0 + [2]
    orientation:
                       [1 2]        [12]    [1 2]        [8]                  
     average(s(x),y) = [0 1]x + y + [4 ] >= [0 1]x + y + [4] = average(x,s(y))
     
                             [1 2]        [24]    [1 2]        [20]                     
     average(x,s(s(s(y)))) = [0 1]x + y + [8 ] >= [0 1]x + y + [6 ] = s(average(s(x),y))
     
                        [10]    [1]      
     average(0(),0()) = [10] >= [4] = 0()
     
                           [18]    [1]      
     average(0(),s(0())) = [12] >= [4] = 0()
     
                              [26]    [9]         
     average(0(),s(s(0()))) = [14] >= [6] = 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