YES(?,O(n^2))

Problem:
 1(q0(1(x1))) -> 0(1(q1(x1)))
 1(q0(0(x1))) -> 0(0(q1(x1)))
 1(q1(1(x1))) -> 1(1(q1(x1)))
 1(q1(0(x1))) -> 1(0(q1(x1)))
 0(q1(x1)) -> q2(1(x1))
 1(q2(x1)) -> q2(1(x1))
 0(q2(x1)) -> 0(q0(x1))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                   [11]
   [q2](x0) = x0 + [1 ],
   
                  [8]
   [0](x0) = x0 + [8],
   
              [1 1]     [6]
   [q1](x0) = [0 1]x0 + [1],
   
                   [7]
   [q0](x0) = x0 + [1],
   
             [1 1]     [0]
   [1](x0) = [0 1]x0 + [8]
  orientation:
                  [1 2]     [16]    [1 2]     [15]               
   1(q0(1(x1))) = [0 1]x1 + [17] >= [0 1]x1 + [17] = 0(1(q1(x1)))
   
                  [1 1]     [24]    [1 1]     [22]               
   1(q0(0(x1))) = [0 1]x1 + [17] >= [0 1]x1 + [17] = 0(0(q1(x1)))
   
                  [1 3]     [23]    [1 3]     [16]               
   1(q1(1(x1))) = [0 1]x1 + [17] >= [0 1]x1 + [17] = 1(1(q1(x1)))
   
                  [1 2]     [31]    [1 2]     [23]               
   1(q1(0(x1))) = [0 1]x1 + [17] >= [0 1]x1 + [17] = 1(0(q1(x1)))
   
               [1 1]     [14]    [1 1]     [11]            
   0(q1(x1)) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(1(x1))
   
               [1 1]     [12]    [1 1]     [11]            
   1(q2(x1)) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(1(x1))
   
                    [19]         [15]            
   0(q2(x1)) = x1 + [9 ] >= x1 + [9 ] = 0(q0(x1))
  problem:
   
  Qed