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)) LPO Processor: argument filtering: pi(if) = [0,1,2] pi(if#) = 0 precedence: if# ~ if problem: DPs: TRS: if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v)) Qed