MAYBE

Problem:
 rev(nil()) -> nil()
 rev(.(x,y)) -> ++(rev(y),.(x,nil()))
 car(.(x,y)) -> x
 cdr(.(x,y)) -> y
 null(nil()) -> true()
 null(.(x,y)) -> false()
 ++(nil(),y) -> y
 ++(.(x,y),z) -> .(x,++(y,z))

Proof:
 Complexity Transformation Processor:
  strict:
   rev(nil()) -> nil()
   rev(.(x,y)) -> ++(rev(y),.(x,nil()))
   car(.(x,y)) -> x
   cdr(.(x,y)) -> y
   null(nil()) -> true()
   null(.(x,y)) -> false()
   ++(nil(),y) -> y
   ++(.(x,y),z) -> .(x,++(y,z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [false] = 0,
     
     [true] = 0,
     
     [null](x0) = x0,
     
     [cdr](x0) = x0,
     
     [car](x0) = x0,
     
     [++](x0, x1) = x0 + x1,
     
     [.](x0, x1) = x0 + x1,
     
     [rev](x0) = x0 + 1,
     
     [nil] = 1
    orientation:
     rev(nil()) = 2 >= 1 = nil()
     
     rev(.(x,y)) = x + y + 1 >= x + y + 2 = ++(rev(y),.(x,nil()))
     
     car(.(x,y)) = x + y >= x = x
     
     cdr(.(x,y)) = x + y >= y = y
     
     null(nil()) = 1 >= 0 = true()
     
     null(.(x,y)) = x + y >= 0 = false()
     
     ++(nil(),y) = y + 1 >= y = y
     
     ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
    problem:
     strict:
      rev(.(x,y)) -> ++(rev(y),.(x,nil()))
      car(.(x,y)) -> x
      cdr(.(x,y)) -> y
      null(.(x,y)) -> false()
      ++(.(x,y),z) -> .(x,++(y,z))
     weak:
      rev(nil()) -> nil()
      null(nil()) -> true()
      ++(nil(),y) -> y
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [false] = 0,
       
       [true] = 0,
       
       [null](x0) = x0 + 1,
       
       [cdr](x0) = x0,
       
       [car](x0) = x0,
       
       [++](x0, x1) = x0 + x1,
       
       [.](x0, x1) = x0 + x1,
       
       [rev](x0) = x0,
       
       [nil] = 0
      orientation:
       rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
       
       car(.(x,y)) = x + y >= x = x
       
       cdr(.(x,y)) = x + y >= y = y
       
       null(.(x,y)) = x + y + 1 >= 0 = false()
       
       ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
       
       rev(nil()) = 0 >= 0 = nil()
       
       null(nil()) = 1 >= 0 = true()
       
       ++(nil(),y) = y >= y = y
      problem:
       strict:
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        car(.(x,y)) -> x
        cdr(.(x,y)) -> y
        ++(.(x,y),z) -> .(x,++(y,z))
       weak:
        null(.(x,y)) -> false()
        rev(nil()) -> nil()
        null(nil()) -> true()
        ++(nil(),y) -> y
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [false] = 0,
         
         [true] = 0,
         
         [null](x0) = x0,
         
         [cdr](x0) = x0 + 1,
         
         [car](x0) = x0,
         
         [++](x0, x1) = x0 + x1,
         
         [.](x0, x1) = x0 + x1,
         
         [rev](x0) = x0,
         
         [nil] = 0
        orientation:
         rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
         
         car(.(x,y)) = x + y >= x = x
         
         cdr(.(x,y)) = x + y + 1 >= y = y
         
         ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
         
         null(.(x,y)) = x + y >= 0 = false()
         
         rev(nil()) = 0 >= 0 = nil()
         
         null(nil()) = 0 >= 0 = true()
         
         ++(nil(),y) = y >= y = y
        problem:
         strict:
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          car(.(x,y)) -> x
          ++(.(x,y),z) -> .(x,++(y,z))
         weak:
          cdr(.(x,y)) -> y
          null(.(x,y)) -> false()
          rev(nil()) -> nil()
          null(nil()) -> true()
          ++(nil(),y) -> y
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [false] = 0,
           
           [true] = 0,
           
           [null](x0) = x0,
           
           [cdr](x0) = x0,
           
           [car](x0) = x0 + 1,
           
           [++](x0, x1) = x0 + x1,
           
           [.](x0, x1) = x0 + x1,
           
           [rev](x0) = x0,
           
           [nil] = 0
          orientation:
           rev(.(x,y)) = x + y >= x + y = ++(rev(y),.(x,nil()))
           
           car(.(x,y)) = x + y + 1 >= x = x
           
           ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
           
           cdr(.(x,y)) = x + y >= y = y
           
           null(.(x,y)) = x + y >= 0 = false()
           
           rev(nil()) = 0 >= 0 = nil()
           
           null(nil()) = 0 >= 0 = true()
           
           ++(nil(),y) = y >= y = y
          problem:
           strict:
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            ++(.(x,y),z) -> .(x,++(y,z))
           weak:
            car(.(x,y)) -> x
            cdr(.(x,y)) -> y
            null(.(x,y)) -> false()
            rev(nil()) -> nil()
            null(nil()) -> true()
            ++(nil(),y) -> y
          Bounds Processor:
           bound: 1
           enrichment: match
           automaton:
            final states: {9,8,7,6,5}
            transitions:
             ++1(10,11) -> 10*
             ++1(12,11) -> 12,5
             rev1(2) -> 12*
             rev1(4) -> 12*
             rev1(1) -> 12*
             rev1(3) -> 12*
             .1(2,10) -> 11*
             .1(4,10) -> 11*
             .1(1,10) -> 11*
             .1(3,10) -> 11*
             nil1() -> 12,10
             rev0(2) -> 5*
             rev0(4) -> 5*
             rev0(1) -> 5*
             rev0(3) -> 5*
             .0(3,1) -> 1*
             .0(3,3) -> 1*
             .0(4,2) -> 1*
             .0(4,4) -> 1*
             .0(4,6) -> 6*
             .0(1,2) -> 1*
             .0(1,4) -> 1*
             .0(1,6) -> 6*
             .0(2,1) -> 1*
             .0(2,3) -> 1*
             .0(3,2) -> 1*
             .0(3,4) -> 1*
             .0(3,6) -> 6*
             .0(4,1) -> 1*
             .0(4,3) -> 1*
             .0(1,1) -> 1*
             .0(1,3) -> 1*
             .0(2,2) -> 1*
             .0(2,4) -> 1*
             .0(2,6) -> 6*
             ++0(3,1) -> 6*
             ++0(3,3) -> 6*
             ++0(4,2) -> 6*
             ++0(4,4) -> 6*
             ++0(1,2) -> 6*
             ++0(1,4) -> 6*
             ++0(2,1) -> 6*
             ++0(2,3) -> 6*
             ++0(3,2) -> 6*
             ++0(3,4) -> 6*
             ++0(4,1) -> 6*
             ++0(4,3) -> 6*
             ++0(1,1) -> 6*
             ++0(1,3) -> 6*
             ++0(2,2) -> 6*
             ++0(2,4) -> 6*
             nil0() -> 5,2
             car0(2) -> 7*
             car0(4) -> 7*
             car0(1) -> 7*
             car0(3) -> 7*
             cdr0(2) -> 8*
             cdr0(4) -> 8*
             cdr0(1) -> 8*
             cdr0(3) -> 8*
             null0(2) -> 9*
             null0(4) -> 9*
             null0(1) -> 9*
             null0(3) -> 9*
             false0() -> 9,3
             true0() -> 9,4
             1 -> 6,8,7
             2 -> 6,8,7
             3 -> 6,8,7
             4 -> 6,8,7
             11 -> 10,5,12
           problem:
            strict:
             ++(.(x,y),z) -> .(x,++(y,z))
            weak:
             rev(.(x,y)) -> ++(rev(y),.(x,nil()))
             car(.(x,y)) -> x
             cdr(.(x,y)) -> y
             null(.(x,y)) -> false()
             rev(nil()) -> nil()
             null(nil()) -> true()
             ++(nil(),y) -> y
           Open