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