\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
↓
\[\begin{array}{l}
t_1 := y \cdot \left(x \cdot z\right)\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := t_3 + \left(t_2 + b \cdot \left(t \cdot i - z \cdot c\right)\right)\\
\mathbf{if}\;t_4 \leq -5 \cdot 10^{+303}:\\
\;\;\;\;\left(t_1 - z \cdot \left(b \cdot c\right)\right) + \left(j \cdot \mathsf{fma}\left(-i, y, y \cdot i\right) + t_3\right)\\
\mathbf{elif}\;t_4 \leq 10^{+307}:\\
\;\;\;\;t_3 + \left(t_2 - \left(b \cdot \mathsf{fma}\left(-i, t, t \cdot i\right) + b \cdot \left(z \cdot c - t \cdot i\right)\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(t_1 - y \cdot \left(i \cdot j\right)\right) + i \cdot \left(t \cdot b\right)\\
\end{array}
\]
(FPCore (x y z t a b c i j)
:precision binary64
(+
(- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i))))
(* j (- (* c a) (* y i)))))
↓
(FPCore (x y z t a b c i j)
:precision binary64
(let* ((t_1 (* y (* x z)))
(t_2 (* x (- (* y z) (* t a))))
(t_3 (* j (- (* a c) (* y i))))
(t_4 (+ t_3 (+ t_2 (* b (- (* t i) (* z c)))))))
(if (<= t_4 -5e+303)
(+ (- t_1 (* z (* b c))) (+ (* j (fma (- i) y (* y i))) t_3))
(if (<= t_4 1e+307)
(+
t_3
(- t_2 (+ (* b (fma (- i) t (* t i))) (* b (- (* z c) (* t i))))))
(+ (- t_1 (* y (* i j))) (* i (* t b)))))))
\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
↓
\begin{array}{l}
t_1 := y \cdot \left(x \cdot z\right)\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := t_3 + \left(t_2 + b \cdot \left(t \cdot i - z \cdot c\right)\right)\\
\mathbf{if}\;t_4 \leq -5 \cdot 10^{+303}:\\
\;\;\;\;\left(t_1 - z \cdot \left(b \cdot c\right)\right) + \left(j \cdot \mathsf{fma}\left(-i, y, y \cdot i\right) + t_3\right)\\
\mathbf{elif}\;t_4 \leq 10^{+307}:\\
\;\;\;\;t_3 + \left(t_2 - \left(b \cdot \mathsf{fma}\left(-i, t, t \cdot i\right) + b \cdot \left(z \cdot c - t \cdot i\right)\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(t_1 - y \cdot \left(i \cdot j\right)\right) + i \cdot \left(t \cdot b\right)\\
\end{array}
Error
Target
Original
12.5
Target
20.3
Herbie
7.9
\[\begin{array}{l}
\mathbf{if}\;x < -1.469694296777705 \cdot 10^{-64}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \frac{b \cdot \left({\left(c \cdot z\right)}^{2} - {\left(t \cdot i\right)}^{2}\right)}{c \cdot z + t \cdot i}\right) + j \cdot \left(c \cdot a - y \cdot i\right)\\
\mathbf{elif}\;x < 3.2113527362226803 \cdot 10^{-147}:\\
\;\;\;\;\left(b \cdot i - x \cdot a\right) \cdot t - \left(z \cdot \left(c \cdot b\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \frac{b \cdot \left({\left(c \cdot z\right)}^{2} - {\left(t \cdot i\right)}^{2}\right)}{c \cdot z + t \cdot i}\right) + j \cdot \left(c \cdot a - y \cdot i\right)\\
\end{array}
\]
Derivation
Split input into 3 regimes
if (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) < -4.9999999999999997e303
Initial program 59.8
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
Simplified59.8
\[\leadsto \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)}
\]
Proof
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 z c) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c a)) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 j (*.f64 c a)) (*.f64 j (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= cancel-sign-sub_binary64 (-.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub_binary64 (+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 y i)) j))): 0 points increase in error, 13 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 (*.f64 y i)) j)))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= distribute-rgt-in_binary64 (*.f64 j (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 c a) (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
Applied egg-rr59.8
\[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \color{blue}{\left(\mathsf{fma}\left(-i, y, y \cdot i\right) \cdot j + j \cdot \left(a \cdot c - y \cdot i\right)\right)}
\]
Taylor expanded in y around inf 48.8
\[\leadsto \left(\color{blue}{y \cdot \left(z \cdot x\right)} - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \left(\mathsf{fma}\left(-i, y, y \cdot i\right) \cdot j + j \cdot \left(a \cdot c - y \cdot i\right)\right)
\]
Taylor expanded in z around inf 42.8
\[\leadsto \left(y \cdot \left(z \cdot x\right) - \color{blue}{c \cdot \left(z \cdot b\right)}\right) + \left(\mathsf{fma}\left(-i, y, y \cdot i\right) \cdot j + j \cdot \left(a \cdot c - y \cdot i\right)\right)
\]
Simplified41.5
\[\leadsto \left(y \cdot \left(z \cdot x\right) - \color{blue}{z \cdot \left(c \cdot b\right)}\right) + \left(\mathsf{fma}\left(-i, y, y \cdot i\right) \cdot j + j \cdot \left(a \cdot c - y \cdot i\right)\right)
\]
Proof
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (*.f64 z (*.f64 c b))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z c) b))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 4 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) b)) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 0 points increase in error, 4 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 z b)))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 4 points increase in error, 0 points decrease in error
if -4.9999999999999997e303 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) < 9.99999999999999986e306
Initial program 0.9
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
Simplified0.9
\[\leadsto \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)}
\]
Proof
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 z c) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c a)) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 j (*.f64 c a)) (*.f64 j (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= cancel-sign-sub_binary64 (-.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub_binary64 (+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 y i)) j))): 0 points increase in error, 13 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 (*.f64 y i)) j)))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= distribute-rgt-in_binary64 (*.f64 j (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 c a) (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
Applied egg-rr0.9
\[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - \color{blue}{\left(\mathsf{fma}\left(-i, t, t \cdot i\right) \cdot b + b \cdot \left(z \cdot c - t \cdot i\right)\right)}\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
if 9.99999999999999986e306 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))
Initial program 63.2
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
Simplified63.2
\[\leadsto \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)}
\]
Proof
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 z c) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 c a)) (*.f64 y i)))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 j (*.f64 c a)) (*.f64 j (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= cancel-sign-sub_binary64 (-.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 (neg.f64 j) (neg.f64 (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub_binary64 (+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (*.f64 j (neg.f64 (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 (*.f64 c a) j)) (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 y i)) j))): 0 points increase in error, 13 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (+.f64 (*.f64 (*.f64 c a) j) (*.f64 (neg.f64 (*.f64 y i)) j)))): 13 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (Rewrite<= distribute-rgt-in_binary64 (*.f64 j (+.f64 (*.f64 c a) (neg.f64 (*.f64 y i)))))): 0 points increase in error, 13 points decrease in error
(+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 c a) (*.f64 y i))))): 13 points increase in error, 0 points decrease in error
Taylor expanded in z around 0 52.5
\[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - \color{blue}{-1 \cdot \left(i \cdot \left(t \cdot b\right)\right)}\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
Simplified52.5
\[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - \color{blue}{\left(-i\right) \cdot \left(t \cdot b\right)}\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
Proof
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (*.f64 z (*.f64 c b))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z c) b))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 4 points increase in error, 0 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 c z)) b)) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 0 points increase in error, 4 points decrease in error
(+.f64 (-.f64 (*.f64 y (*.f64 z x)) (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 z b)))) (+.f64 (*.f64 (fma.f64 (neg.f64 i) y (*.f64 y i)) j) (*.f64 j (-.f64 (*.f64 a c) (*.f64 y i))))): 4 points increase in error, 0 points decrease in error
herbie shell --seed 2022343
(FPCore (x y z t a b c i j)
:name "Data.Colour.Matrix:determinant from colour-2.3.3, A"
:precision binary64
:herbie-target
(if (< x -1.469694296777705e-64) (+ (- (* x (- (* y z) (* t a))) (/ (* b (- (pow (* c z) 2.0) (pow (* t i) 2.0))) (+ (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (if (< x 3.2113527362226803e-147) (- (* (- (* b i) (* x a)) t) (- (* z (* c b)) (* j (- (* c a) (* y i))))) (+ (- (* x (- (* y z) (* t a))) (/ (* b (- (pow (* c z) 2.0) (pow (* t i) 2.0))) (+ (* c z) (* t i)))) (* j (- (* c a) (* y i))))))
(+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))))