YES

Problem:
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 if(x,y,y) -> y
 if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))

Proof:
 DP Processor:
  DPs:
   if#(if(x,y,z),u(),v()) -> if#(z,u(),v())
   if#(if(x,y,z),u(),v()) -> if#(y,u(),v())
   if#(if(x,y,z),u(),v()) -> if#(x,if(y,u(),v()),if(z,u(),v()))
  TRS:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   if(x,y,y) -> y
   if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    
   interpretation:
    [if#](x0, x1, x2) = x0 + 0,
    
    [v] = 1,
    
    [u] = 0,
    
    [false] = 1,
    
    [if](x0, x1, x2) = 1x0 + 1x1 + 1x2 + 1,
    
    [true] = 6
   orientation:
    if#(if(x,y,z),u(),v()) = 1x + 1y + 1z + 1 >= z + 0 = if#(z,u(),v())
    
    if#(if(x,y,z),u(),v()) = 1x + 1y + 1z + 1 >= y + 0 = if#(y,u(),v())
    
    if#(if(x,y,z),u(),v()) = 1x + 1y + 1z + 1 >= x + 0 = if#(x,if(y,u(),v()),if(z,u(),v()))
    
    if(true(),x,y) = 1x + 1y + 7 >= x = x
    
    if(false(),x,y) = 1x + 1y + 2 >= y = y
    
    if(x,y,y) = 1x + 1y + 1 >= y = y
    
    if(if(x,y,z),u(),v()) = 2x + 2y + 2z + 2 >= 1x + 2y + 2z + 3 = if(x,if(y,u(),v()),if(z,u(),v()))
   problem:
    DPs:
     
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     if(x,y,y) -> y
     if(if(x,y,z),u(),v()) -> if(x,if(y,u(),v()),if(z,u(),v()))
   Qed