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:
 RT 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
   interpretation:
    [false] = 0,
    
    [true] = 0,
    
    [null](x0) = x0 + 15,
    
    [cdr](x0) = x0 + 11,
    
    [car](x0) = x0 + 19,
    
    [++](x0, x1) = x0 + x1 + 20,
    
    [.](x0, x1) = x0 + x1 + 9,
    
    [rev](x0) = x0 + 29,
    
    [nil] = 1
   orientation:
    rev(nil()) = 30 >= 1 = nil()
    
    rev(.(x,y)) = x + y + 38 >= x + y + 59 = ++(rev(y),.(x,nil()))
    
    car(.(x,y)) = x + y + 28 >= x = x
    
    cdr(.(x,y)) = x + y + 20 >= y = y
    
    null(nil()) = 16 >= 0 = true()
    
    null(.(x,y)) = x + y + 24 >= 0 = false()
    
    ++(nil(),y) = y + 21 >= y = y
    
    ++(.(x,y),z) = x + y + z + 29 >= x + y + z + 29 = .(x,++(y,z))
   problem:
    strict:
     rev(.(x,y)) -> ++(rev(y),.(x,nil()))
     ++(.(x,y),z) -> .(x,++(y,z))
    weak:
     rev(nil()) -> nil()
     car(.(x,y)) -> x
     cdr(.(x,y)) -> y
     null(nil()) -> true()
     null(.(x,y)) -> false()
     ++(nil(),y) -> y
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [0]
     [false] = [0],
     
              [0]
     [true] = [0],
     
                  [1 0]     [12]
     [null](x0) = [0 0]x0 + [12],
     
                 [1 2]  
     [cdr](x0) = [0 1]x0,
     
                 [1 5]  
     [car](x0) = [0 1]x0,
     
                           
     [++](x0, x1) = x0 + x1,
     
                   [1 8]          [4]
     [.](x0, x1) = [0 1]x0 + x1 + [4],
     
                 [1 4]     [0]
     [rev](x0) = [0 1]x0 + [1],
     
             [7]
     [nil] = [0]
    orientation:
                   [1  12]    [1 4]    [20]    [1 8]    [1 4]    [11]                        
     rev(.(x,y)) = [0  1 ]x + [0 1]y + [5 ] >= [0 1]x + [0 1]y + [5 ] = ++(rev(y),.(x,nil()))
     
                    [1 8]            [4]    [1 8]            [4]               
     ++(.(x,y),z) = [0 1]x + y + z + [4] >= [0 1]x + y + z + [4] = .(x,++(y,z))
     
                  [7]    [7]        
     rev(nil()) = [1] >= [0] = nil()
     
                   [1  13]    [1 5]    [24]         
     car(.(x,y)) = [0  1 ]x + [0 1]y + [4 ] >= x = x
     
                   [1  10]    [1 2]    [12]         
     cdr(.(x,y)) = [0  1 ]x + [0 1]y + [4 ] >= y = y
     
                   [19]    [0]         
     null(nil()) = [12] >= [0] = true()
     
                    [1 8]    [1 0]    [16]    [0]          
     null(.(x,y)) = [0 0]x + [0 0]y + [12] >= [0] = false()
     
                       [7]         
     ++(nil(),y) = y + [0] >= y = y
    problem:
     strict:
      ++(.(x,y),z) -> .(x,++(y,z))
     weak:
      rev(.(x,y)) -> ++(rev(y),.(x,nil()))
      rev(nil()) -> nil()
      car(.(x,y)) -> x
      cdr(.(x,y)) -> y
      null(nil()) -> true()
      null(.(x,y)) -> false()
      ++(nil(),y) -> y
    Open