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