MAYBE

Problem:
 rev(nil()) -> nil()
 rev(.(x,y)) -> ++(rev(y),.(x,nil()))
 car(.(x,y)) -> x
 cdr(.(x,y)) -> y
 null(nil()) -> true()
 null(.(x,y)) -> false()
 ++(nil(),y) -> y
 ++(.(x,y),z) -> .(x,++(y,z))

Proof:
 Complexity Transformation Processor:
  strict:
   rev(nil()) -> nil()
   rev(.(x,y)) -> ++(rev(y),.(x,nil()))
   car(.(x,y)) -> x
   cdr(.(x,y)) -> y
   null(nil()) -> true()
   null(.(x,y)) -> false()
   ++(nil(),y) -> y
   ++(.(x,y),z) -> .(x,++(y,z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [false] = 0,
     
     [true] = 0,
     
     [null](x0) = x0,
     
     [cdr](x0) = x0,
     
     [car](x0) = x0,
     
     [++](x0, x1) = x0 + x1,
     
     [.](x0, x1) = x0 + x1,
     
     [rev](x0) = x0 + 1,
     
     [nil] = 1
    orientation:
     rev(nil()) = 2 >= 1 = nil()
     
     rev(.(x,y)) = x + y + 1 >= x + y + 2 = ++(rev(y),.(x,nil()))
     
     car(.(x,y)) = x + y >= x = x
     
     cdr(.(x,y)) = x + y >= y = y
     
     null(nil()) = 1 >= 0 = true()
     
     null(.(x,y)) = x + y >= 0 = false()
     
     ++(nil(),y) = y + 1 >= y = y
     
     ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
    problem:
     strict:
      rev(.(x,y)) -> ++(rev(y),.(x,nil()))
      car(.(x,y)) -> x
      cdr(.(x,y)) -> y
      null(.(x,y)) -> false()
      ++(.(x,y),z) -> .(x,++(y,z))
     weak:
      rev(nil()) -> nil()
      null(nil()) -> true()
      ++(nil(),y) -> y
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [false] = 0,
       
       [true] = 0,
       
       [null](x0) = x0 + 1,
       
       [cdr](x0) = x0,
       
       [car](x0) = x0,
       
       [++](x0, x1) = x0 + x1,
       
       [.](x0, x1) = x0 + x1,
       
       [rev](x0) = x0,
       
       [nil] = 0
      orientation:
       rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
       
       car(.(x,y)) = x + y >= x = x
       
       cdr(.(x,y)) = x + y >= y = y
       
       null(.(x,y)) = x + y + 1 >= 0 = false()
       
       ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
       
       rev(nil()) = 0 >= 0 = nil()
       
       null(nil()) = 1 >= 0 = true()
       
       ++(nil(),y) = y >= y = y
      problem:
       strict:
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        car(.(x,y)) -> x
        cdr(.(x,y)) -> y
        ++(.(x,y),z) -> .(x,++(y,z))
       weak:
        null(.(x,y)) -> false()
        rev(nil()) -> nil()
        null(nil()) -> true()
        ++(nil(),y) -> y
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [false] = 0,
         
         [true] = 0,
         
         [null](x0) = x0,
         
         [cdr](x0) = x0 + 1,
         
         [car](x0) = x0,
         
         [++](x0, x1) = x0 + x1,
         
         [.](x0, x1) = x0 + x1,
         
         [rev](x0) = x0,
         
         [nil] = 0
        orientation:
         rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
         
         car(.(x,y)) = x + y >= x = x
         
         cdr(.(x,y)) = x + y + 1 >= y = y
         
         ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
         
         null(.(x,y)) = x + y >= 0 = false()
         
         rev(nil()) = 0 >= 0 = nil()
         
         null(nil()) = 0 >= 0 = true()
         
         ++(nil(),y) = y >= y = y
        problem:
         strict:
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          car(.(x,y)) -> x
          ++(.(x,y),z) -> .(x,++(y,z))
         weak:
          cdr(.(x,y)) -> y
          null(.(x,y)) -> false()
          rev(nil()) -> nil()
          null(nil()) -> true()
          ++(nil(),y) -> y
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [false] = 0,
           
           [true] = 0,
           
           [null](x0) = x0,
           
           [cdr](x0) = x0,
           
           [car](x0) = x0 + 1,
           
           [++](x0, x1) = x0 + x1,
           
           [.](x0, x1) = x0 + x1,
           
           [rev](x0) = x0,
           
           [nil] = 0
          orientation:
           rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
           
           car(.(x,y)) = x + y + 1 >= x = x
           
           ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
           
           cdr(.(x,y)) = x + y >= y = y
           
           null(.(x,y)) = x + y >= 0 = false()
           
           rev(nil()) = 0 >= 0 = nil()
           
           null(nil()) = 0 >= 0 = true()
           
           ++(nil(),y) = y >= y = y
          problem:
           strict:
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            ++(.(x,y),z) -> .(x,++(y,z))
           weak:
            car(.(x,y)) -> x
            cdr(.(x,y)) -> y
            null(.(x,y)) -> false()
            rev(nil()) -> nil()
            null(nil()) -> true()
            ++(nil(),y) -> y
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                       [0]
             [false] = [1],
             
                      [0]
             [true] = [0],
             
                            
             [null](x0) = x0,
             
                           
             [cdr](x0) = x0,
             
                         [1 1]  
             [car](x0) = [0 1]x0,
             
                                   
             [++](x0, x1) = x0 + x1,
             
                                     [1]
             [.](x0, x1) = x0 + x1 + [1],
             
                         [1 1]  
             [rev](x0) = [0 1]x0,
             
                     [0]
             [nil] = [0]
            orientation:
                           [1 1]    [1 1]    [2]        [1 1]    [1]                        
             rev(.(x,y)) = [0 1]x + [0 1]y + [1] >= x + [0 1]y + [1] = ++(rev(y),.(x,nil()))
             
                                        [1]                [1]               
             ++(.(x,y),z) = x + y + z + [1] >= x + y + z + [1] = .(x,++(y,z))
             
                           [1 1]    [1 1]    [2]         
             car(.(x,y)) = [0 1]x + [0 1]y + [1] >= x = x
             
                                   [1]         
             cdr(.(x,y)) = x + y + [1] >= y = y
             
                                    [1]    [0]          
             null(.(x,y)) = x + y + [1] >= [1] = false()
             
                          [0]    [0]        
             rev(nil()) = [0] >= [0] = nil()
             
                           [0]    [0]         
             null(nil()) = [0] >= [0] = true()
             
                                     
             ++(nil(),y) = y >= y = y
            problem:
             strict:
              ++(.(x,y),z) -> .(x,++(y,z))
             weak:
              rev(.(x,y)) -> ++(rev(y),.(x,nil()))
              car(.(x,y)) -> x
              cdr(.(x,y)) -> y
              null(.(x,y)) -> false()
              rev(nil()) -> nil()
              null(nil()) -> true()
              ++(nil(),y) -> y
            Open