YES

Problem:
 +(x,+(y,z)) -> +(+(x,y),z)
 +(*(x,y),+(x,z)) -> *(x,+(y,z))
 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u)

Proof:
 Bounds Processor:
  bound: 0
  enrichment: roof
  automaton:
   final states: {11,10,9,5,4,1}
   transitions:
    f20() -> 2*
    +0(9,2) -> 9*
    +0(4,2) -> 5*
    +0(11,2) -> 11*,5
    +0(1,2) -> 9*,3,1
    +0(3,2) -> 9*,3,1
    +0(10,2) -> 11*,5
    +0(5,2) -> 5*
    +0(2,2) -> 3*
    *0(2,3) -> 10*,5,3,1,4
    *0(2,9) -> 10*
    *0(2,11) -> 10*
    *0(2,10) -> 10*
    1 -> 3*
    4 -> 1,3,5
  problem:
   
  Qed