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)
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    
   interpretation:
    [0#](x0) = 0,
    
    [1#](x0) = x0,
    
    [1](x0) = 4,
    
    [0](x0) = 1x0 + 7
   orientation:
    1#(0(x1)) = 1x1 + 7 >= x1 = 1#(x1)
    
    1#(0(x1)) = 1x1 + 7 >= 0 = 0#(1(x1))
    
    1#(0(x1)) = 1x1 + 7 >= 0 = 0#(0(1(x1)))
    
    1#(0(x1)) = 1x1 + 7 >= 0 = 0#(0(0(1(x1))))
    
    1#(1(x1)) = 4 >= 0 = 0#(x1)
    
    1#(1(x1)) = 4 >= 0 = 0#(0(x1))
    
    1#(1(x1)) = 4 >= 0 = 0#(0(0(x1)))
    
    1#(1(x1)) = 4 >= 0 = 0#(0(0(0(x1))))
    
    1(0(x1)) = 4 >= 9 = 0(0(0(1(x1))))
    
    0(1(x1)) = 7 >= 4 = 1(x1)
    
    1(1(x1)) = 4 >= 4x1 + 10 = 0(0(0(0(x1))))
    
    0(0(x1)) = 2x1 + 8 >= 1x1 + 7 = 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