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:
 Complexity Transformation Processor:
  strict:
   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)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [cons](x0, x1) = x0 + x1 + 1,
     
     [nil] = 0,
     
     [check](x0) = x0 + 1,
     
     [rest](x0) = x0 + 1,
     
     [top](x0) = x0,
     
     [sent](x0) = x0
    orientation:
     top(sent(x)) = x >= x + 2 = top(check(rest(x)))
     
     rest(nil()) = 1 >= 0 = sent(nil())
     
     rest(cons(x,y)) = x + y + 2 >= y = sent(y)
     
     check(sent(x)) = x + 1 >= x + 1 = sent(check(x))
     
     check(rest(x)) = x + 2 >= x + 2 = rest(check(x))
     
     check(cons(x,y)) = x + y + 2 >= x + y + 2 = cons(check(x),y)
     
     check(cons(x,y)) = x + y + 2 >= x + y + 2 = cons(x,check(y))
     
     check(cons(x,y)) = x + y + 2 >= x + y + 1 = cons(x,y)
    problem:
     strict:
      top(sent(x)) -> top(check(rest(x)))
      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))
     weak:
      rest(nil()) -> sent(nil())
      rest(cons(x,y)) -> sent(y)
      check(cons(x,y)) -> cons(x,y)
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                             [1 1]     [0]
       [cons](x0, x1) = x0 + [0 1]x1 + [1],
       
               [0]
       [nil] = [0],
       
                     [1 1]  
       [check](x0) = [0 1]x0,
       
                      
       [rest](x0) = x0,
       
                   [1 0]     [0]
       [top](x0) = [0 0]x0 + [1],
       
                    [1 1]  
       [sent](x0) = [0 1]x0
      orientation:
                      [1 1]    [0]    [1 1]    [0]                      
       top(sent(x)) = [0 0]x + [1] >= [0 0]x + [1] = top(check(rest(x)))
       
                        [1 2]     [1 2]                  
       check(sent(x)) = [0 1]x >= [0 1]x = sent(check(x))
       
                        [1 1]     [1 1]                  
       check(rest(x)) = [0 1]x >= [0 1]x = rest(check(x))
       
                          [1 1]    [1 2]    [1]    [1 1]    [1 1]    [0]                   
       check(cons(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = cons(check(x),y)
       
                          [1 1]    [1 2]    [1]        [1 2]    [0]                   
       check(cons(x,y)) = [0 1]x + [0 1]y + [1] >= x + [0 1]y + [1] = cons(x,check(y))
       
                     [0]    [0]              
       rest(nil()) = [0] >= [0] = sent(nil())
       
                             [1 1]    [0]    [1 1]           
       rest(cons(x,y)) = x + [0 1]y + [1] >= [0 1]y = sent(y)
       
                          [1 1]    [1 2]    [1]        [1 1]    [0]            
       check(cons(x,y)) = [0 1]x + [0 1]y + [1] >= x + [0 1]y + [1] = cons(x,y)
      problem:
       strict:
        top(sent(x)) -> top(check(rest(x)))
        check(sent(x)) -> sent(check(x))
        check(rest(x)) -> rest(check(x))
       weak:
        check(cons(x,y)) -> cons(check(x),y)
        check(cons(x,y)) -> cons(x,check(y))
        rest(nil()) -> sent(nil())
        rest(cons(x,y)) -> sent(y)
        check(cons(x,y)) -> cons(x,y)
      Open