YES

Problem:
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))

Proof:
 DP Processor:
  DPs:
   0#(1(2(1(x1)))) -> 0#(1(2(x1)))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(x1))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(x1)))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
  TRS:
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [0#](x0) = [0 1 0]x0,
    
              [0 0 0]     [0]
    [0](x0) = [0 1 1]x0 + [1]
              [0 0 1]     [0],
    
              [0 0 0]  
    [2](x0) = [0 0 1]x0
              [0 0 0]  ,
    
              [0 0 0]     [0]
    [1](x0) = [0 1 0]x0 + [0]
              [0 0 1]     [1]
   orientation:
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [0 0 1]x1 = 0#(1(2(x1)))
    
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [1] = 0#(1(2(0(1(2(x1))))))
    
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [1] = 0#(1(2(0(1(2(0(1(2(x1)))))))))
    
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
    
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
    
    0#(1(2(1(x1)))) = [0 0 1]x1 + [1] >= [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
    
                     [0 0 0]     [0]    [0]                                   
    0(1(2(1(x1)))) = [0 0 1]x1 + [3] >= [3] = 1(2(1(1(0(1(2(0(1(2(x1))))))))))
                     [0 0 0]     [1]    [1]                                   
    
                     [0 0 0]     [0]    [0]                                            
    0(1(2(1(x1)))) = [0 0 1]x1 + [3] >= [3] = 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
                     [0 0 0]     [1]    [1]                                            
    
                     [0 0 0]     [0]    [0]                                                     
    0(1(2(1(x1)))) = [0 0 1]x1 + [3] >= [3] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
                     [0 0 0]     [1]    [1]                                                     
    
                     [0 0 0]     [0]    [0]                                                              
    0(1(2(1(x1)))) = [0 0 1]x1 + [3] >= [3] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
                     [0 0 0]     [1]    [1]                                                              
    
                     [0 0 0]     [0]    [0]                                                                       
    0(1(2(1(x1)))) = [0 0 1]x1 + [3] >= [3] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
                     [0 0 0]     [1]    [1]                                                                       
   problem:
    DPs:
     0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(x1))))))
     0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(x1)))))))))
     0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
     0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
     0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
    TRS:
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
   Matrix Interpretation Processor: dim=4
    
    interpretation:
     [0#](x0) = [0 1 0 1]x0,
     
               [0 1 0 0]     [0]
               [1 0 0 0]     [0]
     [0](x0) = [0 0 0 0]x0 + [0]
               [0 0 0 0]     [1],
     
               [0 0 0 0]  
               [0 0 0 0]  
     [2](x0) = [0 0 1 0]x0
               [1 0 0 0]  ,
     
               [0 0 0 0]     [1]
               [0 0 0 1]     [0]
     [1](x0) = [1 0 0 0]x0 + [0]
               [0 1 1 0]     [0]
    orientation:
     0#(1(2(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(1(2(0(1(2(x1))))))
     
     0#(1(2(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(1(2(0(1(2(0(1(2(x1)))))))))
     
     0#(1(2(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
     
     0#(1(2(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
     
     0#(1(2(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
     
                      [1]    [1]                                   
                      [1]    [1]                                   
     0(1(2(1(x1)))) = [0] >= [0] = 1(2(1(1(0(1(2(0(1(2(x1))))))))))
                      [1]    [1]                                   
     
                      [1]    [1]                                            
                      [1]    [1]                                            
     0(1(2(1(x1)))) = [0] >= [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
                      [1]    [1]                                            
     
                      [1]    [1]                                                     
                      [1]    [1]                                                     
     0(1(2(1(x1)))) = [0] >= [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
                      [1]    [1]                                                     
     
                      [1]    [1]                                                              
                      [1]    [1]                                                              
     0(1(2(1(x1)))) = [0] >= [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
                      [1]    [1]                                                              
     
                      [1]    [1]                                                                       
                      [1]    [1]                                                                       
     0(1(2(1(x1)))) = [0] >= [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
                      [1]    [1]                                                                       
    problem:
     DPs:
      
     TRS:
      0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
      0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
      0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
      0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
      0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
    Qed