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:
 DP Processor:
  DPs:
   top#(sent(x)) -> rest#(x)
   top#(sent(x)) -> check#(rest(x))
   top#(sent(x)) -> top#(check(rest(x)))
   check#(sent(x)) -> check#(x)
   check#(rest(x)) -> check#(x)
   check#(rest(x)) -> rest#(check(x))
   check#(cons(x,y)) -> check#(x)
   check#(cons(x,y)) -> check#(y)
  TRS:
   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)
  Matrix Interpretation Processor: dim=4
   
   interpretation:
    [check#](x0) = [0 1 0 1]x0,
    
    [rest#](x0) = [0 0 0 1]x0,
    
    [top#](x0) = [1 0 0 0]x0 + [1],
    
                     [0 0 0 0]     [0 1 1 1]     [1]
                     [0 1 0 1]     [0 1 1 1]     [1]
    [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
                     [0 0 0 0]     [0 0 0 0]     [0],
    
            [1]
            [0]
    [nil] = [1]
            [0],
    
                  [0 1 0 0]  
                  [0 1 0 0]  
    [check](x0) = [0 0 0 0]x0
                  [0 0 0 1]  ,
    
                 [1 0 1 0]     [0]
                 [0 1 1 0]     [0]
    [rest](x0) = [0 0 0 0]x0 + [0]
                 [0 0 0 1]     [1],
    
                [1]
                [1]
    [top](x0) = [0]
                [1],
    
                 [0 1 1 1]     [1]
                 [0 1 0 1]     [1]
    [sent](x0) = [0 0 0 0]x0 + [0]
                 [0 0 0 0]     [0]
   orientation:
    top#(sent(x)) = [0 1 1 1]x + [2] >= [0 0 0 1]x = rest#(x)
    
    top#(sent(x)) = [0 1 1 1]x + [2] >= [0 1 1 1]x + [1] = check#(rest(x))
    
    top#(sent(x)) = [0 1 1 1]x + [2] >= [0 1 1 0]x + [1] = top#(check(rest(x)))
    
    check#(sent(x)) = [0 1 0 1]x + [1] >= [0 1 0 1]x = check#(x)
    
    check#(rest(x)) = [0 1 1 1]x + [1] >= [0 1 0 1]x = check#(x)
    
    check#(rest(x)) = [0 1 1 1]x + [1] >= [0 0 0 1]x = rest#(check(x))
    
    check#(cons(x,y)) = [0 1 0 1]x + [0 1 1 1]y + [1] >= [0 1 0 1]x = check#(x)
    
    check#(cons(x,y)) = [0 1 0 1]x + [0 1 1 1]y + [1] >= [0 1 0 1]y = check#(y)
    
                   [1]    [1]                      
                   [1]    [1]                      
    top(sent(x)) = [0] >= [0] = top(check(rest(x)))
                   [1]    [1]                      
    
                  [2]    [2]              
                  [1]    [1]              
    rest(nil()) = [0] >= [0] = sent(nil())
                  [1]    [0]              
    
                      [0 0 0 0]    [0 1 1 1]    [1]    [0 1 1 1]    [1]          
                      [0 1 0 1]    [0 1 1 1]    [1]    [0 1 0 1]    [1]          
    rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y + [0] = sent(y)
                      [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [0]          
    
                     [0 1 0 1]    [1]    [0 1 0 1]    [1]                 
                     [0 1 0 1]    [1]    [0 1 0 1]    [1]                 
    check(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = sent(check(x))
                     [0 0 0 0]    [0]    [0 0 0 0]    [0]                 
    
                     [0 1 1 0]    [0]    [0 1 0 0]    [0]                 
                     [0 1 1 0]    [0]    [0 1 0 0]    [0]                 
    check(rest(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = rest(check(x))
                     [0 0 0 1]    [1]    [0 0 0 1]    [1]                 
    
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 0 0 0]    [0 1 1 1]    [1]                   
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 1 0 1]    [0 1 1 1]    [1]                   
    check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(check(x),y)
                       [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
    
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 0 0 0]    [0 1 0 1]    [1]                   
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 1 0 1]    [0 1 0 1]    [1]                   
    check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y))
                       [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
    
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 0 0 0]    [0 1 1 1]    [1]            
                       [0 1 0 1]    [0 1 1 1]    [1]    [0 1 0 1]    [0 1 1 1]    [1]            
    check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,y)
                       [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]            
   problem:
    DPs:
     
    TRS:
     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)
   Qed