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)
  TDG 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)
   graph:
    check#(cons(x,y)) -> check#(y) -> check#(cons(x,y)) -> check#(y)
    check#(cons(x,y)) -> check#(y) -> check#(cons(x,y)) -> check#(x)
    check#(cons(x,y)) -> check#(y) ->
    check#(rest(x)) -> rest#(check(x))
    check#(cons(x,y)) -> check#(y) -> check#(rest(x)) -> check#(x)
    check#(cons(x,y)) -> check#(y) -> check#(sent(x)) -> check#(x)
    check#(cons(x,y)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
    check#(cons(x,y)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
    check#(cons(x,y)) -> check#(x) ->
    check#(rest(x)) -> rest#(check(x))
    check#(cons(x,y)) -> check#(x) -> check#(rest(x)) -> check#(x)
    check#(cons(x,y)) -> check#(x) -> check#(sent(x)) -> check#(x)
    check#(rest(x)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
    check#(rest(x)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
    check#(rest(x)) -> check#(x) -> check#(rest(x)) -> rest#(check(x))
    check#(rest(x)) -> check#(x) -> check#(rest(x)) -> check#(x)
    check#(rest(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
    check#(sent(x)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
    check#(sent(x)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
    check#(sent(x)) -> check#(x) -> check#(rest(x)) -> rest#(check(x))
    check#(sent(x)) -> check#(x) -> check#(rest(x)) -> check#(x)
    check#(sent(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
    top#(sent(x)) -> check#(rest(x)) ->
    check#(cons(x,y)) -> check#(y)
    top#(sent(x)) -> check#(rest(x)) ->
    check#(cons(x,y)) -> check#(x)
    top#(sent(x)) -> check#(rest(x)) ->
    check#(rest(x)) -> rest#(check(x))
    top#(sent(x)) -> check#(rest(x)) ->
    check#(rest(x)) -> check#(x)
    top#(sent(x)) -> check#(rest(x)) ->
    check#(sent(x)) -> check#(x)
    top#(sent(x)) -> top#(check(rest(x))) ->
    top#(sent(x)) -> top#(check(rest(x)))
    top#(sent(x)) -> top#(check(rest(x))) ->
    top#(sent(x)) -> check#(rest(x))
    top#(sent(x)) -> top#(check(rest(x))) -> top#(sent(x)) -> rest#(x)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 28/64
    DPs:
     top#(sent(x)) -> top#(check(rest(x)))
    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=3
     
     interpretation:
      [top#](x0) = [0 0 1]x0,
      
                       [0 0 0]     [0 0 0]     [0]
      [cons](x0, x1) = [1 0 0]x0 + [1 1 0]x1 + [1]
                       [0 0 0]     [1 1 0]     [1],
      
              [1]
      [nil] = [0]
              [1],
      
                    [0 0 0]  
      [check](x0) = [0 1 0]x0
                    [0 1 0]  ,
      
                   [0 0 0]  
      [rest](x0) = [1 1 0]x0
                   [1 0 1]  ,
      
                  [0 0 1]     [1]
      [top](x0) = [0 0 1]x0 + [0]
                  [0 0 0]     [0],
      
                   [0 0 0]     [0]
      [sent](x0) = [0 1 0]x0 + [1]
                   [1 1 0]     [1]
     orientation:
      top#(sent(x)) = [1 1 0]x + [1] >= [1 1 0]x = top#(check(rest(x)))
      
                     [1 1 0]    [2]    [1 1 0]    [1]                      
      top(sent(x)) = [1 1 0]x + [1] >= [1 1 0]x + [0] = top(check(rest(x)))
                     [0 0 0]    [0]    [0 0 0]    [0]                      
      
                    [0]    [0]              
      rest(nil()) = [1] >= [1] = sent(nil())
                    [2]    [2]              
      
                        [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0]          
      rest(cons(x,y)) = [1 0 0]x + [1 1 0]y + [1] >= [0 1 0]y + [1] = sent(y)
                        [0 0 0]    [1 1 0]    [1]    [1 1 0]    [1]          
      
                       [0 0 0]    [0]    [0 0 0]    [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]                 
      
                       [0 0 0]     [0 0 0]                  
      check(rest(x)) = [1 1 0]x >= [0 1 0]x = rest(check(x))
                       [1 1 0]     [0 1 0]                  
      
                         [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0]                   
      check(cons(x,y)) = [1 0 0]x + [1 1 0]y + [1] >= [1 1 0]y + [1] = cons(check(x),y)
                         [1 0 0]    [1 1 0]    [1]    [1 1 0]    [1]                   
      
                         [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                   
      check(cons(x,y)) = [1 0 0]x + [1 1 0]y + [1] >= [1 0 0]x + [0 1 0]y + [1] = cons(x,check(y))
                         [1 0 0]    [1 1 0]    [1]    [0 0 0]    [0 1 0]    [1]                   
      
                         [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]            
      check(cons(x,y)) = [1 0 0]x + [1 1 0]y + [1] >= [1 0 0]x + [1 1 0]y + [1] = cons(x,y)
                         [1 0 0]    [1 1 0]    [1]    [0 0 0]    [1 1 0]    [1]            
     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
    
    DPs:
     check#(cons(x,y)) -> check#(y)
     check#(sent(x)) -> check#(x)
     check#(rest(x)) -> check#(x)
     check#(cons(x,y)) -> check#(x)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(check#) = 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