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 + 1,
     
     [b] = 4,
     
     [rev](x0) = x0 + 6,
     
     [a] = 12
    orientation:
     rev(a()) = 18 >= 12 = a()
     
     rev(b()) = 10 >= 4 = b()
     
     rev(++(x,y)) = x + y + 7 >= x + y + 13 = ++(rev(y),rev(x))
     
     rev(++(x,x)) = 2x + 7 >= x + 6 = rev(x)
    problem:
     strict:
      rev(++(x,y)) -> ++(rev(y),rev(x))
     weak:
      rev(a()) -> a()
      rev(b()) -> b()
      rev(++(x,x)) -> rev(x)
    Matrix Interpretation Processor:
     dimension: 3
     max_matrix:
      [1 1 1]
      [0 1 1]
      [0 0 0]
      interpretation:
                      [1 0 0]     [1 0 1]     [0]
       [++](x0, x1) = [0 1 1]x0 + [0 1 1]x1 + [1]
                      [0 0 0]     [0 0 0]     [0],
       
             [0]
       [b] = [0]
             [0],
       
                   [1 1 0]  
       [rev](x0) = [0 1 1]x0
                   [0 0 0]  ,
       
             [0]
       [a] = [0]
             [0]
      orientation:
                      [1 1 1]    [1 1 2]    [1]    [1 1 0]    [1 1 0]    [0]                    
       rev(++(x,y)) = [0 1 1]x + [0 1 1]y + [1] >= [0 1 1]x + [0 1 1]y + [1] = ++(rev(y),rev(x))
                      [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                    
       
                  [0]    [0]      
       rev(a()) = [0] >= [0] = a()
                  [0]    [0]      
       
                  [0]    [0]      
       rev(b()) = [0] >= [0] = b()
                  [0]    [0]      
       
                      [2 2 3]    [1]    [1 1 0]          
       rev(++(x,x)) = [0 2 2]x + [1] >= [0 1 1]x = rev(x)
                      [0 0 0]    [0]    [0 0 0]          
      problem:
       strict:
        
       weak:
        rev(++(x,y)) -> ++(rev(y),rev(x))
        rev(a()) -> a()
        rev(b()) -> b()
        rev(++(x,x)) -> rev(x)
      Qed