YES

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

Proof:
 Bounds Processor:
  bound: 0
  enrichment: roof
  automaton:
   final states: {7,6,2,1}
   transitions:
    f10() -> 6*,3,1,2
    *0(6,2) -> 7*
    *0(1,2) -> 7*,3,1
    *0(6,6) -> 7*
    *0(1,6) -> 7*
    *0(3,2) -> 7*,3,1
    *0(3,6) -> 7*
    *0(7,2) -> 7*
    *0(2,2) -> 7*,1,3
    *0(7,6) -> 7*
    *0(2,6) -> 7*
    1 -> 3*
    2 -> 7,3
    3 -> 1*
    6 -> 7*
  problem:
   
  Qed