(FPCore (x y z t a) :precision binary64 (+ x (/ (* y (- z t)) (- a t))))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (/ (* y (- z t)) (- a t))))
(if (<= t_1 (- INFINITY))
(+ x (/ (- z t) (- (/ a y) (/ t y))))
(if (<= t_1 2e+285) (+ t_1 x) (+ x (/ (- z t) (/ (- a t) y)))))))
double code(double x, double y, double z, double t, double a) {
return x + ((y * (z - t)) / (a - t));
}
↓
double code(double x, double y, double z, double t, double a) {
double t_1 = (y * (z - t)) / (a - t);
double tmp;
if (t_1 <= -((double) INFINITY)) {
tmp = x + ((z - t) / ((a / y) - (t / y)));
} else if (t_1 <= 2e+285) {
tmp = t_1 + x;
} else {
tmp = x + ((z - t) / ((a - t) / y));
}
return tmp;
}
public static double code(double x, double y, double z, double t, double a) {
return x + ((y * (z - t)) / (a - t));
}
↓
public static double code(double x, double y, double z, double t, double a) {
double t_1 = (y * (z - t)) / (a - t);
double tmp;
if (t_1 <= -Double.POSITIVE_INFINITY) {
tmp = x + ((z - t) / ((a / y) - (t / y)));
} else if (t_1 <= 2e+285) {
tmp = t_1 + x;
} else {
tmp = x + ((z - t) / ((a - t) / y));
}
return tmp;
}
def code(x, y, z, t, a):
return x + ((y * (z - t)) / (a - t))
↓
def code(x, y, z, t, a):
t_1 = (y * (z - t)) / (a - t)
tmp = 0
if t_1 <= -math.inf:
tmp = x + ((z - t) / ((a / y) - (t / y)))
elif t_1 <= 2e+285:
tmp = t_1 + x
else:
tmp = x + ((z - t) / ((a - t) / y))
return tmp
function code(x, y, z, t, a)
return Float64(x + Float64(Float64(y * Float64(z - t)) / Float64(a - t)))
end
\[\leadsto x + \color{blue}{\frac{z - t}{\frac{a - t}{y}}}
\]
Proof
(/.f64 (-.f64 z t) (/.f64 (-.f64 a t) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 z (/.f64 (-.f64 a t) y)) (/.f64 t (/.f64 (-.f64 a t) y)))): 2 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z y) (-.f64 a t))) (/.f64 t (/.f64 (-.f64 a t) y))): 45 points increase in error, 26 points decrease in error
(-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y z)) (-.f64 a t)) (/.f64 t (/.f64 (-.f64 a t) y))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t y) (-.f64 a t)))): 55 points increase in error, 37 points decrease in error
(-.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y t)) (-.f64 a t))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (neg.f64 (/.f64 (*.f64 y t) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y t) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto x + \frac{z - t}{\color{blue}{\frac{a}{y} - \frac{t}{y}}}
\]
if -inf.0 < (/.f64 (*.f64 y (-.f64 z t)) (-.f64 a t)) < 2e285
Initial program 0.3
\[x + \frac{y \cdot \left(z - t\right)}{a - t}
\]
if 2e285 < (/.f64 (*.f64 y (-.f64 z t)) (-.f64 a t))
\[\leadsto x + \color{blue}{\frac{z - t}{\frac{a - t}{y}}}
\]
Proof
(/.f64 (-.f64 z t) (/.f64 (-.f64 a t) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 z (/.f64 (-.f64 a t) y)) (/.f64 t (/.f64 (-.f64 a t) y)))): 2 points increase in error, 1 points decrease in error
(-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z y) (-.f64 a t))) (/.f64 t (/.f64 (-.f64 a t) y))): 45 points increase in error, 26 points decrease in error
(-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y z)) (-.f64 a t)) (/.f64 t (/.f64 (-.f64 a t) y))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t y) (-.f64 a t)))): 55 points increase in error, 37 points decrease in error
(-.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y t)) (-.f64 a t))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (neg.f64 (/.f64 (*.f64 y t) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y z) (-.f64 a t)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y t) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
herbie shell --seed 2022291
(FPCore (x y z t a)
:name "Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisTicks from plot-0.2.3.4, B"
:precision binary64
:herbie-target
(+ x (/ y (/ (- a t) (- z t))))
(+ x (/ (* y (- z t)) (- a t))))