(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 -5000000000000.0)
(* (/ y (+ x 1.0)) (/ z t_1))
(if (<= t_2 1e-191)
(/ (+ x (/ (- y (/ x z)) t)) (+ x 1.0))
(if (<= t_2 5e+278)
t_2
(-
(+ (/ y (* t (+ x 1.0))) (/ x (+ x 1.0)))
(/ x (* (* z t) (+ x 1.0)))))))))
if (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < -5e12
Initial program 18.7
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified18.7
\[\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
(*.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)))): 46 points increase in error, 24 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
if -5e12 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 1e-191
Initial program 3.9
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified3.9
\[\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 1e-191 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 5.00000000000000029e278
Initial program 0.1
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified0.1
\[\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 5.00000000000000029e278 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1))
Initial program 60.6
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified60.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 2022294
(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)))