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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [make](x0) = x0 + 1,
     
     [.](x0, x1) = x0 + x1,
     
     [++](x0, x1) = x0 + x1,
     
     [rev](x0) = x0,
     
     [nil] = 0
    orientation:
     rev(nil()) = 0 >= 0 = nil()
     
     rev(rev(x)) = x >= x = x
     
     rev(++(x,y)) = x + y >= x + y = ++(rev(y),rev(x))
     
     ++(nil(),y) = y >= y = y
     
     ++(x,nil()) = x >= x = x
     
     ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
     
     ++(x,++(y,z)) = x + y + z >= x + y + z = ++(++(x,y),z)
     
     make(x) = x + 1 >= x = .(x,nil())
    problem:
     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)
     weak:
      make(x) -> .(x,nil())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [make](x0) = x0 + 1,
       
       [.](x0, x1) = x0 + x1,
       
       [++](x0, x1) = x0 + x1,
       
       [rev](x0) = x0,
       
       [nil] = 1
      orientation:
       rev(nil()) = 1 >= 1 = nil()
       
       rev(rev(x)) = x >= x = x
       
       rev(++(x,y)) = x + y >= x + y = ++(rev(y),rev(x))
       
       ++(nil(),y) = y + 1 >= y = y
       
       ++(x,nil()) = x + 1 >= x = x
       
       ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
       
       ++(x,++(y,z)) = x + y + z >= x + y + z = ++(++(x,y),z)
       
       make(x) = x + 1 >= x + 1 = .(x,nil())
      problem:
       strict:
        rev(nil()) -> nil()
        rev(rev(x)) -> x
        rev(++(x,y)) -> ++(rev(y),rev(x))
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(x,++(y,z)) -> ++(++(x,y),z)
       weak:
        ++(nil(),y) -> y
        ++(x,nil()) -> x
        make(x) -> .(x,nil())
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [make](x0) = x0,
         
         [.](x0, x1) = x0 + x1,
         
         [++](x0, x1) = x0 + x1 + 1,
         
         [rev](x0) = x0 + 1,
         
         [nil] = 0
        orientation:
         rev(nil()) = 1 >= 0 = nil()
         
         rev(rev(x)) = x + 2 >= x = x
         
         rev(++(x,y)) = x + y + 2 >= x + y + 3 = ++(rev(y),rev(x))
         
         ++(.(x,y),z) = x + y + z + 1 >= x + y + z + 1 = .(x,++(y,z))
         
         ++(x,++(y,z)) = x + y + z + 2 >= x + y + z + 2 = ++(++(x,y),z)
         
         ++(nil(),y) = y + 1 >= y = y
         
         ++(x,nil()) = x + 1 >= x = x
         
         make(x) = x >= x = .(x,nil())
        problem:
         strict:
          rev(++(x,y)) -> ++(rev(y),rev(x))
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(x,++(y,z)) -> ++(++(x,y),z)
         weak:
          rev(nil()) -> nil()
          rev(rev(x)) -> x
          ++(nil(),y) -> y
          ++(x,nil()) -> x
          make(x) -> .(x,nil())
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                        [1 0]     [1]
           [make](x0) = [0 0]x0 + [0],
           
                         [1 0]     [1 0]     [1]
           [.](x0, x1) = [0 0]x0 + [0 0]x1 + [0],
           
                                    [0]
           [++](x0, x1) = x0 + x1 + [1],
           
                       [1 1]  
           [rev](x0) = [0 1]x0,
           
                   [0]
           [nil] = [0]
          orientation:
                          [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]                    
           rev(++(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = ++(rev(y),rev(x))
           
                          [1 0]    [1 0]        [1]    [1 0]    [1 0]    [1 0]    [1]               
           ++(.(x,y),z) = [0 0]x + [0 0]y + z + [1] >= [0 0]x + [0 0]y + [0 0]z + [0] = .(x,++(y,z))
           
                                       [0]                [0]                
           ++(x,++(y,z)) = x + y + z + [2] >= x + y + z + [2] = ++(++(x,y),z)
           
                        [0]    [0]        
           rev(nil()) = [0] >= [0] = nil()
           
                         [1 2]          
           rev(rev(x)) = [0 1]x >= x = x
           
                             [0]         
           ++(nil(),y) = y + [1] >= y = y
           
                             [0]         
           ++(x,nil()) = x + [1] >= x = x
           
                     [1 0]    [1]    [1 0]    [1]             
           make(x) = [0 0]x + [0] >= [0 0]x + [0] = .(x,nil())
          problem:
           strict:
            ++(.(x,y),z) -> .(x,++(y,z))
            ++(x,++(y,z)) -> ++(++(x,y),z)
           weak:
            rev(++(x,y)) -> ++(rev(y),rev(x))
            rev(nil()) -> nil()
            rev(rev(x)) -> x
            ++(nil(),y) -> y
            ++(x,nil()) -> x
            make(x) -> .(x,nil())
          Open