YES Problem: 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(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v)) KBO Processor: argument filtering: pi(if) = [0,1,2] pi(if#) = 0 usable rules: weight function: w0 = 1 w(if#) = w(if) = 1 precedence: if# ~ if problem: DPs: TRS: if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v)) Qed