Simplified63.8
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(y + t, a, \mathsf{fma}\left(x, z, y \cdot \left(z - b\right)\right)\right)}{y + \left(x + t\right)}}
\]
Proof
(/.f64 (fma.f64 (+.f64 y t) a (fma.f64 x z (*.f64 y (-.f64 z b)))) (+.f64 y (+.f64 x 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 y (+.f64 x 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 y (+.f64 x t))): 0 points increase in error, 13 points decrease in error
(/.f64 (fma.f64 (+.f64 t y) a (fma.f64 x z (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 y z) (neg.f64 (*.f64 y b)))))) (+.f64 y (+.f64 x 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 y (+.f64 x t))): 13 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 y (+.f64 x t))): 13 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 y (+.f64 x 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 y (+.f64 x t))): 0 points increase in error, 13 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 y (+.f64 x t))): 0 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 y (+.f64 x 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 y (+.f64 x 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 y (+.f64 x t))): 13 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<= +-commutative_binary64 (+.f64 (+.f64 x t) y))): 0 points increase in error, 13 points decrease in error
Simplified0.2
\[\leadsto \color{blue}{\left(\frac{a}{x + \left(t + y\right)} \cdot \left(t + y\right) + \frac{z}{\frac{x + \left(t + y\right)}{x + y}}\right) - \frac{y}{\frac{x + \left(t + y\right)}{b}}}
\]
Proof
(-.f64 (+.f64 (*.f64 (/.f64 a (+.f64 x (+.f64 t y))) (+.f64 t y)) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (/.f64 a (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y t)))) (+.f64 t y)) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (/.f64 a (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 y t) x))) (+.f64 t y)) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 6 points increase in error, 15 points decrease in error
(-.f64 (+.f64 (*.f64 (/.f64 a (Rewrite<= associate-+r+_binary64 (+.f64 y (+.f64 t x)))) (+.f64 t y)) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 17 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 (/.f64 a (+.f64 y (+.f64 t x))) (Rewrite<= +-commutative_binary64 (+.f64 y t))) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 4 points increase in error, 17 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 a (/.f64 (+.f64 y (+.f64 t x)) (+.f64 y t)))) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 4 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (/.f64 z (/.f64 (+.f64 x (+.f64 t y)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 11 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 z (/.f64 (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y t))) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 15 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 z (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 y t) x)) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 11 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 z (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 y (+.f64 t x))) (+.f64 x y)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 11 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 z (/.f64 (+.f64 y (+.f64 t x)) (Rewrite<= +-commutative_binary64 (+.f64 y x))))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 5 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z (+.f64 y x)) (+.f64 y (+.f64 t x))))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 10 points increase in error, 5 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 y x) z)) (+.f64 y (+.f64 t x)))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 10 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))))) (/.f64 y (/.f64 (+.f64 x (+.f64 t y)) b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (/.f64 y (/.f64 (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y t))) b))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (/.f64 y (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 y t) x)) b))): 21 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (/.f64 y (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 y (+.f64 t x))) b))): 11 points increase in error, 6 points decrease in error
(-.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y b) (+.f64 y (+.f64 t x))))): 0 points increase in error, 15 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (neg.f64 (/.f64 (*.f64 y b) (+.f64 y (+.f64 t x)))))): 15 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y b) (+.f64 y (+.f64 t x)))))): 0 points increase in error, 11 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (*.f64 -1 (/.f64 (*.f64 y b) (+.f64 y (+.f64 t x))))))): 17 points increase in error, 4 points decrease in error