YES

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

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {12,11,10,5,4,1}
   transitions:
    f30() -> 2*
    *0(2,12) -> 10*
    *0(2,3) -> 10*,3,4,1
    *0(2,11) -> 10*
    *0(2,10) -> 10*
    +0(2,12) -> 12*
    +0(1,6) -> 11*,4,3,5
    +0(2,3) -> 12*,3,4
    +0(2,11) -> 12*
    +0(10,6) -> 11*
    +0(2,2) -> 3*
    +0(2,10) -> 12*
    u0() -> 6*
    1 -> 4,3
    4 -> 3*
    5 -> 4*
  problem:
   
  Qed