(FPCore (x y z t a) :precision binary64 (/ (- x (* y z)) (- t (* a z))))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (/ (- x (* z y)) (- t (* z a)))) (t_2 (/ (- y (/ x z)) a)))
(if (<= z -1.3216766444606895e+161)
t_2
(if (<= z -2.3460107355499526e+129)
t_1
(if (<= z -3.9924740520655655e+63)
(- (/ y a) (/ (/ x a) z))
(if (<= z 8.436988778214547e+90) t_1 t_2))))))
double code(double x, double y, double z, double t, double a) {
return (x - (y * z)) / (t - (a * z));
}
↓
double code(double x, double y, double z, double t, double a) {
double t_1 = (x - (z * y)) / (t - (z * a));
double t_2 = (y - (x / z)) / a;
double tmp;
if (z <= -1.3216766444606895e+161) {
tmp = t_2;
} else if (z <= -2.3460107355499526e+129) {
tmp = t_1;
} else if (z <= -3.9924740520655655e+63) {
tmp = (y / a) - ((x / a) / z);
} else if (z <= 8.436988778214547e+90) {
tmp = t_1;
} else {
tmp = t_2;
}
return tmp;
}
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
code = (x - (y * z)) / (t - (a * z))
end function
↓
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
real(8) :: t_1
real(8) :: t_2
real(8) :: tmp
t_1 = (x - (z * y)) / (t - (z * a))
t_2 = (y - (x / z)) / a
if (z <= (-1.3216766444606895d+161)) then
tmp = t_2
else if (z <= (-2.3460107355499526d+129)) then
tmp = t_1
else if (z <= (-3.9924740520655655d+63)) then
tmp = (y / a) - ((x / a) / z)
else if (z <= 8.436988778214547d+90) then
tmp = t_1
else
tmp = t_2
end if
code = tmp
end function
public static double code(double x, double y, double z, double t, double a) {
return (x - (y * z)) / (t - (a * z));
}
↓
public static double code(double x, double y, double z, double t, double a) {
double t_1 = (x - (z * y)) / (t - (z * a));
double t_2 = (y - (x / z)) / a;
double tmp;
if (z <= -1.3216766444606895e+161) {
tmp = t_2;
} else if (z <= -2.3460107355499526e+129) {
tmp = t_1;
} else if (z <= -3.9924740520655655e+63) {
tmp = (y / a) - ((x / a) / z);
} else if (z <= 8.436988778214547e+90) {
tmp = t_1;
} else {
tmp = t_2;
}
return tmp;
}
def code(x, y, z, t, a):
return (x - (y * z)) / (t - (a * z))
↓
def code(x, y, z, t, a):
t_1 = (x - (z * y)) / (t - (z * a))
t_2 = (y - (x / z)) / a
tmp = 0
if z <= -1.3216766444606895e+161:
tmp = t_2
elif z <= -2.3460107355499526e+129:
tmp = t_1
elif z <= -3.9924740520655655e+63:
tmp = (y / a) - ((x / a) / z)
elif z <= 8.436988778214547e+90:
tmp = t_1
else:
tmp = t_2
return tmp
function code(x, y, z, t, a)
return Float64(Float64(x - Float64(y * z)) / Float64(t - Float64(a * z)))
end
↓
function code(x, y, z, t, a)
t_1 = Float64(Float64(x - Float64(z * y)) / Float64(t - Float64(z * a)))
t_2 = Float64(Float64(y - Float64(x / z)) / a)
tmp = 0.0
if (z <= -1.3216766444606895e+161)
tmp = t_2;
elseif (z <= -2.3460107355499526e+129)
tmp = t_1;
elseif (z <= -3.9924740520655655e+63)
tmp = Float64(Float64(y / a) - Float64(Float64(x / a) / z));
elseif (z <= 8.436988778214547e+90)
tmp = t_1;
else
tmp = t_2;
end
return tmp
end
function tmp = code(x, y, z, t, a)
tmp = (x - (y * z)) / (t - (a * z));
end
↓
function tmp_2 = code(x, y, z, t, a)
t_1 = (x - (z * y)) / (t - (z * a));
t_2 = (y - (x / z)) / a;
tmp = 0.0;
if (z <= -1.3216766444606895e+161)
tmp = t_2;
elseif (z <= -2.3460107355499526e+129)
tmp = t_1;
elseif (z <= -3.9924740520655655e+63)
tmp = (y / a) - ((x / a) / z);
elseif (z <= 8.436988778214547e+90)
tmp = t_1;
else
tmp = t_2;
end
tmp_2 = tmp;
end
\[\leadsto \color{blue}{\frac{y}{a} - \frac{a \cdot x - t \cdot y}{a \cdot \left(a \cdot z\right)}}
\]
Proof
(-.f64 (/.f64 y a) (/.f64 (-.f64 (*.f64 a x) (*.f64 t y)) (*.f64 a (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (-.f64 (*.f64 a x) (Rewrite<= *-commutative_binary64 (*.f64 y t))) (*.f64 a (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 a x) (neg.f64 (*.f64 y t)))) (*.f64 a (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (+.f64 (*.f64 a x) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y t)))) (*.f64 a (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 y t)) (*.f64 a x))) (*.f64 a (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (+.f64 (*.f64 -1 (*.f64 y t)) (*.f64 a x)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a a) z)))): 15 points increase in error, 5 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (+.f64 (*.f64 -1 (*.f64 y t)) (*.f64 a x)) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y a) (neg.f64 (/.f64 (+.f64 (*.f64 -1 (*.f64 y t)) (*.f64 a x)) (*.f64 (pow.f64 a 2) z))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 y a) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (+.f64 (*.f64 -1 (*.f64 y t)) (*.f64 a x)) (*.f64 (pow.f64 a 2) z))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (/.f64 (/.f64 x a) z)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 y a) (Rewrite<= associate-/r*_binary64 (/.f64 x (*.f64 a z)))): 30 points increase in error, 28 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y a) (neg.f64 (/.f64 x (*.f64 a z))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 y a) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 x (*.f64 a z))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x (*.f64 a z))) (/.f64 y a))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 x (*.f64 a z)))) (/.f64 y a)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 x (*.f64 a z)))) (/.f64 y a)): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 y)) a)): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (/.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 2 2)) y) a)): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 2 2) (/.f64 y a)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 y a) (/.f64 2 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (*.f64 (/.f64 y a) (Rewrite=> metadata-eval 1))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (*.f64 (/.f64 y a) (Rewrite<= *-inverses_binary64 (/.f64 z z)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 0 (/.f64 x (*.f64 a z))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 y z) (*.f64 a z)))): 57 points increase in error, 8 points decrease in error
(Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 x (*.f64 a z)) (/.f64 (*.f64 y z) (*.f64 a z))))): 0 points increase in error, 0 points decrease in error
(-.f64 0 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x (*.f64 y z)) (*.f64 a z)))): 1 points increase in error, 2 points decrease in error
(Rewrite<= neg-sub0_binary64 (neg.f64 (/.f64 (-.f64 x (*.f64 y z)) (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 x (*.f64 y z)) (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
herbie shell --seed 2022308
(FPCore (x y z t a)
:name "Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A"
:precision binary64
:herbie-target
(if (< z -32113435955957344.0) (- (/ x (- t (* a z))) (/ y (- (/ t z) a))) (if (< z 3.5139522372978296e-86) (* (- x (* y z)) (/ 1.0 (- t (* a z)))) (- (/ x (- t (* a z))) (/ y (- (/ t z) a)))))
(/ (- x (* y z)) (- t (* a z))))