YES

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

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