MAYBE

Problem:
 app(nil(),k) -> k
 app(l,nil()) -> l
 app(cons(x,l),k) -> cons(x,app(l,k))
 sum(cons(x,nil())) -> cons(x,nil())
 sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
 sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
 pred(cons(s(x),nil())) -> cons(x,nil())

Proof:
 Complexity Transformation Processor:
  strict:
   app(nil(),k) -> k
   app(l,nil()) -> l
   app(cons(x,l),k) -> cons(x,app(l,k))
   sum(cons(x,nil())) -> cons(x,nil())
   sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
   sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
   pred(cons(s(x),nil())) -> cons(x,nil())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [pred](x0) = x0 + 1,
     
     [s](x0) = x0,
     
     [0] = 0,
     
     [plus](x0, x1) = x0 + x1,
     
     [sum](x0) = x0,
     
     [cons](x0, x1) = x0 + x1 + 1,
     
     [app](x0, x1) = x0 + x1,
     
     [nil] = 1
    orientation:
     app(nil(),k) = k + 1 >= k = k
     
     app(l,nil()) = l + 1 >= l = l
     
     app(cons(x,l),k) = k + l + x + 1 >= k + l + x + 1 = cons(x,app(l,k))
     
     sum(cons(x,nil())) = x + 2 >= x + 2 = cons(x,nil())
     
     sum(cons(x,cons(y,l))) = l + x + y + 2 >= l + x + y + 1 = sum(cons(plus(x,y),l))
     
     sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 2 >= k + l + x + y + 2 = sum(app(l,sum(cons(x,cons(y,k)))))
     
     plus(0(),y) = y >= y = y
     
     plus(s(x),y) = x + y >= x + y = s(plus(x,y))
     
     sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 2 >= l + x + y + 3 = pred(sum(cons(s(x),cons(y,l))))
     
     pred(cons(s(x),nil())) = x + 3 >= x + 2 = cons(x,nil())
    problem:
     strict:
      app(cons(x,l),k) -> cons(x,app(l,k))
      sum(cons(x,nil())) -> cons(x,nil())
      sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
      plus(0(),y) -> y
      plus(s(x),y) -> s(plus(x,y))
      sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
     weak:
      app(nil(),k) -> k
      app(l,nil()) -> l
      sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
      pred(cons(s(x),nil())) -> cons(x,nil())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [pred](x0) = x0,
       
       [s](x0) = x0,
       
       [0] = 1,
       
       [plus](x0, x1) = x0 + x1,
       
       [sum](x0) = x0,
       
       [cons](x0, x1) = x0 + x1,
       
       [app](x0, x1) = x0 + x1 + 1,
       
       [nil] = 0
      orientation:
       app(cons(x,l),k) = k + l + x + 1 >= k + l + x + 1 = cons(x,app(l,k))
       
       sum(cons(x,nil())) = x >= x = cons(x,nil())
       
       sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 1 >= k + l + x + y + 1 = sum(app(l,sum(cons(x,cons(y,k)))))
       
       plus(0(),y) = y + 1 >= y = y
       
       plus(s(x),y) = x + y >= x + y = s(plus(x,y))
       
       sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 1 >= l + x + y = pred(sum(cons(s(x),cons(y,l))))
       
       app(nil(),k) = k + 1 >= k = k
       
       app(l,nil()) = l + 1 >= l = l
       
       sum(cons(x,cons(y,l))) = l + x + y >= l + x + y = sum(cons(plus(x,y),l))
       
       pred(cons(s(x),nil())) = x >= x = cons(x,nil())
      problem:
       strict:
        app(cons(x,l),k) -> cons(x,app(l,k))
        sum(cons(x,nil())) -> cons(x,nil())
        sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
        plus(s(x),y) -> s(plus(x,y))
       weak:
        plus(0(),y) -> y
        sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
        app(nil(),k) -> k
        app(l,nil()) -> l
        sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
        pred(cons(s(x),nil())) -> cons(x,nil())
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [pred](x0) = x0,
         
         [s](x0) = x0,
         
         [0] = 0,
         
         [plus](x0, x1) = x0 + x1,
         
         [sum](x0) = x0 + 1,
         
         [cons](x0, x1) = x0 + x1,
         
         [app](x0, x1) = x0 + x1,
         
         [nil] = 0
        orientation:
         app(cons(x,l),k) = k + l + x >= k + l + x = cons(x,app(l,k))
         
         sum(cons(x,nil())) = x + 1 >= x = cons(x,nil())
         
         sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 1 >= k + l + x + y + 2 = sum(app(l,sum(cons(x,cons(y,k)))))
         
         plus(s(x),y) = x + y >= x + y = s(plus(x,y))
         
         plus(0(),y) = y >= y = y
         
         sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 1 >= l + x + y + 1 = pred(sum(cons(s(x),cons(y,l))))
         
         app(nil(),k) = k >= k = k
         
         app(l,nil()) = l >= l = l
         
         sum(cons(x,cons(y,l))) = l + x + y + 1 >= l + x + y + 1 = sum(cons(plus(x,y),l))
         
         pred(cons(s(x),nil())) = x >= x = cons(x,nil())
        problem:
         strict:
          app(cons(x,l),k) -> cons(x,app(l,k))
          sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
          plus(s(x),y) -> s(plus(x,y))
         weak:
          sum(cons(x,nil())) -> cons(x,nil())
          plus(0(),y) -> y
          sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
          app(nil(),k) -> k
          app(l,nil()) -> l
          sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
          pred(cons(s(x),nil())) -> cons(x,nil())
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                          
           [pred](x0) = x0,
           
                     [1 0]  
           [s](x0) = [0 0]x0,
           
                 [1]
           [0] = [0],
           
                            [1 0]       
           [plus](x0, x1) = [0 0]x0 + x1,
           
                       [1 0]     [0]
           [sum](x0) = [0 0]x0 + [1],
           
                            [1 0]          [0]
           [cons](x0, x1) = [0 0]x0 + x1 + [1],
           
                                [1 1]  
           [app](x0, x1) = x0 + [0 1]x1,
           
                   [0]
           [nil] = [0]
          orientation:
                              [1 1]        [1 0]    [0]    [1 1]        [1 0]    [0]                   
           app(cons(x,l),k) = [0 1]k + l + [0 0]x + [1] >= [0 1]k + l + [0 0]x + [1] = cons(x,app(l,k))
           
                                           [1 1]    [1 0]    [1 0]    [1 0]    [2]    [1 0]    [1 0]    [1 0]    [1 0]    [1]                                     
           sum(app(l,cons(x,cons(y,k)))) = [0 0]k + [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]k + [0 0]l + [0 0]x + [0 0]y + [1] = sum(app(l,sum(cons(x,cons(y,k)))))
           
                          [1 0]         [1 0]    [1 0]                
           plus(s(x),y) = [0 0]x + y >= [0 0]x + [0 0]y = s(plus(x,y))
           
                                [1 0]    [0]    [1 0]    [0]                
           sum(cons(x,nil())) = [0 0]x + [1] >= [0 0]x + [1] = cons(x,nil())
           
                             [1]         
           plus(0(),y) = y + [0] >= y = y
           
                                              [1 0]    [1 0]    [1 0]    [1]    [1 0]    [1 0]    [1 0]    [0]                                  
           sum(plus(cons(0(),x),cons(y,l))) = [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]l + [0 0]x + [0 0]y + [1] = pred(sum(cons(s(x),cons(y,l))))
           
                          [1 1]          
           app(nil(),k) = [0 1]k >= k = k
           
                                    
           app(l,nil()) = l >= l = l
           
                                    [1 0]    [1 0]    [1 0]    [0]    [1 0]    [1 0]    [1 0]    [0]                         
           sum(cons(x,cons(y,l))) = [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]l + [0 0]x + [0 0]y + [1] = sum(cons(plus(x,y),l))
           
                                    [1 0]    [0]    [1 0]    [0]                
           pred(cons(s(x),nil())) = [0 0]x + [1] >= [0 0]x + [1] = cons(x,nil())
          problem:
           strict:
            app(cons(x,l),k) -> cons(x,app(l,k))
            plus(s(x),y) -> s(plus(x,y))
           weak:
            sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
            sum(cons(x,nil())) -> cons(x,nil())
            plus(0(),y) -> y
            sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
            app(nil(),k) -> k
            app(l,nil()) -> l
            sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
            pred(cons(s(x),nil())) -> cons(x,nil())
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                          [1 0]     [0]
             [pred](x0) = [0 0]x0 + [1],
             
                       [1 0]  
             [s](x0) = [0 0]x0,
             
                   [0]
             [0] = [0],
             
                              [1 0]          [1]
             [plus](x0, x1) = [0 0]x0 + x1 + [0],
             
                         [1 0]     [0]
             [sum](x0) = [0 0]x0 + [1],
             
                              [1 0]          [1]
             [cons](x0, x1) = [0 0]x0 + x1 + [1],
             
                             [1 1]       
             [app](x0, x1) = [0 1]x0 + x1,
             
                     [0]
             [nil] = [0]
            orientation:
                                    [1 1]    [1 0]    [2]        [1 1]    [1 0]    [1]                   
             app(cons(x,l),k) = k + [0 1]l + [0 0]x + [1] >= k + [0 1]l + [0 0]x + [1] = cons(x,app(l,k))
             
                            [1 0]        [1]    [1 0]    [1 0]    [1]               
             plus(s(x),y) = [0 0]x + y + [0] >= [0 0]x + [0 0]y + [0] = s(plus(x,y))
             
                                             [1 0]    [1 1]    [1 0]    [1 0]    [2]    [1 0]    [1 1]    [1 0]    [1 0]    [2]                                     
             sum(app(l,cons(x,cons(y,k)))) = [0 0]k + [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]k + [0 0]l + [0 0]x + [0 0]y + [1] = sum(app(l,sum(cons(x,cons(y,k)))))
             
                                  [1 0]    [1]    [1 0]    [1]                
             sum(cons(x,nil())) = [0 0]x + [1] >= [0 0]x + [1] = cons(x,nil())
             
                               [1]         
             plus(0(),y) = y + [0] >= y = y
             
                                                [1 0]    [1 0]    [1 0]    [3]    [1 0]    [1 0]    [1 0]    [2]                                  
             sum(plus(cons(0(),x),cons(y,l))) = [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]l + [0 0]x + [0 0]y + [1] = pred(sum(cons(s(x),cons(y,l))))
             
                                      
             app(nil(),k) = k >= k = k
             
                            [1 1]          
             app(l,nil()) = [0 1]l >= l = l
             
                                      [1 0]    [1 0]    [1 0]    [2]    [1 0]    [1 0]    [1 0]    [2]                         
             sum(cons(x,cons(y,l))) = [0 0]l + [0 0]x + [0 0]y + [1] >= [0 0]l + [0 0]x + [0 0]y + [1] = sum(cons(plus(x,y),l))
             
                                      [1 0]    [1]    [1 0]    [1]                
             pred(cons(s(x),nil())) = [0 0]x + [1] >= [0 0]x + [1] = cons(x,nil())
            problem:
             strict:
              plus(s(x),y) -> s(plus(x,y))
             weak:
              app(cons(x,l),k) -> cons(x,app(l,k))
              sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
              sum(cons(x,nil())) -> cons(x,nil())
              plus(0(),y) -> y
              sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
              app(nil(),k) -> k
              app(l,nil()) -> l
              sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
              pred(cons(s(x),nil())) -> cons(x,nil())
            Open