NO

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

Proof:
 Unfolding Processor:
  loop length: 3
  terms:
   +(x236,*(x273,+(x274,x275)))
   +(x236,+(*(x273,x274),*(x273,x275)))
   +(+(x236,*(x273,x274)),*(x273,x275))
  context: []
  substitution:
   x236 -> x236
   x273 -> x273
   x274 -> x274
   x275 -> x275
  Qed