\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
↓
\[\begin{array}{l}
t_1 := b \cdot \left(a \cdot i - z \cdot c\right)\\
t_2 := j \cdot \left(t \cdot c - y \cdot i\right)\\
t_3 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_4 := t_2 + \left(t_1 + t_3\right)\\
\mathbf{if}\;t_4 \leq -2 \cdot 10^{+293} \lor \neg \left(t_4 \leq 5 \cdot 10^{+292}\right):\\
\;\;\;\;\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + t_3\\
\mathbf{else}:\\
\;\;\;\;\left(t_3 + \left(t_1 - b \cdot \mathsf{fma}\left(-a, i, a \cdot i\right)\right)\right) + t_2\\
\end{array}
\]
(FPCore (x y z t a b c i j)
:precision binary64
(+
(- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a))))
(* j (- (* c t) (* i y)))))
↓
(FPCore (x y z t a b c i j)
:precision binary64
(let* ((t_1 (* b (- (* a i) (* z c))))
(t_2 (* j (- (* t c) (* y i))))
(t_3 (* x (- (* y z) (* t a))))
(t_4 (+ t_2 (+ t_1 t_3))))
(if (or (<= t_4 -2e+293) (not (<= t_4 5e+292)))
(+ (- (* c (- (* t j) (* z b))) (* i (- (* y j) (* a b)))) t_3)
(+ (+ t_3 (- t_1 (* b (fma (- a) i (* a i))))) t_2))))
if (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) < -1.9999999999999998e293 or 4.9999999999999996e292 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))))
Initial program 82.03
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Simplified82.02
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, a \cdot i - z \cdot c, j \cdot \left(t \cdot c - y \cdot i\right)\right)\right)}
\]
Proof
[Start]82.03
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
associate-+l- [=>]82.03
\[ \color{blue}{x \cdot \left(y \cdot z - t \cdot a\right) - \left(b \cdot \left(c \cdot z - i \cdot a\right) - j \cdot \left(c \cdot t - i \cdot y\right)\right)}
\]
fma-neg [=>]82.03
\[ \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, -\left(b \cdot \left(c \cdot z - i \cdot a\right) - j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)}
\]
neg-sub0 [=>]82.03
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{0 - \left(b \cdot \left(c \cdot z - i \cdot a\right) - j \cdot \left(c \cdot t - i \cdot y\right)\right)}\right)
\]
associate-+l- [<=]82.03
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(0 - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)}\right)
\]
neg-sub0 [<=]82.03
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(-b \cdot \left(c \cdot z - i \cdot a\right)\right)} + j \cdot \left(c \cdot t - i \cdot y\right)\right)
\]
distribute-rgt-neg-in [=>]82.03
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{b \cdot \left(-\left(c \cdot z - i \cdot a\right)\right)} + j \cdot \left(c \cdot t - i \cdot y\right)\right)
\]
fma-def [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\mathsf{fma}\left(b, -\left(c \cdot z - i \cdot a\right), j \cdot \left(c \cdot t - i \cdot y\right)\right)}\right)
\]
sub-neg [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, -\color{blue}{\left(c \cdot z + \left(-i \cdot a\right)\right)}, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
distribute-neg-in [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-c \cdot z\right) + \left(-\left(-i \cdot a\right)\right)}, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
+-commutative [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-\left(-i \cdot a\right)\right) + \left(-c \cdot z\right)}, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
remove-double-neg [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{i \cdot a} + \left(-c \cdot z\right), j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
sub-neg [<=]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{i \cdot a - c \cdot z}, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
*-commutative [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{a \cdot i} - c \cdot z, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
*-commutative [=>]82.02
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, a \cdot i - \color{blue}{z \cdot c}, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)
\]
Taylor expanded in i around -inf 37.38
\[\leadsto \color{blue}{-1 \cdot \left(c \cdot \left(b \cdot z\right)\right) + \left(-1 \cdot \left(i \cdot \left(y \cdot j + -1 \cdot \left(a \cdot b\right)\right)\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(t \cdot j\right)\right)\right)}
\]
Simplified37.38
\[\leadsto \color{blue}{\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + x \cdot \left(y \cdot z - t \cdot a\right)}
\]
Proof
[Start]37.38
\[ -1 \cdot \left(c \cdot \left(b \cdot z\right)\right) + \left(-1 \cdot \left(i \cdot \left(y \cdot j + -1 \cdot \left(a \cdot b\right)\right)\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(t \cdot j\right)\right)\right)
\]
associate-+r+ [=>]37.38
\[ \color{blue}{\left(-1 \cdot \left(c \cdot \left(b \cdot z\right)\right) + -1 \cdot \left(i \cdot \left(y \cdot j + -1 \cdot \left(a \cdot b\right)\right)\right)\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(t \cdot j\right)\right)}
\]
\[ \color{blue}{\left(\left(-1 \cdot \left(c \cdot \left(b \cdot z\right)\right) + -1 \cdot \left(i \cdot \left(y \cdot j + -1 \cdot \left(a \cdot b\right)\right)\right)\right) + c \cdot \left(t \cdot j\right)\right) + x \cdot \left(y \cdot z - t \cdot a\right)}
\]
if -1.9999999999999998e293 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) < 4.9999999999999996e292
Initial program 1.4
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Applied egg-rr1.39
\[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - \color{blue}{\left(\mathsf{fma}\left(-a, i, i \cdot a\right) \cdot b + b \cdot \left(c \cdot z - i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Recombined 2 regimes into one program.
Final simplification9.37
\[\leadsto \begin{array}{l}
\mathbf{if}\;j \cdot \left(t \cdot c - y \cdot i\right) + \left(b \cdot \left(a \cdot i - z \cdot c\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right) \leq -2 \cdot 10^{+293} \lor \neg \left(j \cdot \left(t \cdot c - y \cdot i\right) + \left(b \cdot \left(a \cdot i - z \cdot c\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right) \leq 5 \cdot 10^{+292}\right):\\
\;\;\;\;\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + x \cdot \left(y \cdot z - t \cdot a\right)\\
\mathbf{else}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + \left(b \cdot \left(a \cdot i - z \cdot c\right) - b \cdot \mathsf{fma}\left(-a, i, a \cdot i\right)\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\end{array}
\]
Alternatives
Alternative 1
Error
9.37%
Cost
5833
\[\begin{array}{l}
t_1 := b \cdot \left(a \cdot i - z \cdot c\right)\\
t_2 := j \cdot \left(t \cdot c - y \cdot i\right)\\
t_3 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_4 := t_2 + \left(t_1 + t_3\right)\\
\mathbf{if}\;t_4 \leq -2 \cdot 10^{+293} \lor \neg \left(t_4 \leq 5 \cdot 10^{+292}\right):\\
\;\;\;\;\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + t_3\\
\mathbf{else}:\\
\;\;\;\;\left(\left(x \cdot \left(y \cdot z\right) - x \cdot \left(t \cdot a\right)\right) + t_1\right) + t_2\\
\end{array}
\]
Alternative 2
Error
9.37%
Cost
5705
\[\begin{array}{l}
t_1 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_2 := j \cdot \left(t \cdot c - y \cdot i\right) + \left(b \cdot \left(a \cdot i - z \cdot c\right) + t_1\right)\\
\mathbf{if}\;t_2 \leq -2 \cdot 10^{+293} \lor \neg \left(t_2 \leq 5 \cdot 10^{+292}\right):\\
\;\;\;\;\left(c \cdot \left(t \cdot j - z \cdot b\right) - i \cdot \left(y \cdot j - a \cdot b\right)\right) + t_1\\
\mathbf{else}:\\
\;\;\;\;t_2\\
\end{array}
\]
herbie shell --seed 2023088
(FPCore (x y z t a b c i j)
:name "Linear.Matrix:det33 from linear-1.19.1.3"
:precision binary64
:herbie-target
(if (< t -8.120978919195912e-33) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t -4.712553818218485e-169) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (if (< t -7.633533346031584e-308) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t 1.0535888557455487e-139) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j)))))))
(+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))))