(FPCore (x y z t a)
:precision binary64
(/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))
↓
(FPCore (x y z t a)
:precision binary64
(if (<= z -2e+57)
(/ (* x y) (fma -0.5 (* (/ a (fabs z)) (/ t z)) (/ (fabs z) z)))
(if (<= z -9.5e-165)
(/ (* x y) (/ (sqrt (- (* z z) (* a t))) z))
(if (<= z 6e-70)
(* y (* z (/ x (hypot z (sqrt (* a (- t)))))))
(/ (* x y) (sqrt (- 1.0 (* (/ t z) (/ a z)))))))))
(fma.f64 -1/2 (*.f64 (/.f64 a (fabs.f64 z)) (/.f64 t z)) (/.f64 (fabs.f64 z) z)): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 z z)))) (/.f64 t z)) (/.f64 (fabs.f64 z) z)): 11 points increase in error, 1 points decrease in error
(fma.f64 -1/2 (*.f64 (/.f64 a (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)))) (/.f64 t z)) (/.f64 (fabs.f64 z) z)): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 a t) (*.f64 (sqrt.f64 (pow.f64 z 2)) z))) (/.f64 (fabs.f64 z) z)): 14 points increase in error, 7 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a t) (*.f64 (sqrt.f64 (pow.f64 z 2)) z)) (/.f64 (Rewrite<= rem-sqrt-square_binary64 (sqrt.f64 (*.f64 z z))) z)): 80 points increase in error, 0 points decrease in error
(fma.f64 -1/2 (/.f64 (*.f64 a t) (*.f64 (sqrt.f64 (pow.f64 z 2)) z)) (/.f64 (sqrt.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2))) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 a t) (*.f64 (sqrt.f64 (pow.f64 z 2)) z))) (/.f64 (sqrt.f64 (pow.f64 z 2)) z))): 0 points increase in error, 0 points decrease in error
if -2.0000000000000001e57 < z < -9.49999999999999973e-165
Initial program 7.9
\[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\]
Simplified6.0
\[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}
\]
Proof
(/.f64 (*.f64 x y) (/.f64 (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 x y) z) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))))): 42 points increase in error, 13 points decrease in error
if -9.49999999999999973e-165 < z < 6.0000000000000003e-70
Initial program 16.9
\[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\]
Simplified16.1
\[\leadsto \color{blue}{\frac{x}{\frac{\sqrt{z \cdot z - t \cdot a}}{y \cdot z}}}
\]
Proof
(/.f64 x (/.f64 (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))) (*.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x (*.f64 y z)) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))))): 37 points increase in error, 22 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x y) z)) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a)))): 6 points increase in error, 54 points decrease in error
(sqrt.f64 (-.f64 1 (*.f64 (/.f64 t z) (/.f64 a z)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (-.f64 (Rewrite<= *-inverses_binary64 (/.f64 (*.f64 z z) (*.f64 z z))) (*.f64 (/.f64 t z) (/.f64 a z)))): 94 points increase in error, 0 points decrease in error
(sqrt.f64 (-.f64 (/.f64 (*.f64 z z) (*.f64 z z)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 t a) (*.f64 z z))))): 8 points increase in error, 5 points decrease in error
(sqrt.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 z z) (*.f64 t a)) (*.f64 z z)))): 0 points increase in error, 1 points decrease in error
herbie shell --seed 2022325
(FPCore (x y z t a)
:name "Statistics.Math.RootFinding:ridders from math-functions-0.1.5.2"
:precision binary64
:herbie-target
(if (< z -3.1921305903852764e+46) (- (* y x)) (if (< z 5.976268120920894e+90) (/ (* x z) (/ (sqrt (- (* z z) (* a t))) y)) (* y x)))
(/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))