Simplified3.4
\[\leadsto \color{blue}{\frac{1}{y \cdot \mathsf{fma}\left(z, z \cdot x, x\right)}}
\]
Proof
(/.f64 1 (*.f64 y (fma.f64 z (*.f64 z x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 1 (*.f64 y (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 z (*.f64 z x)) x)))): 0 points increase in error, 0 points decrease in error
(/.f64 1 (*.f64 y (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z z) x)) x))): 11 points increase in error, 9 points decrease in error
(/.f64 1 (*.f64 y (+.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 1 (*.f64 y (Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (pow.f64 z 2) 1) x)))): 0 points increase in error, 0 points decrease in error
Simplified0.5
\[\leadsto \color{blue}{\frac{\frac{1}{\mathsf{fma}\left(z, z \cdot y, y\right)}}{x}}
\]
Proof
(/.f64 (/.f64 1 (fma.f64 z (*.f64 z y) y)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (fma.f64 z (Rewrite<= *-commutative_binary64 (*.f64 y z)) y)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (*.f64 y z)) y))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 y z) z)) y)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 z z))) y)) x): 10 points increase in error, 1 points decrease in error
(/.f64 (/.f64 1 (+.f64 (*.f64 y (Rewrite<= unpow2_binary64 (pow.f64 z 2))) y)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (+.f64 (*.f64 y (pow.f64 z 2)) (Rewrite<= *-rgt-identity_binary64 (*.f64 y 1)))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 1 (Rewrite<= distribute-lft-in_binary64 (*.f64 y (+.f64 (pow.f64 z 2) 1)))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 y) (+.f64 (pow.f64 z 2) 1))) x): 5 points increase in error, 6 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 1 y) (*.f64 (+.f64 (pow.f64 z 2) 1) x))): 14 points increase in error, 10 points decrease in error
(/.f64 (/.f64 1 y) (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 (pow.f64 z 2) x) x))): 0 points increase in error, 1 points decrease in error
(Rewrite=> associate-/l/_binary64 (/.f64 1 (*.f64 (+.f64 (*.f64 (pow.f64 z 2) x) x) y))): 34 points increase in error, 23 points decrease in error