(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)))
(t_3 (/ y (+ x 1.0))))
(if (<= t_2 -1e+240)
(* (/ z t_1) t_3)
(if (<= t_2 4e+187)
t_2
(+ (/ (- t_3 (/ x (* z (+ x 1.0)))) t) (/ x (+ x 1.0)))))))
if (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < -1.00000000000000001e240
Initial program 49.4
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified49.4
\[\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
if -1.00000000000000001e240 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 3.99999999999999963e187
Initial program 0.8
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified0.8
\[\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
if 3.99999999999999963e187 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1))
Initial program 50.6
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified50.6
\[\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 2022318
(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)))