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:
 DP Processor:
  DPs:
   +#(*(x,y),*(x,z)) -> +#(y,z)
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
   +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
  TRS:
   +(*(x,y),*(x,z)) -> *(x,+(y,z))
   +(+(x,y),z) -> +(x,+(y,z))
   +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
  EDG Processor:
   DPs:
    +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
   TRS:
    +(*(x,y),*(x,z)) -> *(x,+(y,z))
    +(+(x,y),z) -> +(x,+(y,z))
    +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
   graph:
    +#(+(x,y),z) -> +#(y,z) -> +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) ->
    +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) ->
    +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z) ->
    +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z) ->
    +#(+(x,y),z) -> +#(y,z)
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z) ->
    +#(+(x,y),z) -> +#(x,+(y,z))
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z) ->
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z) ->
    +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
    +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 20/25
    DPs:
     +#(+(x,y),z) -> +#(y,z)
     +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
     +#(+(x,y),z) -> +#(x,+(y,z))
     +#(*(x,y),*(x,z)) -> +#(y,z)
    TRS:
     +(*(x,y),*(x,z)) -> *(x,+(y,z))
     +(+(x,y),z) -> +(x,+(y,z))
     +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
    Subterm Criterion Processor:
     simple projection:
      pi(+#) = 0
     problem:
      DPs:
       
      TRS:
       +(*(x,y),*(x,z)) -> *(x,+(y,z))
       +(+(x,y),z) -> +(x,+(y,z))
       +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
     Qed