YES

Problem:
 a(a(x1)) -> b(a(b(x1)))
 a(a(a(x1))) -> a(b(a(b(a(x1)))))
 a(b(a(x1))) -> b(b(a(b(b(x1)))))
 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1)))))))
 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1)))))))
 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1)))))))
 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1)))))))
 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1)))))))))
 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1)))))))))
 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1)))))))))
 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1)))))))))
 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1)))))))))
 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1)))))))))
 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1)))))))))
 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1)))))))))

Proof:
 String Reversal Processor:
  a(a(x1)) -> b(a(b(x1)))
  a(a(a(x1))) -> a(b(a(b(a(x1)))))
  a(b(a(x1))) -> b(b(a(b(b(x1)))))
  a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1)))))))
  a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1)))))))
  a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1)))))))
  a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1)))))))
  a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1)))))))))
  a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1)))))))))
  a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1)))))))))
  a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1)))))))))
  a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1)))))))))
  a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1)))))))))
  a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1)))))))))
  a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1)))))))))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
              [1 0]  
    [b](x0) = [0 0]x0,
    
              [1 1]     [0]
    [a](x0) = [0 0]x0 + [1]
   orientation:
               [1 1]     [1]    [1 0]                
    a(a(x1)) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(x1)))
    
                  [1 1]     [2]    [1 1]     [0]                    
    a(a(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(a(b(a(x1)))))
    
                  [1 1]     [0]    [1 0]                      
    a(b(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(a(b(b(x1)))))
    
                     [1 1]     [3]    [1 1]     [2]                          
    a(a(a(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(b(a(b(a(a(x1)))))))
    
                     [1 1]     [1]    [1 1]                            
    a(b(a(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(a(b(b(a(x1)))))))
    
                     [1 1]     [1]    [1 0]     [0]                          
    a(a(b(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(b(a(b(a(b(x1)))))))
    
                     [1 1]     [0]    [1 0]                            
    a(b(b(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(a(b(b(b(x1)))))))
    
                        [1 1]     [4]    [1 1]     [4]                                
    a(a(a(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(a(b(a(b(a(a(a(x1)))))))))
    
                        [1 1]     [2]    [1 1]     [2]                                
    a(b(a(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = b(a(a(b(a(b(b(a(a(x1)))))))))
    
                        [1 1]     [2]    [1 1]     [0]                                
    a(a(b(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(a(b(a(b(a(b(a(x1)))))))))
    
                        [1 1]     [1]    [1 1]                                  
    a(b(b(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(a(b(a(b(b(b(a(x1)))))))))
    
                        [1 1]     [2]    [1 0]     [2]                                
    a(a(a(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(b(b(a(b(a(a(b(x1)))))))))
    
                        [1 1]     [0]    [1 0]                                  
    a(b(a(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(b(a(b(b(a(b(x1)))))))))
    
                        [1 1]     [1]    [1 0]     [0]                                
    a(a(b(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(b(b(a(b(a(b(b(x1)))))))))
    
                        [1 1]     [0]    [1 0]                                  
    a(b(b(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(b(a(b(b(b(b(x1)))))))))
   problem:
    a(b(a(x1))) -> b(b(a(b(b(x1)))))
    a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1)))))))
    a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1)))))))))
    a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1)))))))))
    a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1)))))))))
    a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1)))))))))
    a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1)))))))))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 0 0]  
     [b](x0) = [0 0 0]x0
               [0 0 0]  ,
     
               [1 0 1]     [0]
     [a](x0) = [0 0 0]x0 + [1]
               [0 1 0]     [0]
    orientation:
                   [1 0 1]     [0]    [1 0 0]                      
     a(b(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(a(b(b(x1)))))
                   [0 0 0]     [0]    [0 0 0]                      
     
                      [1 0 1]     [0]    [1 0 0]                            
     a(b(b(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(a(b(b(b(x1)))))))
                      [0 0 0]     [0]    [0 0 0]                            
     
                         [1 1 1]     [3]    [1 1 1]     [2]                                
     a(a(a(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(a(b(a(b(a(a(a(x1)))))))))
                         [0 0 0]     [1]    [0 0 0]     [1]                                
     
                         [1 1 1]     [1]    [1 1 1]                                  
     a(b(a(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(a(a(b(a(b(b(a(a(x1)))))))))
                         [0 0 0]     [0]    [0 0 0]                                  
     
                         [1 0 1]     [1]    [1 0 0]     [0]                                
     a(a(a(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(b(a(b(a(a(b(x1)))))))))
                         [0 0 0]     [1]    [0 0 0]     [1]                                
     
                         [1 0 1]     [0]    [1 0 0]                                  
     a(b(a(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(a(b(b(a(b(b(a(b(x1)))))))))
                         [0 0 0]     [0]    [0 0 0]                                  
     
                         [1 0 1]     [0]    [1 0 0]                                  
     a(b(b(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(b(a(b(b(b(b(x1)))))))))
                         [0 0 0]     [0]    [0 0 0]                                  
    problem:
     a(b(a(x1))) -> b(b(a(b(b(x1)))))
     a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1)))))))
     a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1)))))))))
     a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1)))))))))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b](x0) = x0,
      
      [a](x0) = 1x0
     orientation:
      a(b(a(x1))) = 2x1 >= 1x1 = b(b(a(b(b(x1)))))
      
      a(b(b(a(x1)))) = 2x1 >= 1x1 = b(b(b(a(b(b(b(x1)))))))
      
      a(b(a(b(a(x1))))) = 3x1 >= 3x1 = b(a(b(b(a(b(b(a(b(x1)))))))))
      
      a(b(b(b(a(x1))))) = 2x1 >= 1x1 = b(b(b(b(a(b(b(b(b(x1)))))))))
     problem:
      a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1)))))))))
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {3}
       transitions:
        b1(20) -> 21*
        b1(22) -> 23*
        b1(17) -> 18*
        b1(24) -> 25*
        b1(19) -> 20*
        b1(14) -> 15*
        b1(16) -> 17*
        a1(15) -> 16*
        a1(21) -> 22*
        a1(18) -> 19*
        a0(3) -> 3*
        b0(3) -> 3*
        3 -> 14*
        21 -> 24*
        23 -> 16,3
        25 -> 15*
      problem:
       
      Qed