Error

Derivation

1. Initial program 0.3

   \[\frac{\left(\frac{\left(d1 \cdot \left(real->posit(10)\right)\right)}{\left(d1 \cdot d2\right)}\right)}{\left(d1 \cdot \left(real->posit(20)\right)\right)}\]
2. Using strategy rm

3. Applied *-commutative0.3

   \[\leadsto \frac{\left(\frac{\left(d1 \cdot \left(real->posit(10)\right)\right)}{\color{blue}{\left(d2 \cdot d1\right)}}\right)}{\left(d1 \cdot \left(real->posit(20)\right)\right)}\]

4. Applied *-commutative0.3

   \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(real->posit(10)\right) \cdot d1\right)}}{\left(d2 \cdot d1\right)}\right)}{\left(d1 \cdot \left(real->posit(20)\right)\right)}\]

5. Applied distribute-rgt-out0.3

   \[\leadsto \frac{\color{blue}{\left(d1 \cdot \left(\frac{\left(real->posit(10)\right)}{d2}\right)\right)}}{\left(d1 \cdot \left(real->posit(20)\right)\right)}\]

6. Final simplification0.3

   \[\leadsto d1 \cdot \left(10 + d2\right) + d1 \cdot 20\]

Reproduce

herbie shell --seed 2019072 +o rules:numerics
(FPCore (d1 d2)
  :name "FastMath test2"
  (+.p16 (+.p16 (*.p16 d1 (real->posit16 10)) (*.p16 d1 d2)) (*.p16 d1 (real->posit16 20))))