MAYBE

Problem:
 R(2(x1)) -> 2(R(x1))
 R(3(x1)) -> 3(R(x1))
 R(1(x1)) -> L(3(x1))
 3(L(x1)) -> L(3(x1))
 2(L(x1)) -> L(2(x1))
 0(L(x1)) -> 2(R(x1))
 R(b(x1)) -> c(1(b(x1)))
 3(c(x1)) -> c(1(x1))
 2(c(1(x1))) -> c(0(R(1(x1))))
 2(c(0(x1))) -> c(0(0(x1)))

Proof:
 Complexity Transformation Processor:
  strict:
   R(2(x1)) -> 2(R(x1))
   R(3(x1)) -> 3(R(x1))
   R(1(x1)) -> L(3(x1))
   3(L(x1)) -> L(3(x1))
   2(L(x1)) -> L(2(x1))
   0(L(x1)) -> 2(R(x1))
   R(b(x1)) -> c(1(b(x1)))
   3(c(x1)) -> c(1(x1))
   2(c(1(x1))) -> c(0(R(1(x1))))
   2(c(0(x1))) -> c(0(0(x1)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [c](x0) = x0,
     
     [b](x0) = x0,
     
     [0](x0) = x0,
     
     [L](x0) = x0,
     
     [1](x0) = x0,
     
     [3](x0) = x0,
     
     [R](x0) = x0,
     
     [2](x0) = x0 + 1
    orientation:
     R(2(x1)) = x1 + 1 >= x1 + 1 = 2(R(x1))
     
     R(3(x1)) = x1 >= x1 = 3(R(x1))
     
     R(1(x1)) = x1 >= x1 = L(3(x1))
     
     3(L(x1)) = x1 >= x1 = L(3(x1))
     
     2(L(x1)) = x1 + 1 >= x1 + 1 = L(2(x1))
     
     0(L(x1)) = x1 >= x1 + 1 = 2(R(x1))
     
     R(b(x1)) = x1 >= x1 = c(1(b(x1)))
     
     3(c(x1)) = x1 >= x1 = c(1(x1))
     
     2(c(1(x1))) = x1 + 1 >= x1 = c(0(R(1(x1))))
     
     2(c(0(x1))) = x1 + 1 >= x1 = c(0(0(x1)))
    problem:
     strict:
      R(2(x1)) -> 2(R(x1))
      R(3(x1)) -> 3(R(x1))
      R(1(x1)) -> L(3(x1))
      3(L(x1)) -> L(3(x1))
      2(L(x1)) -> L(2(x1))
      0(L(x1)) -> 2(R(x1))
      R(b(x1)) -> c(1(b(x1)))
      3(c(x1)) -> c(1(x1))
     weak:
      2(c(1(x1))) -> c(0(R(1(x1))))
      2(c(0(x1))) -> c(0(0(x1)))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [c](x0) = x0,
       
       [b](x0) = x0,
       
       [0](x0) = x0 + 1,
       
       [L](x0) = x0,
       
       [1](x0) = x0,
       
       [3](x0) = x0 + 1,
       
       [R](x0) = x0,
       
       [2](x0) = x0 + 1
      orientation:
       R(2(x1)) = x1 + 1 >= x1 + 1 = 2(R(x1))
       
       R(3(x1)) = x1 + 1 >= x1 + 1 = 3(R(x1))
       
       R(1(x1)) = x1 >= x1 + 1 = L(3(x1))
       
       3(L(x1)) = x1 + 1 >= x1 + 1 = L(3(x1))
       
       2(L(x1)) = x1 + 1 >= x1 + 1 = L(2(x1))
       
       0(L(x1)) = x1 + 1 >= x1 + 1 = 2(R(x1))
       
       R(b(x1)) = x1 >= x1 = c(1(b(x1)))
       
       3(c(x1)) = x1 + 1 >= x1 = c(1(x1))
       
       2(c(1(x1))) = x1 + 1 >= x1 + 1 = c(0(R(1(x1))))
       
       2(c(0(x1))) = x1 + 2 >= x1 + 2 = c(0(0(x1)))
      problem:
       strict:
        R(2(x1)) -> 2(R(x1))
        R(3(x1)) -> 3(R(x1))
        R(1(x1)) -> L(3(x1))
        3(L(x1)) -> L(3(x1))
        2(L(x1)) -> L(2(x1))
        0(L(x1)) -> 2(R(x1))
        R(b(x1)) -> c(1(b(x1)))
       weak:
        3(c(x1)) -> c(1(x1))
        2(c(1(x1))) -> c(0(R(1(x1))))
        2(c(0(x1))) -> c(0(0(x1)))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [c](x0) = x0,
         
         [b](x0) = x0 + 1,
         
         [0](x0) = x0,
         
         [L](x0) = x0 + 1,
         
         [1](x0) = x0,
         
         [3](x0) = x0,
         
         [R](x0) = x0,
         
         [2](x0) = x0
        orientation:
         R(2(x1)) = x1 >= x1 = 2(R(x1))
         
         R(3(x1)) = x1 >= x1 = 3(R(x1))
         
         R(1(x1)) = x1 >= x1 + 1 = L(3(x1))
         
         3(L(x1)) = x1 + 1 >= x1 + 1 = L(3(x1))
         
         2(L(x1)) = x1 + 1 >= x1 + 1 = L(2(x1))
         
         0(L(x1)) = x1 + 1 >= x1 = 2(R(x1))
         
         R(b(x1)) = x1 + 1 >= x1 + 1 = c(1(b(x1)))
         
         3(c(x1)) = x1 >= x1 = c(1(x1))
         
         2(c(1(x1))) = x1 >= x1 = c(0(R(1(x1))))
         
         2(c(0(x1))) = x1 >= x1 = c(0(0(x1)))
        problem:
         strict:
          R(2(x1)) -> 2(R(x1))
          R(3(x1)) -> 3(R(x1))
          R(1(x1)) -> L(3(x1))
          3(L(x1)) -> L(3(x1))
          2(L(x1)) -> L(2(x1))
          R(b(x1)) -> c(1(b(x1)))
         weak:
          0(L(x1)) -> 2(R(x1))
          3(c(x1)) -> c(1(x1))
          2(c(1(x1))) -> c(0(R(1(x1))))
          2(c(0(x1))) -> c(0(0(x1)))
        Open