NO

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

Proof:
 Unfolding Processor:
  loop length: 2
  terms:
   *(x45,+(f(z),f(x46)))
   *(g(x45,x46),+(f(z),f(z)))
  context: []
  substitution:
   z -> z
   x45 -> g(g(x45,x46),z)
   x46 -> z
  Qed