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 CDG Processor: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) TRS: *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x graph: Qed