(FPCore (x y z t)
:precision binary64
(/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)))
↓
(FPCore (x y z t)
:precision binary64
(let* ((t_1 (- (* z t) x)) (t_2 (/ (+ x (/ (- (* y z) x) t_1)) (+ x 1.0))))
(if (<= t_2 -1e+68)
(/ (/ y (/ t_1 z)) (+ x 1.0))
(if (<= t_2 5e+286)
(/ (+ x (/ (fma y z (- x)) (fma z t (- x)))) (+ x 1.0))
(/ (+ x (/ y t)) (+ x 1.0))))))
(/.f64 (+.f64 x (/.f64 (fma.f64 y z (neg.f64 x)) (fma.f64 z t (neg.f64 x)))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 y z) x)) (fma.f64 z t (neg.f64 x)))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z t) x)))) (+.f64 x 1)): 1 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 t z)) x))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 y (+.f64 x 1)) (/.f64 z (-.f64 (*.f64 t z) x))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 y (Rewrite=> +-commutative_binary64 (+.f64 1 x))) (/.f64 z (-.f64 (*.f64 t z) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 y z) (*.f64 (+.f64 1 x) (-.f64 (*.f64 t z) x)))): 53 points increase in error, 32 points decrease in error
(/.f64 (*.f64 y z) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (*.f64 t z) x) (+.f64 1 x)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr7.9
\[\leadsto \color{blue}{\frac{\frac{y}{\frac{z \cdot t - x}{z}}}{x + 1}}
\]
if -9.99999999999999953e67 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 5.0000000000000004e286
Initial program 0.7
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
(/.f64 (+.f64 x (/.f64 (fma.f64 y z (neg.f64 x)) (fma.f64 z t (neg.f64 x)))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 y z) x)) (fma.f64 z t (neg.f64 x)))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z t) x)))) (+.f64 x 1)): 1 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 t z)) x))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
if 5.0000000000000004e286 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1))
Initial program 61.0
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified61.0
\[\leadsto \color{blue}{\frac{x + \frac{y \cdot z - x}{z \cdot t - x}}{x + 1}}
\]
Proof
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 z t) x))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 t z)) x))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
herbie shell --seed 2022325
(FPCore (x y z t)
:name "Diagrams.Trail:splitAtParam from diagrams-lib-1.3.0.3, A"
:precision binary64
:herbie-target
(/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1.0))
(/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)))