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 Restore Modifier: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) TRS: *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 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: dimension: 1 interpretation: [*#](x0, x1) = x0 + x1, [*](x0, x1) = x0 + x1 + 1 orientation: *#(x,*(y,z)) = x + y + z + 1 >= x + y = *#(x,y) *#(x,*(y,z)) = x + y + z + 1 >= x + y + z + 1 = *#(*(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: *#(x,*(y,z)) -> *#(*(x,y),z) TRS: *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x Matrix Interpretation Processor: dimension: 1 interpretation: [*#](x0, x1) = x1, [*](x0, x1) = x1 + 1 orientation: *#(x,*(y,z)) = z + 1 >= z = *#(*(x,y),z) *(x,*(y,z)) = z + 2 >= z + 1 = *(*(x,y),z) *(x,x) = x + 1 >= x = x problem: DPs: TRS: *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x Qed