TRS:
 {*(x, +(y, z)) -> +(*(x, y), *(x, z)),
  *(+(x, y), z) -> +(*(x, z), *(y, z)),
      *(x, 1()) -> x,
      *(1(), y) -> y}
 MPO:
  Prec:
   * > +
   empty
  Strict:
   {}
   Weak:
    {}
  Qed