YES

Problem:
 r1(a(x1)) -> a(a(a(r1(x1))))
 r2(a(x1)) -> a(a(a(r2(x1))))
 a(l1(x1)) -> l1(a(a(a(x1))))
 a(a(l2(x1))) -> l2(a(a(x1)))
 r1(b(x1)) -> l1(b(x1))
 r2(b(x1)) -> l2(a(b(x1)))
 b(l1(x1)) -> b(r2(x1))
 b(l2(x1)) -> b(r1(x1))
 a(a(x1)) -> x1

Proof:
 String Reversal Processor:
  a(r1(x1)) -> r1(a(a(a(x1))))
  a(r2(x1)) -> r2(a(a(a(x1))))
  l1(a(x1)) -> a(a(a(l1(x1))))
  l2(a(a(x1))) -> a(a(l2(x1)))
  b(r1(x1)) -> b(l1(x1))
  b(r2(x1)) -> b(a(l2(x1)))
  l1(b(x1)) -> r2(b(x1))
  l2(b(x1)) -> r1(b(x1))
  a(a(x1)) -> x1
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 1 0]     [0]
    [b](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [1],
    
               [1 0 1]  
    [l2](x0) = [0 1 1]x0
               [0 0 0]  ,
    
               [1 0 0]  
    [l1](x0) = [0 0 1]x0
               [0 1 0]  ,
    
               [1 0 0]  
    [r2](x0) = [0 0 1]x0
               [0 1 0]  ,
    
               [1 0 0]     [1]
    [r1](x0) = [0 0 1]x0 + [0]
               [0 1 0]     [0],
    
              [1 0 0]  
    [a](x0) = [0 0 1]x0
              [0 1 0]  
   orientation:
                     [1]         [1]                  
    a(r1(x1)) = x1 + [0] >= x1 + [0] = r1(a(a(a(x1))))
                     [0]         [0]                  
    
                                          
    a(r2(x1)) = x1 >= x1 = r2(a(a(a(x1))))
                                          
    
                                          
    l1(a(x1)) = x1 >= x1 = a(a(a(l1(x1))))
                                          
    
                   [1 0 1]      [1 0 1]                 
    l2(a(a(x1))) = [0 1 1]x1 >= [0 1 1]x1 = a(a(l2(x1)))
                   [0 0 0]      [0 0 0]                 
    
                [1 0 1]     [1]    [1 0 1]     [0]            
    b(r1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(l1(x1))
                [0 0 0]     [1]    [0 0 0]     [1]            
    
                [1 0 1]     [0]    [1 0 1]     [0]               
    b(r2(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(l2(x1)))
                [0 0 0]     [1]    [0 0 0]     [1]               
    
                [1 1 0]     [0]    [1 1 0]     [0]            
    l1(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r2(b(x1))
                [0 0 0]     [0]    [0 0 0]     [0]            
    
                [1 1 0]     [1]    [1 1 0]     [1]            
    l2(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r1(b(x1))
                [0 0 0]     [0]    [0 0 0]     [0]            
    
                            
    a(a(x1)) = x1 >= x1 = x1
                            
   problem:
    a(r1(x1)) -> r1(a(a(a(x1))))
    a(r2(x1)) -> r2(a(a(a(x1))))
    l1(a(x1)) -> a(a(a(l1(x1))))
    l2(a(a(x1))) -> a(a(l2(x1)))
    b(r2(x1)) -> b(a(l2(x1)))
    l1(b(x1)) -> r2(b(x1))
    l2(b(x1)) -> r1(b(x1))
    a(a(x1)) -> x1
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [b](x0) = x0,
     
     [l2](x0) = 2x0,
     
     [l1](x0) = 5x0,
     
     [r2](x0) = 2x0,
     
     [r1](x0) = x0,
     
     [a](x0) = x0
    orientation:
     a(r1(x1)) = x1 >= x1 = r1(a(a(a(x1))))
     
     a(r2(x1)) = 2x1 >= 2x1 = r2(a(a(a(x1))))
     
     l1(a(x1)) = 5x1 >= 5x1 = a(a(a(l1(x1))))
     
     l2(a(a(x1))) = 2x1 >= 2x1 = a(a(l2(x1)))
     
     b(r2(x1)) = 2x1 >= 2x1 = b(a(l2(x1)))
     
     l1(b(x1)) = 5x1 >= 2x1 = r2(b(x1))
     
     l2(b(x1)) = 2x1 >= x1 = r1(b(x1))
     
     a(a(x1)) = x1 >= x1 = x1
    problem:
     a(r1(x1)) -> r1(a(a(a(x1))))
     a(r2(x1)) -> r2(a(a(a(x1))))
     l1(a(x1)) -> a(a(a(l1(x1))))
     l2(a(a(x1))) -> a(a(l2(x1)))
     b(r2(x1)) -> b(a(l2(x1)))
     a(a(x1)) -> x1
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b](x0) = x0,
      
      [l2](x0) = x0,
      
      [l1](x0) = 5x0,
      
      [r2](x0) = 8x0,
      
      [r1](x0) = 4x0,
      
      [a](x0) = x0
     orientation:
      a(r1(x1)) = 4x1 >= 4x1 = r1(a(a(a(x1))))
      
      a(r2(x1)) = 8x1 >= 8x1 = r2(a(a(a(x1))))
      
      l1(a(x1)) = 5x1 >= 5x1 = a(a(a(l1(x1))))
      
      l2(a(a(x1))) = x1 >= x1 = a(a(l2(x1)))
      
      b(r2(x1)) = 8x1 >= x1 = b(a(l2(x1)))
      
      a(a(x1)) = x1 >= x1 = x1
     problem:
      a(r1(x1)) -> r1(a(a(a(x1))))
      a(r2(x1)) -> r2(a(a(a(x1))))
      l1(a(x1)) -> a(a(a(l1(x1))))
      l2(a(a(x1))) -> a(a(l2(x1)))
      a(a(x1)) -> x1
     String Reversal Processor:
      r1(a(x1)) -> a(a(a(r1(x1))))
      r2(a(x1)) -> a(a(a(r2(x1))))
      a(l1(x1)) -> l1(a(a(a(x1))))
      a(a(l2(x1))) -> l2(a(a(x1)))
      a(a(x1)) -> x1
      Matrix Interpretation Processor: dim=2
       
       interpretation:
                   [1 0]  
        [l2](x0) = [2 1]x0,
        
                   [1 0]     [0]
        [l1](x0) = [0 0]x0 + [3],
        
                   [2 1]     [0]
        [r2](x0) = [1 3]x0 + [1],
        
                   [2 0]     [0]
        [r1](x0) = [0 3]x0 + [2],
        
                       [0]
        [a](x0) = x0 + [1]
       orientation:
                    [2 0]     [0]    [2 0]     [0]                  
        r1(a(x1)) = [0 3]x1 + [5] >= [0 3]x1 + [5] = a(a(a(r1(x1))))
        
                    [2 1]     [1]    [2 1]     [0]                  
        r2(a(x1)) = [1 3]x1 + [4] >= [1 3]x1 + [4] = a(a(a(r2(x1))))
        
                    [1 0]     [0]    [1 0]     [0]                  
        a(l1(x1)) = [0 0]x1 + [4] >= [0 0]x1 + [3] = l1(a(a(a(x1))))
        
                       [1 0]     [0]    [1 0]     [0]               
        a(a(l2(x1))) = [2 1]x1 + [2] >= [2 1]x1 + [2] = l2(a(a(x1)))
        
                        [0]           
        a(a(x1)) = x1 + [2] >= x1 = x1
       problem:
        r1(a(x1)) -> a(a(a(r1(x1))))
        a(l1(x1)) -> l1(a(a(a(x1))))
        a(a(l2(x1))) -> l2(a(a(x1)))
        a(a(x1)) -> x1
       String Reversal Processor:
        a(r1(x1)) -> r1(a(a(a(x1))))
        l1(a(x1)) -> a(a(a(l1(x1))))
        l2(a(a(x1))) -> a(a(l2(x1)))
        a(a(x1)) -> x1
        Matrix Interpretation Processor: dim=2
         
         interpretation:
                     [1 0]     [0]
          [l2](x0) = [0 2]x0 + [2],
          
                     [2 2]     [1]
          [l1](x0) = [1 3]x0 + [3],
          
                     [2 0]     [0]
          [r1](x0) = [0 0]x0 + [3],
          
                         [0]
          [a](x0) = x0 + [1]
         orientation:
                      [2 0]     [0]    [2 0]     [0]                  
          a(r1(x1)) = [0 0]x1 + [4] >= [0 0]x1 + [3] = r1(a(a(a(x1))))
          
                      [2 2]     [3]    [2 2]     [1]                  
          l1(a(x1)) = [1 3]x1 + [6] >= [1 3]x1 + [6] = a(a(a(l1(x1))))
          
                         [1 0]     [0]    [1 0]     [0]               
          l2(a(a(x1))) = [0 2]x1 + [6] >= [0 2]x1 + [4] = a(a(l2(x1)))
          
                          [0]           
          a(a(x1)) = x1 + [2] >= x1 = x1
         problem:
          a(r1(x1)) -> r1(a(a(a(x1))))
          l2(a(a(x1))) -> a(a(l2(x1)))
          a(a(x1)) -> x1
         String Reversal Processor:
          r1(a(x1)) -> a(a(a(r1(x1))))
          a(a(l2(x1))) -> l2(a(a(x1)))
          a(a(x1)) -> x1
          Bounds Processor:
           bound: 0
           enrichment: match
           automaton:
            final states: {2,6,1}
            transitions:
             f60() -> 2*
             a0(5) -> 1*
             a0(7) -> 8*
             a0(2) -> 7*
             a0(4) -> 5*
             a0(3) -> 4*
             r10(2) -> 3*
             l20(8) -> 6*
             1 -> 3,5
             2 -> 7,8
             3 -> 5*
             4 -> 1*
             5 -> 4,1
             6 -> 7,8
           problem:
            
           Qed