MAYBE

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)
  Usable Rule 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:
    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)
   EDG 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:
     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#(sent(x)) -> check#(x)
     check#(cons(x,y)) -> check#(y) -> check#(rest(x)) -> check#(x)
     check#(cons(x,y)) -> check#(y) ->
     check#(rest(x)) -> rest#(check(x))
     check#(cons(x,y)) -> check#(y) -> check#(cons(x,y)) -> check#(x)
     check#(cons(x,y)) -> check#(y) -> check#(cons(x,y)) -> check#(y)
     check#(cons(x,y)) -> check#(x) -> check#(sent(x)) -> check#(x)
     check#(cons(x,y)) -> check#(x) -> check#(rest(x)) -> check#(x)
     check#(cons(x,y)) -> check#(x) ->
     check#(rest(x)) -> rest#(check(x))
     check#(cons(x,y)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
     check#(cons(x,y)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
     check#(rest(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
     check#(rest(x)) -> check#(x) -> check#(rest(x)) -> check#(x)
     check#(rest(x)) -> check#(x) -> check#(rest(x)) -> rest#(check(x))
     check#(rest(x)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
     check#(rest(x)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
     check#(sent(x)) -> check#(x) -> check#(sent(x)) -> check#(x)
     check#(sent(x)) -> check#(x) -> check#(rest(x)) -> check#(x)
     check#(sent(x)) -> check#(x) -> check#(rest(x)) -> rest#(check(x))
     check#(sent(x)) -> check#(x) -> check#(cons(x,y)) -> check#(x)
     check#(sent(x)) -> check#(x) -> check#(cons(x,y)) -> check#(y)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(sent(x)) -> check#(x)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(rest(x)) -> check#(x)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(rest(x)) -> rest#(check(x))
     top#(sent(x)) -> check#(rest(x)) ->
     check#(cons(x,y)) -> check#(x)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(cons(x,y)) -> check#(y)
     top#(sent(x)) -> top#(check(rest(x))) ->
     top#(sent(x)) -> 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)) -> top#(check(rest(x)))
    Restore Modifier:
     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)
     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)
      Open
      
      DPs:
       check#(cons(x,y)) -> check#(y)
       check#(cons(x,y)) -> check#(x)
       check#(rest(x)) -> check#(x)
       check#(sent(x)) -> 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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [check#](x0) = x0,
        
        [cons](x0, x1) = x0 + x1,
        
        [nil] = 0,
        
        [check](x0) = x0,
        
        [rest](x0) = x0 + 1,
        
        [top](x0) = 0,
        
        [sent](x0) = x0
       orientation:
        check#(cons(x,y)) = x + y >= y = check#(y)
        
        check#(cons(x,y)) = x + y >= x = check#(x)
        
        check#(rest(x)) = x + 1 >= x = check#(x)
        
        check#(sent(x)) = x >= x = check#(x)
        
        top(sent(x)) = 0 >= 0 = top(check(rest(x)))
        
        rest(nil()) = 1 >= 0 = sent(nil())
        
        rest(cons(x,y)) = x + y + 1 >= y = sent(y)
        
        check(sent(x)) = x >= x = sent(check(x))
        
        check(rest(x)) = x + 1 >= x + 1 = rest(check(x))
        
        check(cons(x,y)) = x + y >= x + y = cons(check(x),y)
        
        check(cons(x,y)) = x + y >= x + y = cons(x,check(y))
        
        check(cons(x,y)) = x + y >= x + y = cons(x,y)
       problem:
        DPs:
         check#(cons(x,y)) -> check#(y)
         check#(cons(x,y)) -> check#(x)
         check#(sent(x)) -> 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)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [check#](x0) = x0 + 1,
         
         [cons](x0, x1) = x0 + x1,
         
         [nil] = 1,
         
         [check](x0) = x0,
         
         [rest](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [sent](x0) = x0 + 1
        orientation:
         check#(cons(x,y)) = x + y + 1 >= y + 1 = check#(y)
         
         check#(cons(x,y)) = x + y + 1 >= x + 1 = check#(x)
         
         check#(sent(x)) = x + 2 >= x + 1 = check#(x)
         
         top(sent(x)) = 0 >= 0 = top(check(rest(x)))
         
         rest(nil()) = 2 >= 2 = sent(nil())
         
         rest(cons(x,y)) = x + y + 1 >= y + 1 = sent(y)
         
         check(sent(x)) = x + 1 >= x + 1 = sent(check(x))
         
         check(rest(x)) = x + 1 >= x + 1 = rest(check(x))
         
         check(cons(x,y)) = x + y >= x + y = cons(check(x),y)
         
         check(cons(x,y)) = x + y >= x + y = cons(x,check(y))
         
         check(cons(x,y)) = x + y >= x + y = cons(x,y)
        problem:
         DPs:
          check#(cons(x,y)) -> check#(y)
          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)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [check#](x0) = x0,
          
          [cons](x0, x1) = x0 + x1 + 1,
          
          [nil] = 0,
          
          [check](x0) = x0,
          
          [rest](x0) = 0,
          
          [top](x0) = 0,
          
          [sent](x0) = 0
         orientation:
          check#(cons(x,y)) = x + y + 1 >= y = check#(y)
          
          check#(cons(x,y)) = x + y + 1 >= x = check#(x)
          
          top(sent(x)) = 0 >= 0 = top(check(rest(x)))
          
          rest(nil()) = 0 >= 0 = sent(nil())
          
          rest(cons(x,y)) = 0 >= 0 = sent(y)
          
          check(sent(x)) = 0 >= 0 = sent(check(x))
          
          check(rest(x)) = 0 >= 0 = rest(check(x))
          
          check(cons(x,y)) = x + y + 1 >= x + y + 1 = cons(check(x),y)
          
          check(cons(x,y)) = x + y + 1 >= x + y + 1 = cons(x,check(y))
          
          check(cons(x,y)) = x + y + 1 >= x + y + 1 = cons(x,y)
         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