YES

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

Proof:
 Bounds Processor:
  bound: 0
  enrichment: roof
  automaton:
   final states: {8,5,1}
   transitions:
    f30() -> 2*
    *0(4,2) -> 1*
    *0(2,5) -> 8*,6,5
    *0(2,2) -> 6*
    *0(2,6) -> 8*,6,5
    *0(2,8) -> 8*
    +0(2,3) -> 4*
    a0() -> 3*
    5 -> 6*
  problem:
   
  Qed