MAYBE

Problem:
 rev(nil()) -> nil()
 rev(rev(x)) -> x
 rev(++(x,y)) -> ++(rev(y),rev(x))
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(x,++(y,z)) -> ++(++(x,y),z)
 make(x) -> .(x,nil())

Proof:
 RT Transformation Processor:
  strict:
   rev(nil()) -> nil()
   rev(rev(x)) -> x
   rev(++(x,y)) -> ++(rev(y),rev(x))
   ++(nil(),y) -> y
   ++(x,nil()) -> x
   ++(.(x,y),z) -> .(x,++(y,z))
   ++(x,++(y,z)) -> ++(++(x,y),z)
   make(x) -> .(x,nil())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [make](x0) = x0,
    
    [.](x0, x1) = x0 + x1 + 12,
    
    [++](x0, x1) = x0 + x1 + 19,
    
    [rev](x0) = x0 + 12,
    
    [nil] = 17
   orientation:
    rev(nil()) = 29 >= 17 = nil()
    
    rev(rev(x)) = x + 24 >= x = x
    
    rev(++(x,y)) = x + y + 31 >= x + y + 43 = ++(rev(y),rev(x))
    
    ++(nil(),y) = y + 36 >= y = y
    
    ++(x,nil()) = x + 36 >= x = x
    
    ++(.(x,y),z) = x + y + z + 31 >= x + y + z + 31 = .(x,++(y,z))
    
    ++(x,++(y,z)) = x + y + z + 38 >= x + y + z + 38 = ++(++(x,y),z)
    
    make(x) = x >= x + 29 = .(x,nil())
   problem:
    strict:
     rev(++(x,y)) -> ++(rev(y),rev(x))
     ++(.(x,y),z) -> .(x,++(y,z))
     ++(x,++(y,z)) -> ++(++(x,y),z)
     make(x) -> .(x,nil())
    weak:
     rev(nil()) -> nil()
     rev(rev(x)) -> x
     ++(nil(),y) -> y
     ++(x,nil()) -> x
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [make](x0) = x0 + 25,
     
     [.](x0, x1) = x0 + x1 + 7,
     
     [++](x0, x1) = x0 + x1 + 16,
     
     [rev](x0) = x0,
     
     [nil] = 17
    orientation:
     rev(++(x,y)) = x + y + 16 >= x + y + 16 = ++(rev(y),rev(x))
     
     ++(.(x,y),z) = x + y + z + 23 >= x + y + z + 23 = .(x,++(y,z))
     
     ++(x,++(y,z)) = x + y + z + 32 >= x + y + z + 32 = ++(++(x,y),z)
     
     make(x) = x + 25 >= x + 24 = .(x,nil())
     
     rev(nil()) = 17 >= 17 = nil()
     
     rev(rev(x)) = x >= x = x
     
     ++(nil(),y) = y + 33 >= y = y
     
     ++(x,nil()) = x + 33 >= x = x
    problem:
     strict:
      rev(++(x,y)) -> ++(rev(y),rev(x))
      ++(.(x,y),z) -> .(x,++(y,z))
      ++(x,++(y,z)) -> ++(++(x,y),z)
     weak:
      make(x) -> .(x,nil())
      rev(nil()) -> nil()
      rev(rev(x)) -> x
      ++(nil(),y) -> y
      ++(x,nil()) -> x
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                   [1  11]     [8 ]
      [make](x0) = [0  0 ]x0 + [12],
      
                    [1  10]     [1 0]     [0 ]
      [.](x0, x1) = [0  0 ]x0 + [0 0]x1 + [12],
      
                               [1]
      [++](x0, x1) = x0 + x1 + [2],
      
                  [1  14]  
      [rev](x0) = [0  1 ]x0,
      
              [1]
      [nil] = [0]
     orientation:
                     [1  14]    [1  14]    [29]    [1  14]    [1  14]    [1]                    
      rev(++(x,y)) = [0  1 ]x + [0  1 ]y + [2 ] >= [0  1 ]x + [0  1 ]y + [2] = ++(rev(y),rev(x))
      
                     [1  10]    [1 0]        [1 ]    [1  10]    [1 0]    [1 0]    [1 ]               
      ++(.(x,y),z) = [0  0 ]x + [0 0]y + z + [14] >= [0  0 ]x + [0 0]y + [0 0]z + [12] = .(x,++(y,z))
      
                                  [2]                [2]                
      ++(x,++(y,z)) = x + y + z + [4] >= x + y + z + [4] = ++(++(x,y),z)
      
                [1  11]    [8 ]    [1  10]    [1 ]             
      make(x) = [0  0 ]x + [12] >= [0  0 ]x + [12] = .(x,nil())
      
                   [1]    [1]        
      rev(nil()) = [0] >= [0] = nil()
      
                    [1  28]          
      rev(rev(x)) = [0  1 ]x >= x = x
      
                        [2]         
      ++(nil(),y) = y + [2] >= y = y
      
                        [2]         
      ++(x,nil()) = x + [2] >= x = x
     problem:
      strict:
       ++(.(x,y),z) -> .(x,++(y,z))
       ++(x,++(y,z)) -> ++(++(x,y),z)
      weak:
       rev(++(x,y)) -> ++(rev(y),rev(x))
       make(x) -> .(x,nil())
       rev(nil()) -> nil()
       rev(rev(x)) -> x
       ++(nil(),y) -> y
       ++(x,nil()) -> x
     Open