YES(?,O(n^2))

Problem:
 rev(a()) -> a()
 rev(b()) -> b()
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(++(x,x)) -> rev(x)

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