Simplified64.0
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(y + t, a, \mathsf{fma}\left(x, z, y \cdot \left(z - b\right)\right)\right)}{x + \left(y + t\right)}}
\]
Proof
(/.f64 (fma.f64 (+.f64 y t) a (fma.f64 x z (*.f64 y (-.f64 z b)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 t y)) a (fma.f64 x z (*.f64 y (-.f64 z b)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (fma.f64 x z (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y z) (*.f64 y b))))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (fma.f64 x z (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 y z) (neg.f64 (*.f64 y b)))))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x z) (+.f64 (*.f64 y z) (neg.f64 (*.f64 y b)))))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 x z) (*.f64 y z)) (neg.f64 (*.f64 y b))))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 z (+.f64 x y))) (neg.f64 (*.f64 y b)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x y) z)) (neg.f64 (*.f64 y b)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 t y) a) (+.f64 (*.f64 (+.f64 x y) z) (neg.f64 (*.f64 y b))))) (+.f64 x (+.f64 y t))): 1 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (+.f64 t y) a) (*.f64 (+.f64 x y) z)) (neg.f64 (*.f64 y b)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a))) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b)) (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x t) y))): 0 points increase in error, 0 points decrease in error
Simplified18.8
\[\leadsto \color{blue}{\frac{z - b}{\frac{x + \left(t + y\right)}{y}} + \left(\frac{z \cdot x}{x + \left(t + y\right)} + \frac{a}{x + \left(t + y\right)} \cdot \left(t + y\right)\right)}
\]
Proof
(+.f64 (/.f64 (-.f64 z b) (/.f64 (+.f64 x (+.f64 t y)) y)) (+.f64 (/.f64 (*.f64 z x) (+.f64 x (+.f64 t y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x t) y)) y)) (+.f64 (/.f64 (*.f64 z x) (+.f64 x (+.f64 t y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 t x)) y) y)) (+.f64 (/.f64 (*.f64 z x) (+.f64 x (+.f64 t y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 t x))) y)) (+.f64 (/.f64 (*.f64 z x) (+.f64 x (+.f64 t y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x)))) (+.f64 (/.f64 (*.f64 z x) (+.f64 x (+.f64 t y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 46 points increase in error, 10 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x t) y))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 t x)) y)) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 t x)))) (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (*.f64 (/.f64 a (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y t)))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (*.f64 (/.f64 a (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 y t) x))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (*.f64 (/.f64 a (+.f64 (Rewrite=> +-commutative_binary64 (+.f64 t y)) x)) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (*.f64 (/.f64 a (Rewrite<= associate-+r+_binary64 (+.f64 t (+.f64 y x)))) (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (*.f64 (/.f64 a (+.f64 t (+.f64 y x))) (Rewrite<= +-commutative_binary64 (+.f64 y t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (Rewrite<= associate-/r/_binary64 (/.f64 a (/.f64 (+.f64 t (+.f64 y x)) (+.f64 y t)))))): 5 points increase in error, 26 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (/.f64 a (/.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 t y) x)) (+.f64 y t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (/.f64 a (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 y t)) x) (+.f64 y t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (/.f64 a (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 y (+.f64 t x))) (+.f64 y t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))))): 44 points increase in error, 4 points decrease in error