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