YES

Problem:
 rec[append_0][2](Nil(),Cons(x6,Nil())) -> Cons(x6,Nil())
 rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) -> Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
 rec[rev_0][1](Nil()) -> Nil()
 rec[rev_0][1](Cons(x5,x3)) -> rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
 main(x1) -> rec[rev_0][1](x1)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [main](x0) = x0 + 1,
   
   [rec[rev_0][1]](x0) = x0,
   
   [rec[append_0][2]](x0, x1) = x0 + x1,
   
   [Cons](x0, x1) = x0 + x1 + 2,
   
   [Nil] = 0
  orientation:
   rec[append_0][2](Nil(),Cons(x6,Nil())) = x6 + 2 >= x6 + 2 = Cons(x6,Nil())
   
   rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) = x10 + x14 + x6 + 4 >= x10 + x14 + x6 + 4 = Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
   
   rec[rev_0][1](Nil()) = 0 >= 0 = Nil()
   
   rec[rev_0][1](Cons(x5,x3)) = x3 + x5 + 2 >= x3 + x5 + 2 = rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
   
   main(x1) = x1 + 1 >= x1 = rec[rev_0][1](x1)
  problem:
   rec[append_0][2](Nil(),Cons(x6,Nil())) -> Cons(x6,Nil())
   rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) -> Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
   rec[rev_0][1](Nil()) -> Nil()
   rec[rev_0][1](Cons(x5,x3)) -> rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
                          [1 1 1]  
    [rec[rev_0][1]](x0) = [1 1 0]x0
                          [0 0 1]  ,
    
                                 [1 0 0]     [1 0 0]     [1]
    [rec[append_0][2]](x0, x1) = [0 1 1]x0 + [0 0 0]x1 + [0]
                                 [0 0 0]     [0 0 0]     [1],
    
                     [1 1 0]     [1 0 0]     [0]
    [Cons](x0, x1) = [0 0 0]x0 + [0 1 1]x1 + [0]
                     [0 0 0]     [0 0 0]     [1],
    
            [0]
    [Nil] = [0]
            [0]
   orientation:
                                             [1 1 0]     [1]    [1 1 0]     [0]                 
    rec[append_0][2](Nil(),Cons(x6,Nil())) = [0 0 0]x6 + [0] >= [0 0 0]x6 + [0] = Cons(x6,Nil())
                                             [0 0 0]     [1]    [0 0 0]     [1]                 
    
                                                     [1 0 0]      [1 1 0]      [1 1 0]     [1]    [1 0 0]      [1 1 0]      [1 1 0]     [1]                                                 
    rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) = [0 1 1]x10 + [0 0 0]x14 + [0 0 0]x6 + [1] >= [0 1 1]x10 + [0 0 0]x14 + [0 0 0]x6 + [1] = Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
                                                     [0 0 0]      [0 0 0]      [0 0 0]     [1]    [0 0 0]      [0 0 0]      [0 0 0]     [1]                                                 
    
                           [0]    [0]        
    rec[rev_0][1](Nil()) = [0] >= [0] = Nil()
                           [0]    [0]        
    
                                 [1 1 1]     [1 1 0]     [1]    [1 1 1]     [1 1 0]     [1]                                                     
    rec[rev_0][1](Cons(x5,x3)) = [1 1 1]x3 + [1 1 0]x5 + [0] >= [1 1 1]x3 + [0 0 0]x5 + [0] = rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
                                 [0 0 0]     [0 0 0]     [1]    [0 0 0]     [0 0 0]     [1]                                                     
   problem:
    rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) ->
    Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
    rec[rev_0][1](Nil()) -> Nil()
    rec[rev_0][1](Cons(x5,x3)) -> rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [rec[rev_0][1]](x0) = 4x0 + 1,
     
     [rec[append_0][2]](x0, x1) = x0 + 4x1,
     
     [Cons](x0, x1) = 4x0 + x1 + 2,
     
     [Nil] = 0
    orientation:
     rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) = x10 + 4x14 + 16x6 + 10 >= x10 + 4x14 + 16x6 + 10 = Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
     
     rec[rev_0][1](Nil()) = 1 >= 0 = Nil()
     
     rec[rev_0][1](Cons(x5,x3)) = 4x3 + 16x5 + 9 >= 4x3 + 16x5 + 9 = rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
    problem:
     rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) ->
     Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
     rec[rev_0][1](Cons(x5,x3)) -> rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [rec[rev_0][1]](x0) = 5x0 + 4,
      
      [rec[append_0][2]](x0, x1) = x0 + 2x1 + 1,
      
      [Cons](x0, x1) = 3x0 + x1 + 1,
      
      [Nil] = 0
     orientation:
      rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) = x10 + 3x14 + 6x6 + 4 >= x10 + 3x14 + 6x6 + 4 = Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
      
      rec[rev_0][1](Cons(x5,x3)) = 5x3 + 15x5 + 9 >= 5x3 + 6x5 + 7 = rec[append_0][2](rec[rev_0][1](x3),Cons(x5,Nil()))
     problem:
      rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) ->
      Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
     Matrix Interpretation Processor: dim=3
      
      interpretation:
                                    [1 0 1]     [1 0 0]  
       [rec[append_0][2]](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                                    [1 0 1]     [1 0 0]  ,
       
                        [1 1 0]     [1 0 0]     [0]
       [Cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                        [0 0 0]     [0 1 1]     [1],
       
               [0]
       [Nil] = [0]
               [0]
      orientation:
                                                        [1 1 1]      [1 1 0]      [1 1 0]     [1]    [1 0 1]      [1 1 0]      [1 1 0]     [0]                                                 
       rec[append_0][2](Cons(x14,x10),Cons(x6,Nil())) = [0 0 0]x10 + [0 0 0]x14 + [0 0 0]x6 + [0] >= [0 0 0]x10 + [0 0 0]x14 + [0 0 0]x6 + [0] = Cons(x14,rec[append_0][2](x10,Cons(x6,Nil())))
                                                        [1 1 1]      [1 1 0]      [1 1 0]     [1]    [1 0 1]      [0 0 0]      [1 1 0]     [1]                                                 
      problem:
       
      Qed