YES Problem: *(x,+(y,z)) -> +(*(x,y),*(x,z)) Proof: DP Processor: DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) KBO Processor: argument filtering: pi(+) = [0,1] pi(*) = 1 pi(*#) = 1 weight function: w0 = 1 w(*#) = 1 w(*) = w(+) = 0 precedence: *# ~ * ~ + problem: DPs: TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) Qed