YES(?,O(n^2))

Problem:
 q0(a(x1)) -> x(q1(x1))
 q1(a(x1)) -> a(q1(x1))
 q1(y(x1)) -> y(q1(x1))
 a(q1(b(x1))) -> q2(a(y(x1)))
 a(q2(a(x1))) -> q2(a(a(x1)))
 a(q2(y(x1))) -> q2(a(y(x1)))
 y(q1(b(x1))) -> q2(y(y(x1)))
 y(q2(a(x1))) -> q2(y(a(x1)))
 y(q2(y(x1))) -> q2(y(y(x1)))
 q2(x(x1)) -> x(q0(x1))
 q0(y(x1)) -> y(q3(x1))
 q3(y(x1)) -> y(q3(x1))
 q3(bl(x1)) -> bl(q4(x1))

Proof:
 RT Transformation Processor:
  strict:
   q0(a(x1)) -> x(q1(x1))
   q1(a(x1)) -> a(q1(x1))
   q1(y(x1)) -> y(q1(x1))
   a(q1(b(x1))) -> q2(a(y(x1)))
   a(q2(a(x1))) -> q2(a(a(x1)))
   a(q2(y(x1))) -> q2(a(y(x1)))
   y(q1(b(x1))) -> q2(y(y(x1)))
   y(q2(a(x1))) -> q2(y(a(x1)))
   y(q2(y(x1))) -> q2(y(y(x1)))
   q2(x(x1)) -> x(q0(x1))
   q0(y(x1)) -> y(q3(x1))
   q3(y(x1)) -> y(q3(x1))
   q3(bl(x1)) -> bl(q4(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [q4](x0) = x0 + 8,
    
    [bl](x0) = x0 + 28,
    
    [q3](x0) = x0 + 9,
    
    [q2](x0) = x0 + 3,
    
    [b](x0) = x0 + 16,
    
    [y](x0) = x0,
    
    [x](x0) = x0 + 1,
    
    [q1](x0) = x0,
    
    [q0](x0) = x0 + 24,
    
    [a](x0) = x0 + 17
   orientation:
    q0(a(x1)) = x1 + 41 >= x1 + 1 = x(q1(x1))
    
    q1(a(x1)) = x1 + 17 >= x1 + 17 = a(q1(x1))
    
    q1(y(x1)) = x1 >= x1 = y(q1(x1))
    
    a(q1(b(x1))) = x1 + 33 >= x1 + 20 = q2(a(y(x1)))
    
    a(q2(a(x1))) = x1 + 37 >= x1 + 37 = q2(a(a(x1)))
    
    a(q2(y(x1))) = x1 + 20 >= x1 + 20 = q2(a(y(x1)))
    
    y(q1(b(x1))) = x1 + 16 >= x1 + 3 = q2(y(y(x1)))
    
    y(q2(a(x1))) = x1 + 20 >= x1 + 20 = q2(y(a(x1)))
    
    y(q2(y(x1))) = x1 + 3 >= x1 + 3 = q2(y(y(x1)))
    
    q2(x(x1)) = x1 + 4 >= x1 + 25 = x(q0(x1))
    
    q0(y(x1)) = x1 + 24 >= x1 + 9 = y(q3(x1))
    
    q3(y(x1)) = x1 + 9 >= x1 + 9 = y(q3(x1))
    
    q3(bl(x1)) = x1 + 37 >= x1 + 36 = bl(q4(x1))
   problem:
    strict:
     q1(a(x1)) -> a(q1(x1))
     q1(y(x1)) -> y(q1(x1))
     a(q2(a(x1))) -> q2(a(a(x1)))
     a(q2(y(x1))) -> q2(a(y(x1)))
     y(q2(a(x1))) -> q2(y(a(x1)))
     y(q2(y(x1))) -> q2(y(y(x1)))
     q2(x(x1)) -> x(q0(x1))
     q3(y(x1)) -> y(q3(x1))
    weak:
     q0(a(x1)) -> x(q1(x1))
     a(q1(b(x1))) -> q2(a(y(x1)))
     y(q1(b(x1))) -> q2(y(y(x1)))
     q0(y(x1)) -> y(q3(x1))
     q3(bl(x1)) -> bl(q4(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [q4](x0) = x0,
     
     [bl](x0) = x0 + 13,
     
     [q3](x0) = x0 + 3,
     
     [q2](x0) = x0 + 4,
     
     [b](x0) = x0 + 9,
     
     [y](x0) = x0 + 4,
     
     [x](x0) = x0 + 2,
     
     [q1](x0) = x0,
     
     [q0](x0) = x0 + 3,
     
     [a](x0) = x0 + 22
    orientation:
     q1(a(x1)) = x1 + 22 >= x1 + 22 = a(q1(x1))
     
     q1(y(x1)) = x1 + 4 >= x1 + 4 = y(q1(x1))
     
     a(q2(a(x1))) = x1 + 48 >= x1 + 48 = q2(a(a(x1)))
     
     a(q2(y(x1))) = x1 + 30 >= x1 + 30 = q2(a(y(x1)))
     
     y(q2(a(x1))) = x1 + 30 >= x1 + 30 = q2(y(a(x1)))
     
     y(q2(y(x1))) = x1 + 12 >= x1 + 12 = q2(y(y(x1)))
     
     q2(x(x1)) = x1 + 6 >= x1 + 5 = x(q0(x1))
     
     q3(y(x1)) = x1 + 7 >= x1 + 7 = y(q3(x1))
     
     q0(a(x1)) = x1 + 25 >= x1 + 2 = x(q1(x1))
     
     a(q1(b(x1))) = x1 + 31 >= x1 + 30 = q2(a(y(x1)))
     
     y(q1(b(x1))) = x1 + 13 >= x1 + 12 = q2(y(y(x1)))
     
     q0(y(x1)) = x1 + 7 >= x1 + 7 = y(q3(x1))
     
     q3(bl(x1)) = x1 + 16 >= x1 + 13 = bl(q4(x1))
    problem:
     strict:
      q1(a(x1)) -> a(q1(x1))
      q1(y(x1)) -> y(q1(x1))
      a(q2(a(x1))) -> q2(a(a(x1)))
      a(q2(y(x1))) -> q2(a(y(x1)))
      y(q2(a(x1))) -> q2(y(a(x1)))
      y(q2(y(x1))) -> q2(y(y(x1)))
      q3(y(x1)) -> y(q3(x1))
     weak:
      q2(x(x1)) -> x(q0(x1))
      q0(a(x1)) -> x(q1(x1))
      a(q1(b(x1))) -> q2(a(y(x1)))
      y(q1(b(x1))) -> q2(y(y(x1)))
      q0(y(x1)) -> y(q3(x1))
      q3(bl(x1)) -> bl(q4(x1))
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                 [1  10]  
      [q4](x0) = [0  0 ]x0,
      
                 [1  11]     [3]
      [bl](x0) = [0  0 ]x0 + [0],
      
                 [1 0]  
      [q3](x0) = [0 0]x0,
      
                      [0]
      [q2](x0) = x0 + [2],
      
                [1 8]     [1]
      [b](x0) = [0 1]x0 + [8],
      
                  
      [y](x0) = x0,
      
                [1 8]  
      [x](x0) = [0 0]x0,
      
                   
      [q1](x0) = x0,
      
                 [1 6]  
      [q0](x0) = [0 0]x0,
      
                [1 2]  
      [a](x0) = [0 1]x0
     orientation:
                  [1 2]      [1 2]              
      q1(a(x1)) = [0 1]x1 >= [0 1]x1 = a(q1(x1))
      
                                      
      q1(y(x1)) = x1 >= x1 = y(q1(x1))
      
                     [1 4]     [4]    [1 4]     [0]               
      a(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(a(x1)))
      
                     [1 2]     [4]    [1 2]     [0]               
      a(q2(y(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(y(x1)))
      
                     [1 2]     [0]    [1 2]     [0]               
      y(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(y(a(x1)))
      
                          [0]         [0]               
      y(q2(y(x1))) = x1 + [2] >= x1 + [2] = q2(y(y(x1)))
      
                  [1 0]      [1 0]              
      q3(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
      
                  [1 8]     [0]    [1 6]              
      q2(x(x1)) = [0 0]x1 + [2] >= [0 0]x1 = x(q0(x1))
      
                  [1 8]      [1 8]              
      q0(a(x1)) = [0 0]x1 >= [0 0]x1 = x(q1(x1))
      
                     [1  10]     [17]    [1 2]     [0]               
      a(q1(b(x1))) = [0  1 ]x1 + [8 ] >= [0 1]x1 + [2] = q2(a(y(x1)))
      
                     [1 8]     [1]         [0]               
      y(q1(b(x1))) = [0 1]x1 + [8] >= x1 + [2] = q2(y(y(x1)))
      
                  [1 6]      [1 0]              
      q0(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
      
                   [1  11]     [3]    [1  10]     [3]             
      q3(bl(x1)) = [0  0 ]x1 + [0] >= [0  0 ]x1 + [0] = bl(q4(x1))
     problem:
      strict:
       q1(a(x1)) -> a(q1(x1))
       q1(y(x1)) -> y(q1(x1))
       y(q2(a(x1))) -> q2(y(a(x1)))
       y(q2(y(x1))) -> q2(y(y(x1)))
       q3(y(x1)) -> y(q3(x1))
      weak:
       a(q2(a(x1))) -> q2(a(a(x1)))
       a(q2(y(x1))) -> q2(a(y(x1)))
       q2(x(x1)) -> x(q0(x1))
       q0(a(x1)) -> x(q1(x1))
       a(q1(b(x1))) -> q2(a(y(x1)))
       y(q1(b(x1))) -> q2(y(y(x1)))
       q0(y(x1)) -> y(q3(x1))
       q3(bl(x1)) -> bl(q4(x1))
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                  [1 5]     [13]
       [q4](x0) = [0 1]x0 + [1 ],
       
                  [1 3]     [2]
       [bl](x0) = [0 1]x0 + [2],
       
                  [1 8]     [8]
       [q3](x0) = [0 1]x0 + [1],
       
                  [1 8]     [0]
       [q2](x0) = [0 1]x0 + [4],
       
                 [1  11]     [8]
       [b](x0) = [0  1 ]x0 + [5],
       
                 [1 2]     [0]
       [y](x0) = [0 1]x0 + [1],
       
                 [1 8]     [0]
       [x](x0) = [0 1]x0 + [3],
       
                       [2]
       [q1](x0) = x0 + [0],
       
                  [1 8]     [3]
       [q0](x0) = [0 1]x0 + [2],
       
                 [1 4]     [0]
       [a](x0) = [0 1]x0 + [1]
      orientation:
                   [1 4]     [2]    [1 4]     [2]            
       q1(a(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(q1(x1))
       
                   [1 2]     [2]    [1 2]     [2]            
       q1(y(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = y(q1(x1))
       
                      [1  14]     [18]    [1  14]     [18]               
       y(q2(a(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(y(a(x1)))
       
                      [1  12]     [18]    [1  12]     [18]               
       y(q2(y(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(y(y(x1)))
       
                   [1  10]     [16]    [1  10]     [10]            
       q3(y(x1)) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2 ] = y(q3(x1))
       
                      [1  16]     [28]    [1  16]     [20]               
       a(q2(a(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(a(a(x1)))
       
                      [1  14]     [28]    [1  14]     [20]               
       a(q2(y(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(a(y(x1)))
       
                   [1  16]     [24]    [1  16]     [19]            
       q2(x(x1)) = [0  1 ]x1 + [7 ] >= [0  1 ]x1 + [5 ] = x(q0(x1))
       
                   [1  12]     [11]    [1 8]     [2]            
       q0(a(x1)) = [0  1 ]x1 + [3 ] >= [0 1]x1 + [3] = x(q1(x1))
       
                      [1  15]     [30]    [1  14]     [20]               
       a(q1(b(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(a(y(x1)))
       
                      [1  13]     [20]    [1  12]     [18]               
       y(q1(b(x1))) = [0  1 ]x1 + [6 ] >= [0  1 ]x1 + [6 ] = q2(y(y(x1)))
       
                   [1  10]     [11]    [1  10]     [10]            
       q0(y(x1)) = [0  1 ]x1 + [3 ] >= [0  1 ]x1 + [2 ] = y(q3(x1))
       
                    [1  11]     [26]    [1 8]     [18]             
       q3(bl(x1)) = [0  1 ]x1 + [3 ] >= [0 1]x1 + [3 ] = bl(q4(x1))
      problem:
       strict:
        q1(a(x1)) -> a(q1(x1))
        q1(y(x1)) -> y(q1(x1))
        y(q2(a(x1))) -> q2(y(a(x1)))
        y(q2(y(x1))) -> q2(y(y(x1)))
       weak:
        q3(y(x1)) -> y(q3(x1))
        a(q2(a(x1))) -> q2(a(a(x1)))
        a(q2(y(x1))) -> q2(a(y(x1)))
        q2(x(x1)) -> x(q0(x1))
        q0(a(x1)) -> x(q1(x1))
        a(q1(b(x1))) -> q2(a(y(x1)))
        y(q1(b(x1))) -> q2(y(y(x1)))
        q0(y(x1)) -> y(q3(x1))
        q3(bl(x1)) -> bl(q4(x1))
      Matrix Interpretation Processor:
       dimension: 2
       interpretation:
                   [1 1]  
        [q4](x0) = [0 0]x0,
        
                   [1 8]     [4]
        [bl](x0) = [0 0]x0 + [2],
        
                     
        [q3](x0) = x0,
        
                   [1 4]     [0 ]
        [q2](x0) = [0 1]x0 + [10],
        
                  [1  10]     [15]
        [b](x0) = [0  1 ]x0 + [12],
        
                  [1 1]     [0]
        [y](x0) = [0 1]x0 + [2],
        
                  [1 0]     [3]
        [x](x0) = [0 0]x0 + [7],
        
                        [1]
        [q1](x0) = x0 + [0],
        
                        [1]
        [q0](x0) = x0 + [7],
        
                       [8]
        [a](x0) = x0 + [0]
       orientation:
                         [9]         [9]            
        q1(a(x1)) = x1 + [0] >= x1 + [0] = a(q1(x1))
        
                    [1 1]     [1]    [1 1]     [1]            
        q1(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = y(q1(x1))
        
                       [1 5]     [18]    [1 5]     [16]               
        y(q2(a(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [12] = q2(y(a(x1)))
        
                       [1 6]     [20]    [1 6]     [18]               
        y(q2(y(x1))) = [0 1]x1 + [14] >= [0 1]x1 + [14] = q2(y(y(x1)))
        
                    [1 1]     [0]    [1 1]     [0]            
        q3(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = y(q3(x1))
        
                       [1 4]     [16]    [1 4]     [16]               
        a(q2(a(x1))) = [0 1]x1 + [10] >= [0 1]x1 + [10] = q2(a(a(x1)))
        
                       [1 5]     [16]    [1 5]     [16]               
        a(q2(y(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [12] = q2(a(y(x1)))
        
                    [1 0]     [31]    [1 0]     [4]            
        q2(x(x1)) = [0 0]x1 + [17] >= [0 0]x1 + [7] = x(q0(x1))
        
                         [9]    [1 0]     [4]            
        q0(a(x1)) = x1 + [7] >= [0 0]x1 + [7] = x(q1(x1))
        
                       [1  10]     [24]    [1 5]     [16]               
        a(q1(b(x1))) = [0  1 ]x1 + [12] >= [0 1]x1 + [12] = q2(a(y(x1)))
        
                       [1  11]     [28]    [1 6]     [18]               
        y(q1(b(x1))) = [0  1 ]x1 + [14] >= [0 1]x1 + [14] = q2(y(y(x1)))
        
                    [1 1]     [1]    [1 1]     [0]            
        q0(y(x1)) = [0 1]x1 + [9] >= [0 1]x1 + [2] = y(q3(x1))
        
                     [1 8]     [4]    [1 1]     [4]             
        q3(bl(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = bl(q4(x1))
       problem:
        strict:
         q1(a(x1)) -> a(q1(x1))
         q1(y(x1)) -> y(q1(x1))
        weak:
         y(q2(a(x1))) -> q2(y(a(x1)))
         y(q2(y(x1))) -> q2(y(y(x1)))
         q3(y(x1)) -> y(q3(x1))
         a(q2(a(x1))) -> q2(a(a(x1)))
         a(q2(y(x1))) -> q2(a(y(x1)))
         q2(x(x1)) -> x(q0(x1))
         q0(a(x1)) -> x(q1(x1))
         a(q1(b(x1))) -> q2(a(y(x1)))
         y(q1(b(x1))) -> q2(y(y(x1)))
         q0(y(x1)) -> y(q3(x1))
         q3(bl(x1)) -> bl(q4(x1))
       Matrix Interpretation Processor:
        dimension: 2
        interpretation:
                    [1  12]  
         [q4](x0) = [0  0 ]x0,
         
                    [1  12]     [5]
         [bl](x0) = [0  0 ]x0 + [1],
         
                         [0]
         [q3](x0) = x0 + [2],
         
                      
         [q2](x0) = x0,
         
                   [1  13]     [3]
         [b](x0) = [0  1 ]x0 + [1],
         
                        [7]
         [y](x0) = x0 + [5],
         
                   [1 0]  
         [x](x0) = [0 0]x0,
         
                    [1 4]     [1]
         [q1](x0) = [0 1]x0 + [4],
         
                         [0]
         [q0](x0) = x0 + [5],
         
                   [1 4]     [1]
         [a](x0) = [0 1]x0 + [4]
        orientation:
                     [1 8]     [18]    [1 8]     [18]            
         q1(a(x1)) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = a(q1(x1))
         
                     [1 4]     [28]    [1 4]     [8]            
         q1(y(x1)) = [0 1]x1 + [9 ] >= [0 1]x1 + [9] = y(q1(x1))
         
                        [1 4]     [8]    [1 4]     [8]               
         y(q2(a(x1))) = [0 1]x1 + [9] >= [0 1]x1 + [9] = q2(y(a(x1)))
         
                             [14]         [14]               
         y(q2(y(x1))) = x1 + [10] >= x1 + [10] = q2(y(y(x1)))
         
                          [7]         [7]            
         q3(y(x1)) = x1 + [7] >= x1 + [7] = y(q3(x1))
         
                        [1 8]     [18]    [1 8]     [18]               
         a(q2(a(x1))) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = q2(a(a(x1)))
         
                        [1 4]     [28]    [1 4]     [28]               
         a(q2(y(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(a(y(x1)))
         
                     [1 0]      [1 0]              
         q2(x(x1)) = [0 0]x1 >= [0 0]x1 = x(q0(x1))
         
                     [1 4]     [1]    [1 4]     [1]            
         q0(a(x1)) = [0 1]x1 + [9] >= [0 0]x1 + [0] = x(q1(x1))
         
                        [1  21]     [29]    [1 4]     [28]               
         a(q1(b(x1))) = [0  1 ]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(a(y(x1)))
         
                        [1  17]     [15]         [14]               
         y(q1(b(x1))) = [0  1 ]x1 + [10] >= x1 + [10] = q2(y(y(x1)))
         
                          [7 ]         [7]            
         q0(y(x1)) = x1 + [10] >= x1 + [7] = y(q3(x1))
         
                      [1  12]     [5]    [1  12]     [5]             
         q3(bl(x1)) = [0  0 ]x1 + [3] >= [0  0 ]x1 + [1] = bl(q4(x1))
        problem:
         strict:
          q1(a(x1)) -> a(q1(x1))
         weak:
          q1(y(x1)) -> y(q1(x1))
          y(q2(a(x1))) -> q2(y(a(x1)))
          y(q2(y(x1))) -> q2(y(y(x1)))
          q3(y(x1)) -> y(q3(x1))
          a(q2(a(x1))) -> q2(a(a(x1)))
          a(q2(y(x1))) -> q2(a(y(x1)))
          q2(x(x1)) -> x(q0(x1))
          q0(a(x1)) -> x(q1(x1))
          a(q1(b(x1))) -> q2(a(y(x1)))
          y(q1(b(x1))) -> q2(y(y(x1)))
          q0(y(x1)) -> y(q3(x1))
          q3(bl(x1)) -> bl(q4(x1))
        Matrix Interpretation Processor:
         dimension: 2
         interpretation:
                     [1 0]  
          [q4](x0) = [0 0]x0,
          
                     [1 6]     [2]
          [bl](x0) = [0 0]x0 + [0],
          
                       
          [q3](x0) = x0,
          
                          [9]
          [q2](x0) = x0 + [0],
          
                         [10]
          [b](x0) = x0 + [1 ],
          
                    [1 2]     [0]
          [y](x0) = [0 1]x0 + [8],
          
                    [1 0]     [4]
          [x](x0) = [0 0]x0 + [4],
          
                     [1 2]     [2]
          [q1](x0) = [0 1]x0 + [7],
          
                          [8]
          [q0](x0) = x0 + [1],
          
                    [1 2]     [0]
          [a](x0) = [0 1]x0 + [8]
         orientation:
                      [1 4]     [18]    [1 4]     [16]            
          q1(a(x1)) = [0 1]x1 + [15] >= [0 1]x1 + [15] = a(q1(x1))
          
                      [1 4]     [18]    [1 4]     [16]            
          q1(y(x1)) = [0 1]x1 + [15] >= [0 1]x1 + [15] = y(q1(x1))
          
                         [1 4]     [25]    [1 4]     [25]               
          y(q2(a(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(a(x1)))
          
                         [1 4]     [25]    [1 4]     [25]               
          y(q2(y(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(y(x1)))
          
                      [1 2]     [0]    [1 2]     [0]            
          q3(y(x1)) = [0 1]x1 + [8] >= [0 1]x1 + [8] = y(q3(x1))
          
                         [1 4]     [25]    [1 4]     [25]               
          a(q2(a(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(a(x1)))
          
                         [1 4]     [25]    [1 4]     [25]               
          a(q2(y(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(y(x1)))
          
                      [1 0]     [13]    [1 0]     [12]            
          q2(x(x1)) = [0 0]x1 + [4 ] >= [0 0]x1 + [4 ] = x(q0(x1))
          
                      [1 2]     [8]    [1 2]     [6]            
          q0(a(x1)) = [0 1]x1 + [9] >= [0 0]x1 + [4] = x(q1(x1))
          
                         [1 4]     [30]    [1 4]     [25]               
          a(q1(b(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(y(x1)))
          
                         [1 4]     [30]    [1 4]     [25]               
          y(q1(b(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(y(x1)))
          
                      [1 2]     [8]    [1 2]     [0]            
          q0(y(x1)) = [0 1]x1 + [9] >= [0 1]x1 + [8] = y(q3(x1))
          
                       [1 6]     [2]    [1 0]     [2]             
          q3(bl(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
         problem:
          strict:
           
          weak:
           q1(a(x1)) -> a(q1(x1))
           q1(y(x1)) -> y(q1(x1))
           y(q2(a(x1))) -> q2(y(a(x1)))
           y(q2(y(x1))) -> q2(y(y(x1)))
           q3(y(x1)) -> y(q3(x1))
           a(q2(a(x1))) -> q2(a(a(x1)))
           a(q2(y(x1))) -> q2(a(y(x1)))
           q2(x(x1)) -> x(q0(x1))
           q0(a(x1)) -> x(q1(x1))
           a(q1(b(x1))) -> q2(a(y(x1)))
           y(q1(b(x1))) -> q2(y(y(x1)))
           q0(y(x1)) -> y(q3(x1))
           q3(bl(x1)) -> bl(q4(x1))
         Qed