YES

Problem:
 top(sent(x)) -> top(check(rest(x)))
 rest(nil()) -> sent(nil())
 rest(cons(x,y)) -> sent(y)
 check(sent(x)) -> sent(check(x))
 check(rest(x)) -> rest(check(x))
 check(cons(x,y)) -> cons(check(x),y)
 check(cons(x,y)) -> cons(x,check(y))
 check(cons(x,y)) -> cons(x,y)

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
                    [1 0 0]     [1 0 0]     [1]
   [cons](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0]
                    [0 0 0]     [0 1 0]     [0],
   
           [1]
   [nil] = [0]
           [0],
   
                   
   [check](x0) = x0
                   ,
   
                [1 0 0]  
   [rest](x0) = [0 0 1]x0
                [0 1 0]  ,
   
               [1 1 1]     [1]
   [top](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [0],
   
                  
   [sent](x0) = x0
                  
  orientation:
                  [1 1 1]    [1]    [1 1 1]    [1]                      
   top(sent(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = top(check(rest(x)))
                  [0 0 0]    [0]    [0 0 0]    [0]                      
   
                 [1]    [1]              
   rest(nil()) = [0] >= [0] = sent(nil())
                 [0]    [0]              
   
                     [1 0 0]        [1]               
   rest(cons(x,y)) = [0 0 0]x + y + [0] >= y = sent(y)
                     [0 0 0]        [0]               
   
                                           
   check(sent(x)) = x >= x = sent(check(x))
                                           
   
                    [1 0 0]     [1 0 0]                  
   check(rest(x)) = [0 0 1]x >= [0 0 1]x = rest(check(x))
                    [0 1 0]     [0 1 0]                  
   
                      [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]                   
   check(cons(x,y)) = [0 0 0]x + [0 0 1]y + [0] >= [0 0 0]x + [0 0 1]y + [0] = cons(check(x),y)
                      [0 0 0]    [0 1 0]    [0]    [0 0 0]    [0 1 0]    [0]                   
   
                      [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]                   
   check(cons(x,y)) = [0 0 0]x + [0 0 1]y + [0] >= [0 0 0]x + [0 0 1]y + [0] = cons(x,check(y))
                      [0 0 0]    [0 1 0]    [0]    [0 0 0]    [0 1 0]    [0]                   
   
                      [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]            
   check(cons(x,y)) = [0 0 0]x + [0 0 1]y + [0] >= [0 0 0]x + [0 0 1]y + [0] = cons(x,y)
                      [0 0 0]    [0 1 0]    [0]    [0 0 0]    [0 1 0]    [0]            
  problem:
   top(sent(x)) -> top(check(rest(x)))
   rest(nil()) -> sent(nil())
   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   check(cons(x,y)) -> cons(check(x),y)
   check(cons(x,y)) -> cons(x,check(y))
   check(cons(x,y)) -> cons(x,y)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [cons](x0, x1) = 2x0 + 4x1 + 1,
    
    [nil] = 0,
    
    [check](x0) = 2x0,
    
    [rest](x0) = x0,
    
    [top](x0) = 2x0,
    
    [sent](x0) = 2x0
   orientation:
    top(sent(x)) = 4x >= 4x = top(check(rest(x)))
    
    rest(nil()) = 0 >= 0 = sent(nil())
    
    check(sent(x)) = 4x >= 4x = sent(check(x))
    
    check(rest(x)) = 2x >= 2x = rest(check(x))
    
    check(cons(x,y)) = 4x + 8y + 2 >= 4x + 4y + 1 = cons(check(x),y)
    
    check(cons(x,y)) = 4x + 8y + 2 >= 2x + 8y + 1 = cons(x,check(y))
    
    check(cons(x,y)) = 4x + 8y + 2 >= 2x + 4y + 1 = cons(x,y)
   problem:
    top(sent(x)) -> top(check(rest(x)))
    rest(nil()) -> sent(nil())
    check(sent(x)) -> sent(check(x))
    check(rest(x)) -> rest(check(x))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
             [0]
     [nil] = [1]
             [1],
     
                   [1 0 0]  
     [check](x0) = [0 0 0]x0
                   [0 0 0]  ,
     
                  [1 1 0]  
     [rest](x0) = [0 1 0]x0
                  [0 1 0]  ,
     
                 [1 0 1]     [0]
     [top](x0) = [0 1 0]x0 + [1]
                 [0 0 1]     [0],
     
                  [1 0 0]  
     [sent](x0) = [0 0 1]x0
                  [0 1 0]  
    orientation:
                    [1 1 0]    [0]    [1 1 0]    [0]                      
     top(sent(x)) = [0 0 1]x + [1] >= [0 0 0]x + [1] = top(check(rest(x)))
                    [0 1 0]    [0]    [0 0 0]    [0]                      
     
                   [1]    [0]              
     rest(nil()) = [1] >= [1] = sent(nil())
                   [1]    [1]              
     
                      [1 0 0]     [1 0 0]                  
     check(sent(x)) = [0 0 0]x >= [0 0 0]x = sent(check(x))
                      [0 0 0]     [0 0 0]                  
     
                      [1 1 0]     [1 0 0]                  
     check(rest(x)) = [0 0 0]x >= [0 0 0]x = rest(check(x))
                      [0 0 0]     [0 0 0]                  
    problem:
     top(sent(x)) -> top(check(rest(x)))
     check(sent(x)) -> sent(check(x))
     check(rest(x)) -> rest(check(x))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                    [1 0 1]  
      [check](x0) = [0 1 0]x0
                    [0 1 0]  ,
      
                     
      [rest](x0) = x0
                     ,
      
                  [1 1 0]  
      [top](x0) = [0 0 0]x0
                  [0 0 0]  ,
      
                   [1 0 1]     [0]
      [sent](x0) = [0 1 0]x0 + [1]
                   [0 1 0]     [1]
     orientation:
                     [1 1 1]    [1]    [1 1 1]                       
      top(sent(x)) = [0 0 0]x + [0] >= [0 0 0]x = top(check(rest(x)))
                     [0 0 0]    [0]    [0 0 0]                       
      
                       [1 1 1]    [1]    [1 1 1]    [0]                 
      check(sent(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = sent(check(x))
                       [0 1 0]    [1]    [0 1 0]    [1]                 
      
                       [1 0 1]     [1 0 1]                  
      check(rest(x)) = [0 1 0]x >= [0 1 0]x = rest(check(x))
                       [0 1 0]     [0 1 0]                  
     problem:
      check(rest(x)) -> rest(check(x))
     Matrix Interpretation Processor: dim=3
      
      interpretation:
                     [1 0 1]  
       [check](x0) = [0 0 0]x0
                     [0 0 1]  ,
       
                    [1 0 0]     [0]
       [rest](x0) = [0 0 0]x0 + [0]
                    [0 0 1]     [1]
      orientation:
                        [1 0 1]    [1]    [1 0 1]    [0]                 
       check(rest(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = rest(check(x))
                        [0 0 1]    [1]    [0 0 1]    [1]                 
      problem:
       
      Qed