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 Matrix Interpretation Processor: dim=1 interpretation: [*#](x0, x1) = 4x0 + 5x1 + 2, [*](x0, x1) = x0 + x1 + 1 orientation: *#(x,*(y,z)) = 4x + 5y + 5z + 7 >= 4x + 5y + 2 = *#(x,y) *#(x,*(y,z)) = 4x + 5y + 5z + 7 >= 4x + 4y + 5z + 6 = *#(*(x,y),z) *(x,*(y,z)) = x + y + z + 2 >= x + y + z + 2 = *(*(x,y),z) *(x,x) = 2x + 1 >= x = x problem: DPs: TRS: *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x Qed