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:
 Bounds Processor:
  bound: 0
  enrichment: top
  automaton:
   final states: {12,11,10,2,1}
   transitions:
    u0() -> 10*,6,5,2,4
    v0() -> 11*,6,5,2,3
    f50() -> 1*
    if0(1,4,3) -> 12*,2,6,5
    if0(1,10,3) -> 12*
    if0(1,6,12) -> 12*
    if0(1,10,12) -> 12*
    if0(1,12,12) -> 12*
    if0(1,11,11) -> 12*
    if0(1,6,10) -> 12*
    if0(1,11,5) -> 12*
    if0(1,10,10) -> 12*
    if0(1,12,10) -> 12*
    if0(1,11,12) -> 12*
    if0(1,4,11) -> 12*
    if0(1,6,11) -> 12*
    if0(1,10,11) -> 12*
    if0(1,12,11) -> 12*
    if0(1,6,5) -> 12*,6,5,2
    if0(1,10,5) -> 12*
    if0(1,12,5) -> 12*
    if0(1,11,10) -> 12*
    2 -> 5,6
    3 -> 5,6
    4 -> 5,6
    5 -> 2*
    6 -> 2*
    10 -> 12*
    11 -> 12*
  problem:
   
  Qed