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)))))))))))))))))))

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)))))))))))))))
  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)))))))))))))))))))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [0#](x0) = [0 0 1]x0,
    
              [0 1 0]     [0]
    [0](x0) = [0 0 1]x0 + [1]
              [0 0 1]     [1],
    
              [0 0 0]     [0]
    [2](x0) = [1 0 0]x0 + [1]
              [1 0 0]     [0],
    
              [1 0 0]     [1]
    [1](x0) = [0 0 1]x0 + [0]
              [0 1 0]     [0]
   orientation:
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(x1)))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(x1))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(x1)))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                   
    0(1(2(1(x1)))) = [1 0 0]x1 + [3] >= [1 0 0]x1 + [2] = 1(2(1(1(0(1(2(0(1(2(x1))))))))))
                     [1 0 0]     [3]    [1 0 0]     [3]                                   
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                            
    0(1(2(1(x1)))) = [1 0 0]x1 + [3] >= [1 0 0]x1 + [2] = 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [3]                                            
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                     
    0(1(2(1(x1)))) = [1 0 0]x1 + [3] >= [1 0 0]x1 + [2] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [3]                                                     
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                              
    0(1(2(1(x1)))) = [1 0 0]x1 + [3] >= [1 0 0]x1 + [2] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [3]                                                              
   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)))))))))))))))))))
   Qed