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))

Proof:
 RT 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))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [s](x0) = x0,
    
    [0] = 0,
    
    [plus](x0, x1) = x0 + x1 + 4,
    
    [sum](x0) = x0 + 1,
    
    [cons](x0, x1) = x0 + x1 + 24,
    
    [app](x0, x1) = x0 + x1 + 10,
    
    [nil] = 8
   orientation:
    app(nil(),k) = k + 18 >= k = k
    
    app(l,nil()) = l + 18 >= l = l
    
    app(cons(x,l),k) = k + l + x + 34 >= k + l + x + 34 = cons(x,app(l,k))
    
    sum(cons(x,nil())) = x + 33 >= x + 32 = cons(x,nil())
    
    sum(cons(x,cons(y,l))) = l + x + y + 49 >= l + x + y + 29 = sum(cons(plus(x,y),l))
    
    sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 59 >= k + l + x + y + 60 = sum(app(l,sum(cons(x,cons(y,k)))))
    
    plus(0(),y) = y + 4 >= y = y
    
    plus(s(x),y) = x + y + 4 >= x + y + 4 = s(plus(x,y))
   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:
     app(nil(),k) -> k
     app(l,nil()) -> l
     sum(cons(x,nil())) -> cons(x,nil())
     sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
     plus(0(),y) -> y
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [1 0]  
     [s](x0) = [0 0]x0,
     
           [0]
     [0] = [0],
     
                      [1 0]       
     [plus](x0, x1) = [0 0]x0 + x1,
     
                 [1 0]     [0]
     [sum](x0) = [0 0]x0 + [3],
     
                      [1 0]          [0]
     [cons](x0, x1) = [0 0]x0 + x1 + [2],
     
                     [1 2]          [0 ]
     [app](x0, x1) = [0 1]x0 + x1 + [13],
     
             [12]
     [nil] = [1 ]
    orientation:
                            [1 2]    [1 0]    [4 ]        [1 2]    [1 0]    [0 ]                   
     app(cons(x,l),k) = k + [0 1]l + [0 0]x + [15] >= k + [0 1]l + [0 0]x + [15] = cons(x,app(l,k))
     
                                     [1 0]    [1 2]    [1 0]    [1 0]    [0]    [1 0]    [1 2]    [1 0]    [1 0]    [0]                                     
     sum(app(l,cons(x,cons(y,k)))) = [0 0]k + [0 0]l + [0 0]x + [0 0]y + [3] >= [0 0]k + [0 0]l + [0 0]x + [0 0]y + [3] = 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))
     
                        [14]         
     app(nil(),k) = k + [14] >= k = k
     
                    [1 2]    [12]         
     app(l,nil()) = [0 1]l + [14] >= l = l
     
                          [1 0]    [12]    [1 0]    [12]                
     sum(cons(x,nil())) = [0 0]x + [3 ] >= [0 0]x + [3 ] = cons(x,nil())
     
                              [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 + [3] >= [0 0]l + [0 0]x + [0 0]y + [3] = sum(cons(plus(x,y),l))
     
                             
     plus(0(),y) = y >= y = y
    problem:
     strict:
      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:
      app(cons(x,l),k) -> cons(x,app(l,k))
      app(nil(),k) -> k
      app(l,nil()) -> l
      sum(cons(x,nil())) -> cons(x,nil())
      sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
      plus(0(),y) -> y
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                [1 0]     [0]
      [s](x0) = [0 0]x0 + [4],
      
            [0]
      [0] = [0],
      
                       [1 0]          [0]
      [plus](x0, x1) = [0 0]x0 + x1 + [4],
      
                  [1 0]     [0]
      [sum](x0) = [0 0]x0 + [9],
      
                       [1 0]          [0]
      [cons](x0, x1) = [0 0]x0 + x1 + [5],
      
                           [1 1]     [3]
      [app](x0, x1) = x0 + [0 1]x1 + [4],
      
              [2]
      [nil] = [3]
     orientation:
                                      [1 1]    [1 0]    [1 0]    [1 0]    [13]    [1 0]    [1 0]    [1 0]    [1 0]    [12]                                     
      sum(app(l,cons(x,cons(y,k)))) = [0 0]k + [0 0]l + [0 0]x + [0 0]y + [9 ] >= [0 0]k + [0 0]l + [0 0]x + [0 0]y + [9 ] = sum(app(l,sum(cons(x,cons(y,k)))))
      
                     [1 0]        [0]    [1 0]    [1 0]    [0]               
      plus(s(x),y) = [0 0]x + y + [4] >= [0 0]x + [0 0]y + [4] = s(plus(x,y))
      
                         [1 1]        [1 0]    [3]    [1 1]        [1 0]    [3]                   
      app(cons(x,l),k) = [0 1]k + l + [0 0]x + [9] >= [0 1]k + l + [0 0]x + [9] = cons(x,app(l,k))
      
                     [1 1]    [5]         
      app(nil(),k) = [0 1]k + [7] >= k = k
      
                         [8]         
      app(l,nil()) = l + [7] >= l = l
      
                           [1 0]    [2]    [1 0]    [2]                
      sum(cons(x,nil())) = [0 0]x + [9] >= [0 0]x + [8] = cons(x,nil())
      
                               [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 + [9] >= [0 0]l + [0 0]x + [0 0]y + [9] = sum(cons(plus(x,y),l))
      
                        [0]         
      plus(0(),y) = y + [4] >= y = y
     problem:
      strict:
       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)))))
       app(cons(x,l),k) -> cons(x,app(l,k))
       app(nil(),k) -> k
       app(l,nil()) -> l
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
       plus(0(),y) -> y
     Open