MAYBE

Problem:
 flatten(nil()) -> nil()
 flatten(unit(x)) -> flatten(x)
 flatten(++(x,y)) -> ++(flatten(x),flatten(y))
 flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
 flatten(flatten(x)) -> flatten(x)
 rev(nil()) -> nil()
 rev(unit(x)) -> unit(x)
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(rev(x)) -> x
 ++(x,nil()) -> x
 ++(nil(),y) -> y
 ++(++(x,y),z) -> ++(x,++(y,z))

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