MAYBE

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

Proof:
 Complexity Transformation Processor:
  strict:
   1(2(1(x1))) -> 2(0(2(x1)))
   0(2(1(x1))) -> 1(0(2(x1)))
   L(2(1(x1))) -> L(1(0(2(x1))))
   1(2(0(x1))) -> 2(0(1(x1)))
   1(2(R(x1))) -> 2(0(1(R(x1))))
   0(2(0(x1))) -> 1(0(1(x1)))
   L(2(0(x1))) -> L(1(0(1(x1))))
   0(2(R(x1))) -> 1(0(1(R(x1))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [R](x0) = x0 + 1,
     
     [L](x0) = x0,
     
     [0](x0) = x0,
     
     [2](x0) = x0,
     
     [1](x0) = x0 + 1
    orientation:
     1(2(1(x1))) = x1 + 2 >= x1 = 2(0(2(x1)))
     
     0(2(1(x1))) = x1 + 1 >= x1 + 1 = 1(0(2(x1)))
     
     L(2(1(x1))) = x1 + 1 >= x1 + 1 = L(1(0(2(x1))))
     
     1(2(0(x1))) = x1 + 1 >= x1 + 1 = 2(0(1(x1)))
     
     1(2(R(x1))) = x1 + 2 >= x1 + 2 = 2(0(1(R(x1))))
     
     0(2(0(x1))) = x1 >= x1 + 2 = 1(0(1(x1)))
     
     L(2(0(x1))) = x1 >= x1 + 2 = L(1(0(1(x1))))
     
     0(2(R(x1))) = x1 + 1 >= x1 + 3 = 1(0(1(R(x1))))
    problem:
     strict:
      0(2(1(x1))) -> 1(0(2(x1)))
      L(2(1(x1))) -> L(1(0(2(x1))))
      1(2(0(x1))) -> 2(0(1(x1)))
      1(2(R(x1))) -> 2(0(1(R(x1))))
      0(2(0(x1))) -> 1(0(1(x1)))
      L(2(0(x1))) -> L(1(0(1(x1))))
      0(2(R(x1))) -> 1(0(1(R(x1))))
     weak:
      1(2(1(x1))) -> 2(0(2(x1)))
    Bounds Processor:
     bound: 1
     enrichment: match
     automaton:
      final states: {6}
      transitions:
       11(67) -> 68*
       11(234) -> 235*
       11(69) -> 70*
       11(236) -> 237*
       01(68) -> 69*
       21(137) -> 138*
       21(71) -> 72*
       L1(135) -> 136*
       R1(66) -> 67*
       00(6) -> 6*
       20(6) -> 6*
       10(6) -> 6*
       L0(6) -> 6*
       R0(6) -> 6*
       6 -> 234,137,66
       68 -> 236*
       69 -> 71*
       70 -> 69,135,6
       72 -> 237,235,6,68
       136 -> 6*
       138 -> 68*
       235 -> 68*
       237 -> 68*
     problem:
      strict:
       0(2(1(x1))) -> 1(0(2(x1)))
       L(2(1(x1))) -> L(1(0(2(x1))))
       1(2(0(x1))) -> 2(0(1(x1)))
       1(2(R(x1))) -> 2(0(1(R(x1))))
       0(2(0(x1))) -> 1(0(1(x1)))
       L(2(0(x1))) -> L(1(0(1(x1))))
      weak:
       0(2(R(x1))) -> 1(0(1(R(x1))))
       1(2(1(x1))) -> 2(0(2(x1)))
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {6}
       transitions:
        11(334) -> 335*
        11(107) -> 108*
        11(39) -> 40*
        11(71) -> 72*
        11(170) -> 171*
        11(130) -> 131*
        01(70) -> 71*
        01(40) -> 41*
        21(214) -> 215*
        21(69) -> 70*
        21(41) -> 42*
        21(317) -> 318*
        L1(72) -> 73*
        L1(158) -> 159*
        R1(38) -> 39*
        00(6) -> 6*
        20(6) -> 6*
        10(6) -> 6*
        L0(6) -> 6*
        R0(6) -> 6*
        6 -> 170,69,38
        40 -> 107*
        41 -> 130*
        42 -> 335,108,171,6
        70 -> 334*
        71 -> 317*
        72 -> 71*
        73 -> 6*
        108 -> 40*
        130 -> 214*
        131 -> 41,71,158,6
        159 -> 6*
        171 -> 40*
        215 -> 40*
        318 -> 335,171
        335 -> 40*
      problem:
       strict:
        0(2(1(x1))) -> 1(0(2(x1)))
        L(2(1(x1))) -> L(1(0(2(x1))))
        1(2(0(x1))) -> 2(0(1(x1)))
        0(2(0(x1))) -> 1(0(1(x1)))
        L(2(0(x1))) -> L(1(0(1(x1))))
       weak:
        1(2(R(x1))) -> 2(0(1(R(x1))))
        0(2(R(x1))) -> 1(0(1(R(x1))))
        1(2(1(x1))) -> 2(0(2(x1)))
      Bounds Processor:
       bound: 1
       enrichment: match
       automaton:
        final states: {6}
        transitions:
         11(212) -> 213*
         11(77) -> 78*
         11(22) -> 23*
         11(109) -> 110*
         11(296) -> 297*
         11(123) -> 124*
         01(21) -> 22*
         01(110) -> 111*
         21(20) -> 21*
         21(192) -> 193*
         21(111) -> 112*
         21(145) -> 146*
         L1(259) -> 260*
         L1(23) -> 24*
         R1(108) -> 109*
         00(6) -> 6*
         20(6) -> 6*
         10(6) -> 6*
         L0(6) -> 6*
         R0(6) -> 6*
         6 -> 108,77,20
         21 -> 296*
         22 -> 192*
         23 -> 6,22
         24 -> 6*
         78 -> 21*
         110 -> 212*
         111 -> 123*
         112 -> 297,78,6
         123 -> 145*
         124 -> 259,22,6
         146 -> 21*
         193 -> 297,6,78,21
         213 -> 110*
         260 -> 6*
         297 -> 21*
       problem:
        strict:
         0(2(1(x1))) -> 1(0(2(x1)))
         1(2(0(x1))) -> 2(0(1(x1)))
         0(2(0(x1))) -> 1(0(1(x1)))
         L(2(0(x1))) -> L(1(0(1(x1))))
        weak:
         L(2(1(x1))) -> L(1(0(2(x1))))
         1(2(R(x1))) -> 2(0(1(R(x1))))
         0(2(R(x1))) -> 1(0(1(R(x1))))
         1(2(1(x1))) -> 2(0(2(x1)))
       Bounds Processor:
        bound: 1
        enrichment: match
        automaton:
         final states: {6}
         transitions:
          11(36) -> 37*
          11(193) -> 194*
          11(143) -> 144*
          11(38) -> 39*
          11(110) -> 111*
          11(80) -> 81*
          01(37) -> 38*
          01(81) -> 82*
          21(82) -> 83*
          21(77) -> 78*
          21(41) -> 42*
          21(145) -> 146*
          L1(39) -> 40*
          L1(226) -> 227*
          R1(79) -> 80*
          00(6) -> 6*
          20(6) -> 6*
          10(6) -> 6*
          L0(6) -> 6*
          R0(6) -> 6*
          6 -> 79,77,36
          37 -> 193*
          38 -> 41*
          39 -> 82,6,38
          40 -> 6*
          42 -> 111,194,6,37
          78 -> 37*
          81 -> 110*
          82 -> 143*
          83 -> 194,37,6
          111 -> 37*
          143 -> 145*
          144 -> 226,38,6
          146 -> 81*
          194 -> 37*
          227 -> 6*
        problem:
         strict:
          0(2(1(x1))) -> 1(0(2(x1)))
          1(2(0(x1))) -> 2(0(1(x1)))
          0(2(0(x1))) -> 1(0(1(x1)))
         weak:
          L(2(0(x1))) -> L(1(0(1(x1))))
          L(2(1(x1))) -> L(1(0(2(x1))))
          1(2(R(x1))) -> 2(0(1(R(x1))))
          0(2(R(x1))) -> 1(0(1(R(x1))))
          1(2(1(x1))) -> 2(0(2(x1)))
        Open