YES(?,O(n^2))

Problem:
 q0(0(x1)) -> 0'(q1(x1))
 q1(0(x1)) -> 0(q1(x1))
 q1(1'(x1)) -> 1'(q1(x1))
 0(q1(1(x1))) -> q2(0(1'(x1)))
 0'(q1(1(x1))) -> q2(0'(1'(x1)))
 1'(q1(1(x1))) -> q2(1'(1'(x1)))
 0(q2(0(x1))) -> q2(0(0(x1)))
 0'(q2(0(x1))) -> q2(0'(0(x1)))
 1'(q2(0(x1))) -> q2(1'(0(x1)))
 0(q2(1'(x1))) -> q2(0(1'(x1)))
 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
 q2(0'(x1)) -> 0'(q0(x1))
 q0(1'(x1)) -> 1'(q3(x1))
 q3(1'(x1)) -> 1'(q3(x1))
 q3(b(x1)) -> b(q4(x1))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
              [1 2]     [2]
   [q4](x0) = [0 0]x0 + [0],
   
             [1 1]     [4]
   [b](x0) = [0 1]x0 + [3],
   
              [1 1]  
   [q3](x0) = [0 1]x0,
   
              [1 2]     [1]
   [q2](x0) = [0 1]x0 + [3],
   
             [1 3]     [2]
   [1](x0) = [0 1]x0 + [5],
   
              [1 2]     [0]
   [1'](x0) = [0 1]x0 + [2],
   
              [1 1]  
   [0'](x0) = [0 1]x0,
   
              [1 1]     [1]
   [q1](x0) = [0 1]x0 + [0],
   
              [1 1]  
   [q0](x0) = [0 1]x0,
   
             [1 3]     [0]
   [0](x0) = [0 1]x0 + [4]
  orientation:
               [1 4]     [4]    [1 2]     [1]             
   q0(0(x1)) = [0 1]x1 + [4] >= [0 1]x1 + [0] = 0'(q1(x1))
   
               [1 4]     [5]    [1 4]     [1]            
   q1(0(x1)) = [0 1]x1 + [4] >= [0 1]x1 + [4] = 0(q1(x1))
   
                [1 3]     [3]    [1 3]     [1]             
   q1(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1'(q1(x1))
   
                  [1 7]     [23]    [1 7]     [19]                
   0(q1(1(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(0(1'(x1)))
   
                   [1 5]     [13]    [1 5]     [7]                 
   0'(q1(1(x1))) = [0 1]x1 + [5 ] >= [0 1]x1 + [5] = q2(0'(1'(x1)))
   
                   [1 6]     [18]    [1 6]     [13]                 
   1'(q1(1(x1))) = [0 1]x1 + [7 ] >= [0 1]x1 + [7 ] = q2(1'(1'(x1)))
   
                  [1 8]     [30]    [1 8]     [29]               
   0(q2(0(x1))) = [0 1]x1 + [11] >= [0 1]x1 + [11] = q2(0(0(x1)))
   
                   [1 6]     [16]    [1 6]     [13]                
   0'(q2(0(x1))) = [0 1]x1 + [7 ] >= [0 1]x1 + [7 ] = q2(0'(0(x1)))
   
                   [1 7]     [23]    [1 7]     [21]                
   1'(q2(0(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(1'(0(x1)))
   
                   [1 7]     [20]    [1 7]     [19]                
   0(q2(1'(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(0(1'(x1)))
   
                    [1 5]     [10]    [1 5]     [7]                 
   0'(q2(1'(x1))) = [0 1]x1 + [5 ] >= [0 1]x1 + [5] = q2(0'(1'(x1)))
   
                    [1 6]     [15]    [1 6]     [13]                 
   1'(q2(1'(x1))) = [0 1]x1 + [7 ] >= [0 1]x1 + [7 ] = q2(1'(1'(x1)))
   
                [1 3]     [1]    [1 2]               
   q2(0'(x1)) = [0 1]x1 + [3] >= [0 1]x1 = 0'(q0(x1))
   
                [1 3]     [2]    [1 3]     [0]             
   q0(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1'(q3(x1))
   
                [1 3]     [2]    [1 3]     [0]             
   q3(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1'(q3(x1))
   
               [1 2]     [7]    [1 2]     [6]            
   q3(b(x1)) = [0 1]x1 + [3] >= [0 0]x1 + [3] = b(q4(x1))
  problem:
   
  Qed