MAYBE

Problem:
 int(0(),0()) -> .(0(),nil())
 int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
 int(s(x),0()) -> nil()
 int(s(x),s(y)) -> int_list(int(x,y))
 int_list(nil()) -> nil()
 int_list(.(x,y)) -> .(s(x),int_list(y))

Proof:
 Complexity Transformation Processor:
  strict:
   int(0(),0()) -> .(0(),nil())
   int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
   int(s(x),0()) -> nil()
   int(s(x),s(y)) -> int_list(int(x,y))
   int_list(nil()) -> nil()
   int_list(.(x,y)) -> .(s(x),int_list(y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [int_list](x0) = x0,
     
     [s](x0) = x0,
     
     [.](x0, x1) = x0 + x1,
     
     [nil] = 1,
     
     [int](x0, x1) = x0 + x1 + 1,
     
     [0] = 1
    orientation:
     int(0(),0()) = 3 >= 2 = .(0(),nil())
     
     int(0(),s(y)) = y + 2 >= y + 3 = .(0(),int(s(0()),s(y)))
     
     int(s(x),0()) = x + 2 >= 1 = nil()
     
     int(s(x),s(y)) = x + y + 1 >= x + y + 1 = int_list(int(x,y))
     
     int_list(nil()) = 1 >= 1 = nil()
     
     int_list(.(x,y)) = x + y >= x + y = .(s(x),int_list(y))
    problem:
     strict:
      int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
      int(s(x),s(y)) -> int_list(int(x,y))
      int_list(nil()) -> nil()
      int_list(.(x,y)) -> .(s(x),int_list(y))
     weak:
      int(0(),0()) -> .(0(),nil())
      int(s(x),0()) -> nil()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [int_list](x0) = x0 + 1,
       
       [s](x0) = x0,
       
       [.](x0, x1) = x0 + x1,
       
       [nil] = 1,
       
       [int](x0, x1) = x0 + x1 + 1,
       
       [0] = 0
      orientation:
       int(0(),s(y)) = y + 1 >= y + 1 = .(0(),int(s(0()),s(y)))
       
       int(s(x),s(y)) = x + y + 1 >= x + y + 2 = int_list(int(x,y))
       
       int_list(nil()) = 2 >= 1 = nil()
       
       int_list(.(x,y)) = x + y + 1 >= x + y + 1 = .(s(x),int_list(y))
       
       int(0(),0()) = 1 >= 1 = .(0(),nil())
       
       int(s(x),0()) = x + 1 >= 1 = nil()
      problem:
       strict:
        int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
        int(s(x),s(y)) -> int_list(int(x,y))
        int_list(.(x,y)) -> .(s(x),int_list(y))
       weak:
        int_list(nil()) -> nil()
        int(0(),0()) -> .(0(),nil())
        int(s(x),0()) -> nil()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [int_list](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [.](x0, x1) = x0 + x1,
         
         [nil] = 0,
         
         [int](x0, x1) = x0 + x1,
         
         [0] = 0
        orientation:
         int(0(),s(y)) = y + 1 >= y + 2 = .(0(),int(s(0()),s(y)))
         
         int(s(x),s(y)) = x + y + 2 >= x + y = int_list(int(x,y))
         
         int_list(.(x,y)) = x + y >= x + y + 1 = .(s(x),int_list(y))
         
         int_list(nil()) = 0 >= 0 = nil()
         
         int(0(),0()) = 0 >= 0 = .(0(),nil())
         
         int(s(x),0()) = x + 1 >= 0 = nil()
        problem:
         strict:
          int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
          int_list(.(x,y)) -> .(s(x),int_list(y))
         weak:
          int(s(x),s(y)) -> int_list(int(x,y))
          int_list(nil()) -> nil()
          int(0(),0()) -> .(0(),nil())
          int(s(x),0()) -> nil()
        Bounds Processor:
         bound: 1
         enrichment: match
         automaton:
          final states: {6,5}
          transitions:
           .1(8,13) -> 18*
           .1(7,13) -> 5,13,6
           .1(8,10) -> 32,10,21,18,5
           .1(9,21) -> 18,32,21,10,5
           01() -> 8*
           int1(8,1) -> 18*
           int1(3,1) -> 32*
           int1(8,3) -> 18*
           int1(3,3) -> 32*
           int1(9,2) -> 32*
           int1(4,2) -> 32*
           int1(9,4) -> 32*
           int1(4,4) -> 32*
           int1(1,2) -> 32*
           int1(1,4) -> 32*
           int1(7,1) -> 18*
           int1(2,1) -> 32*
           int1(7,3) -> 18*
           int1(2,3) -> 32*
           int1(8,2) -> 18*
           int1(3,2) -> 32*
           int1(8,4) -> 18*
           int1(3,4) -> 32*
           int1(9,1) -> 32*
           int1(4,1) -> 32*
           int1(9,3) -> 32*
           int1(4,3) -> 32*
           int1(9,7) -> 10*
           int1(1,1) -> 32*
           int1(1,3) -> 32*
           int1(7,2) -> 18*
           int1(2,2) -> 32*
           int1(7,4) -> 18*
           int1(2,4) -> 32*
           s1(7) -> 9*
           s1(2) -> 7*
           s1(9) -> 8*
           s1(4) -> 7*
           s1(1) -> 7*
           s1(8) -> 9*
           s1(3) -> 7*
           int_list1(10) -> 21*
           int_list1(32) -> 32,18
           int_list1(2) -> 13*
           int_list1(4) -> 13*
           int_list1(21) -> 10*
           int_list1(1) -> 13*
           int_list1(18) -> 32,10
           int_list1(13) -> 21*
           int_list1(3) -> 13*
           nil1() -> 32,10,18,21,13
           int0(3,1) -> 5*
           int0(3,3) -> 5*
           int0(4,2) -> 5*
           int0(4,4) -> 5*
           int0(1,2) -> 5*
           int0(1,4) -> 5*
           int0(2,1) -> 5*
           int0(2,3) -> 5*
           int0(3,2) -> 5*
           int0(3,4) -> 5*
           int0(4,1) -> 5*
           int0(4,3) -> 5*
           int0(1,1) -> 5*
           int0(1,3) -> 5*
           int0(2,2) -> 5*
           int0(2,4) -> 5*
           00() -> 1*
           s0(2) -> 2*
           s0(4) -> 2*
           s0(1) -> 2*
           s0(3) -> 2*
           .0(3,1) -> 3*
           .0(3,3) -> 3*
           .0(4,2) -> 3*
           .0(4,4) -> 3*
           .0(1,2) -> 3*
           .0(1,4) -> 5,3
           .0(2,1) -> 3*
           .0(2,3) -> 3*
           .0(3,2) -> 3*
           .0(3,4) -> 3*
           .0(4,1) -> 3*
           .0(4,3) -> 3*
           .0(1,1) -> 3*
           .0(1,3) -> 3*
           .0(2,2) -> 3*
           .0(2,4) -> 3*
           int_list0(5) -> 5*
           int_list0(2) -> 6*
           int_list0(4) -> 6*
           int_list0(1) -> 6*
           int_list0(3) -> 6*
           nil0() -> 5,6,4
         problem:
          strict:
           int_list(.(x,y)) -> .(s(x),int_list(y))
          weak:
           int(0(),s(y)) -> .(0(),int(s(0()),s(y)))
           int(s(x),s(y)) -> int_list(int(x,y))
           int_list(nil()) -> nil()
           int(0(),0()) -> .(0(),nil())
           int(s(x),0()) -> nil()
         Open