YES

Problem:
 r0(0(x1)) -> 0(r0(x1))
 r0(1(x1)) -> 1(r0(x1))
 r0(m(x1)) -> m(r0(x1))
 r1(0(x1)) -> 0(r1(x1))
 r1(1(x1)) -> 1(r1(x1))
 r1(m(x1)) -> m(r1(x1))
 r0(b(x1)) -> qr(0(b(x1)))
 r1(b(x1)) -> qr(1(b(x1)))
 0(qr(x1)) -> qr(0(x1))
 1(qr(x1)) -> qr(1(x1))
 m(qr(x1)) -> ql(m(x1))
 0(ql(x1)) -> ql(0(x1))
 1(ql(x1)) -> ql(1(x1))
 b(ql(0(x1))) -> 0(b(r0(x1)))
 b(ql(1(x1))) -> 1(b(r1(x1)))

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