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())
        Bounds Processor:
         bound: 0
         enrichment: match
         automaton:
          final states: {8,7,6,5}
          transitions:
           app0(3,1) -> 5*
           app0(3,3) -> 5*
           app0(4,2) -> 5*
           app0(4,4) -> 5*
           app0(1,2) -> 5*
           app0(1,4) -> 5*
           app0(2,1) -> 5*
           app0(2,3) -> 5*
           app0(3,2) -> 5*
           app0(3,4) -> 5*
           app0(4,1) -> 5*
           app0(4,3) -> 5*
           app0(1,1) -> 5*
           app0(1,3) -> 5*
           app0(2,2) -> 5*
           app0(2,4) -> 5*
           cons0(3,1) -> 1*
           cons0(3,3) -> 8,6,1
           cons0(3,5) -> 5*
           cons0(4,2) -> 1*
           cons0(4,4) -> 1*
           cons0(1,2) -> 1*
           cons0(1,4) -> 1*
           cons0(7,1) -> 1*
           cons0(2,1) -> 1*
           cons0(7,3) -> 8,6,1
           cons0(2,3) -> 8,6,1
           cons0(7,5) -> 5*
           cons0(2,5) -> 5*
           cons0(3,2) -> 1*
           cons0(3,4) -> 1*
           cons0(4,1) -> 1*
           cons0(4,3) -> 8,6,1
           cons0(4,5) -> 5*
           cons0(1,1) -> 1*
           cons0(1,3) -> 8,6,1
           cons0(1,5) -> 5*
           cons0(7,2) -> 1*
           cons0(2,2) -> 1*
           cons0(7,4) -> 1*
           cons0(2,4) -> 1*
           sum0(2) -> 6*
           sum0(4) -> 6*
           sum0(1) -> 6*
           sum0(3) -> 6*
           plus0(3,1) -> 7*
           plus0(3,3) -> 7*
           plus0(3,7) -> 1*
           plus0(4,2) -> 7*
           plus0(4,4) -> 7*
           plus0(1,2) -> 7*
           plus0(1,4) -> 7*
           plus0(7,1) -> 1*
           plus0(2,1) -> 7*
           plus0(7,3) -> 1*
           plus0(2,3) -> 7*
           plus0(7,7) -> 1*
           plus0(3,2) -> 7*
           plus0(3,4) -> 7*
           plus0(4,1) -> 7*
           plus0(4,3) -> 7*
           plus0(1,1) -> 7*
           plus0(1,3) -> 7*
           plus0(2,2) -> 7*
           plus0(7,4) -> 1*
           plus0(2,4) -> 7*
           s0(7) -> 7*
           s0(2) -> 2*
           s0(4) -> 2*
           s0(1) -> 1,2
           s0(3) -> 2*
           nil0() -> 3*
           00() -> 4*
           pred0(2) -> 8*
           pred0(4) -> 8*
           pred0(6) -> 6*
           pred0(1) -> 8*
           pred0(3) -> 8*
           1 -> 5,7
           2 -> 5,7
           3 -> 5,7
           4 -> 1,5,7
           7 -> 1*
         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())
         Bounds Processor:
          bound: 1
          enrichment: match
          automaton:
           final states: {8,7,6,5}
           transitions:
            cons1(2,16) -> 16*
            cons1(3,9) -> 11,9,5
            cons1(3,11) -> 9,5
            cons1(3,21) -> 15*
            cons1(4,16) -> 16*
            cons1(25,9) -> 16*
            cons1(25,11) -> 16*
            cons1(25,21) -> 8,15,7
            cons1(6,16) -> 16*
            cons1(27,1) -> 16*
            cons1(1,16) -> 16*
            cons1(27,3) -> 16*
            cons1(27,9) -> 16*
            cons1(27,11) -> 16*
            cons1(2,9) -> 9,5
            cons1(2,11) -> 9,5
            cons1(27,21) -> 15,7
            cons1(2,21) -> 15*
            cons1(3,16) -> 16*
            cons1(4,9) -> 11,9,5
            cons1(4,11) -> 9,5
            cons1(25,2) -> 16*
            cons1(25,4) -> 16*
            cons1(4,21) -> 15*
            cons1(25,16) -> 16*
            cons1(6,9) -> 9,5
            cons1(1,9) -> 11,9,5
            cons1(1,11) -> 9,5
            cons1(27,2) -> 16*
            cons1(27,4) -> 16*
            cons1(6,21) -> 15,7
            cons1(1,21) -> 7*
            app1(3,1) -> 9*
            app1(3,3) -> 9*
            app1(3,15) -> 16*
            app1(4,2) -> 9*
            app1(4,4) -> 9*
            app1(1,2) -> 9*
            app1(1,4) -> 9*
            app1(2,1) -> 9*
            app1(2,3) -> 11*
            app1(2,15) -> 16*
            app1(3,2) -> 9*
            app1(3,4) -> 9*
            app1(4,1) -> 9*
            app1(4,3) -> 11*
            app1(4,15) -> 16*
            app1(1,1) -> 9*
            app1(1,3) -> 9*
            app1(1,15) -> 16*
            app1(2,2) -> 9*
            app1(2,4) -> 9*
            s1(25) -> 25*
            s1(27) -> 27*
            s1(1) -> 2,1
            plus1(3,25) -> 25*
            plus1(3,27) -> 25*
            plus1(25,25) -> 1*
            plus1(6,2) -> 25*
            plus1(1,2) -> 25*
            plus1(25,27) -> 25*
            plus1(6,6) -> 27*
            plus1(1,6) -> 27*
            plus1(27,1) -> 25*
            plus1(25,6) -> 2*
            plus1(6,1) -> 27*
            plus1(1,1) -> 27*
            plus1(1,25) -> 25*
            plus1(1,27) -> 25*
            pred1(7) -> 7,15
            nil1() -> 21*
            app0(3,1) -> 5*
            app0(3,3) -> 5*
            app0(4,2) -> 5*
            app0(4,4) -> 5*
            app0(1,2) -> 5*
            app0(1,4) -> 5*
            app0(2,1) -> 5*
            app0(2,3) -> 5*
            app0(3,2) -> 5*
            app0(3,4) -> 5*
            app0(4,1) -> 5*
            app0(4,3) -> 5*
            app0(1,1) -> 5*
            app0(1,3) -> 5*
            app0(2,2) -> 5*
            app0(2,4) -> 5*
            sum1(5) -> 15*
            sum1(16) -> 15,7
            cons0(3,1) -> 1*
            cons0(3,3) -> 8,7,1
            cons0(4,2) -> 1*
            cons0(4,4) -> 1*
            cons0(1,2) -> 1*
            cons0(1,4) -> 1*
            cons0(2,1) -> 1*
            cons0(2,3) -> 8,7,1
            cons0(3,2) -> 1*
            cons0(3,4) -> 1*
            cons0(4,1) -> 1*
            cons0(4,3) -> 8,7,1
            cons0(6,1) -> 1*
            cons0(1,1) -> 1*
            cons0(1,3) -> 8,7,1
            cons0(2,2) -> 1*
            cons0(2,4) -> 1*
            sum0(5) -> 7*
            sum0(2) -> 7*
            sum0(4) -> 7*
            sum0(1) -> 7*
            sum0(3) -> 7*
            plus0(3,1) -> 6*
            plus0(3,3) -> 6*
            plus0(4,2) -> 6*
            plus0(4,4) -> 6*
            plus0(6,2) -> 1*
            plus0(1,2) -> 6*
            plus0(1,4) -> 6*
            plus0(6,6) -> 1*
            plus0(1,6) -> 1*
            plus0(2,1) -> 6*
            plus0(2,3) -> 6*
            plus0(3,2) -> 6*
            plus0(3,4) -> 6*
            plus0(4,1) -> 6*
            plus0(4,3) -> 6*
            plus0(6,1) -> 1*
            plus0(1,1) -> 6*
            plus0(1,3) -> 6*
            plus0(2,2) -> 6*
            plus0(2,4) -> 6*
            s0(2) -> 2*
            s0(4) -> 2*
            s0(6) -> 6*
            s0(1) -> 1,2
            s0(3) -> 2*
            nil0() -> 3*
            00() -> 4*
            pred0(7) -> 7*
            pred0(2) -> 8*
            pred0(4) -> 8*
            pred0(1) -> 8*
            pred0(3) -> 8*
            1 -> 27,9,5,6
            2 -> 25,11,9,5,6
            3 -> 9,5,6
            4 -> 11,9,5,6
            6 -> 2,1,27
            15 -> 16*
            25 -> 1*
            27 -> 25*
          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