(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+14)
(/ (+ x (/ y (/ t_1 z))) (+ x 1.0))
(if (<= t_2 2e-48)
(/ (+ x (/ (- y (/ x z)) t)) (+ x 1.0))
(if (<= t_2 2e+26)
t_2
(if (<= t_2 INFINITY)
(* y (/ (/ z (+ x 1.0)) t_1))
(-
(+ (/ x (+ x 1.0)) (/ y (* t (+ 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)) < -1e14
Initial program 16.6
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified16.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
(/.f64 (+.f64 x (/.f64 y (/.f64 (-.f64 (*.f64 t z) x) z))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y z) (-.f64 (*.f64 t z) x)))) (+.f64 x 1)): 0 points increase in error, 2 points decrease in error
if -1e14 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 1.9999999999999999e-48
Initial program 3.2
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified3.2
\[\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.9999999999999999e-48 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 2.0000000000000001e26
Initial program 0.0
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
if 2.0000000000000001e26 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < +inf.0
Initial program 19.6
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified19.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
(/.f64 (+.f64 x (/.f64 y (/.f64 (-.f64 (*.f64 t z) x) z))) (+.f64 x 1)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y z) (-.f64 (*.f64 t z) x)))) (+.f64 x 1)): 0 points increase in error, 2 points decrease in error
if +inf.0 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1))
Initial program 64.0
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\]
Simplified64.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 2022340
(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)))