Initial program 0.0
\[\left(\left(d1 \cdot d2 - d1 \cdot d3\right) + d4 \cdot d1\right) - d1 \cdot d1
\]
Simplified0.0
\[\leadsto \color{blue}{d1 \cdot \left(d2 + \left(d4 - \left(d1 + d3\right)\right)\right)}
\]
Proof
(*.f64 d1 (+.f64 d2 (-.f64 d4 (+.f64 d1 d3)))): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (+.f64 d2 (-.f64 d4 (Rewrite<= +-commutative_binary64 (+.f64 d3 d1))))): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 d2 d4) (+.f64 d3 d1)))): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 d4 d2)) (+.f64 d3 d1))): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (Rewrite<= associate--l-_binary64 (-.f64 (-.f64 (+.f64 d4 d2) d3) d1))): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (-.f64 (Rewrite<= associate-+r-_binary64 (+.f64 d4 (-.f64 d2 d3))) d1)): 0 points increase in error, 0 points decrease in error
(*.f64 d1 (-.f64 (Rewrite=> +-commutative_binary64 (+.f64 (-.f64 d2 d3) d4)) d1)): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 d1 (+.f64 (-.f64 d2 d3) d4)) (*.f64 d1 d1))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 d1 (-.f64 d2 d3)) (*.f64 d1 d4))) (*.f64 d1 d1)): 5 points increase in error, 2 points decrease in error
(-.f64 (+.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 d1 d2) (*.f64 d1 d3))) (*.f64 d1 d4)) (*.f64 d1 d1)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (-.f64 (*.f64 d1 d2) (*.f64 d1 d3)) (Rewrite<= *-commutative_binary64 (*.f64 d4 d1))) (*.f64 d1 d1)): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \color{blue}{\mathsf{fma}\left(d4 - \left(d1 + d3\right), d1, d1 \cdot d2\right)}
\]
Final simplification0.0
\[\leadsto \mathsf{fma}\left(d4 - \left(d1 + d3\right), d1, d1 \cdot d2\right)
\]