\[\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 z - t \cdot a\\
t_2 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := \left(x \cdot t_1 + t_2\right) + t_3\\
\mathbf{if}\;t_4 \leq -2 \cdot 10^{+284} \lor \neg \left(t_4 \leq 10^{+289}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + \left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\mathsf{fma}\left(x, t_1, \mathsf{fma}\left(-a, t, t \cdot a\right) \cdot \left(x + x\right)\right) + t_2\right) + t_3\\
\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 z) (* t a)))
(t_2 (* b (- (* t i) (* z c))))
(t_3 (* j (- (* a c) (* y i))))
(t_4 (+ (+ (* x t_1) t_2) t_3)))
(if (or (<= t_4 -2e+284) (not (<= t_4 1e+289)))
(+
(+ (* t (- (* b i) (* x a))) (- (* c (* a j)) (* y (* i j))))
(* z (- (* x y) (* b c))))
(+ (+ (fma x t_1 (* (fma (- a) t (* t a)) (+ x x))) t_2) t_3))))
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)))) < -2.00000000000000016e284 or 1.0000000000000001e289 < (+.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 73.88
\[\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)
\]
Simplified73.88
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - z \cdot c, j \cdot \left(a \cdot c - y \cdot i\right)\right)\right)}
\]
Proof
[Start]73.88
\[ \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)
\]
associate-+l- [=>]73.88
\[ \color{blue}{x \cdot \left(y \cdot z - t \cdot a\right) - \left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)}
\]
fma-neg [=>]73.88
\[ \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, -\left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)}
\]
neg-sub0 [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{0 - \left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)}\right)
\]
associate-+l- [<=]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(0 - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)}\right)
\]
neg-sub0 [<=]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(-b \cdot \left(c \cdot z - t \cdot i\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)\right)
\]
distribute-rgt-neg-in [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{b \cdot \left(-\left(c \cdot z - t \cdot i\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)\right)
\]
fma-def [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\mathsf{fma}\left(b, -\left(c \cdot z - t \cdot i\right), j \cdot \left(c \cdot a - y \cdot i\right)\right)}\right)
\]
sub-neg [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, -\color{blue}{\left(c \cdot z + \left(-t \cdot i\right)\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
distribute-neg-in [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-c \cdot z\right) + \left(-\left(-t \cdot i\right)\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
+-commutative [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-\left(-t \cdot i\right)\right) + \left(-c \cdot z\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
remove-double-neg [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{t \cdot i} + \left(-c \cdot z\right), j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
sub-neg [<=]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{t \cdot i - c \cdot z}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
*-commutative [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - \color{blue}{z \cdot c}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
*-commutative [=>]73.88
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - z \cdot c, j \cdot \left(\color{blue}{a \cdot c} - y \cdot i\right)\right)\right)
\]
\[\leadsto \color{blue}{\left(t \cdot \left(i \cdot b - a \cdot x\right) + j \cdot \left(c \cdot a - i \cdot y\right)\right) - z \cdot \left(c \cdot b - y \cdot x\right)}
\]
Proof
[Start]43.3
\[ i \cdot \left(t \cdot b\right) + \left(-1 \cdot \left(\left(c \cdot b + -1 \cdot \left(y \cdot x\right)\right) \cdot z\right) + \left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
+-commutative [=>]43.3
\[ i \cdot \left(t \cdot b\right) + \color{blue}{\left(\left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right) + -1 \cdot \left(\left(c \cdot b + -1 \cdot \left(y \cdot x\right)\right) \cdot z\right)\right)}
\]
mul-1-neg [=>]43.3
\[ i \cdot \left(t \cdot b\right) + \left(\left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right) + \color{blue}{\left(-\left(c \cdot b + -1 \cdot \left(y \cdot x\right)\right) \cdot z\right)}\right)
\]
unsub-neg [=>]43.3
\[ i \cdot \left(t \cdot b\right) + \color{blue}{\left(\left(-1 \cdot \left(a \cdot \left(t \cdot x\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right) - \left(c \cdot b + -1 \cdot \left(y \cdot x\right)\right) \cdot z\right)}
\]
\[\leadsto \left(t \cdot \left(i \cdot b - a \cdot x\right) + \color{blue}{\left(-1 \cdot \left(y \cdot \left(i \cdot j\right)\right) + c \cdot \left(a \cdot j\right)\right)}\right) - z \cdot \left(c \cdot b - y \cdot x\right)
\]
if -2.00000000000000016e284 < (+.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)))) < 1.0000000000000001e289
Initial program 1.11
\[\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)
\]
Simplified1.11
\[\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
[Start]1.11
\[ \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)
\]
sub-neg [=>]1.11
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \color{blue}{\left(c \cdot a + \left(-y \cdot i\right)\right)}
\]
distribute-rgt-in [=>]1.11
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + \color{blue}{\left(\left(c \cdot a\right) \cdot j + \left(-y \cdot i\right) \cdot j\right)}
\]
associate-+r+ [=>]1.11
\[ \color{blue}{\left(\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + \left(c \cdot a\right) \cdot j\right) + \left(-y \cdot i\right) \cdot j}
\]
*-commutative [=>]1.11
\[ \left(\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + \left(c \cdot a\right) \cdot j\right) + \color{blue}{j \cdot \left(-y \cdot i\right)}
\]
cancel-sign-sub [<=]1.11
\[ \color{blue}{\left(\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + \left(c \cdot a\right) \cdot j\right) - \left(-j\right) \cdot \left(-y \cdot i\right)}
\]
associate-+r- [<=]1.11
\[ \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + \left(\left(c \cdot a\right) \cdot j - \left(-j\right) \cdot \left(-y \cdot i\right)\right)}
\]
*-commutative [=>]1.11
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - t \cdot i\right)\right) + \left(\left(c \cdot a\right) \cdot j - \left(-j\right) \cdot \left(-y \cdot i\right)\right)
\]
cancel-sign-sub [=>]1.11
\[ \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(\left(c \cdot a\right) \cdot j + j \cdot \left(-y \cdot i\right)\right)}
\]
*-commutative [<=]1.11
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \left(\left(c \cdot a\right) \cdot j + \color{blue}{\left(-y \cdot i\right) \cdot j}\right)
\]
distribute-rgt-in [<=]1.11
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \color{blue}{j \cdot \left(c \cdot a + \left(-y \cdot i\right)\right)}
\]
Applied egg-rr1.14
\[\leadsto \left(\color{blue}{\left(x \cdot \left(z \cdot y - t \cdot a\right) + \left(x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right) + x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right)\right)\right)} - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
Simplified1.13
\[\leadsto \left(\color{blue}{\mathsf{fma}\left(x, z \cdot y - t \cdot a, \mathsf{fma}\left(-a, t, t \cdot a\right) \cdot \left(x + x\right)\right)} - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
Proof
[Start]1.14
\[ \left(\left(x \cdot \left(z \cdot y - t \cdot a\right) + \left(x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right) + x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right)\right)\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
fma-def [=>]1.12
\[ \left(\color{blue}{\mathsf{fma}\left(x, z \cdot y - t \cdot a, x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right) + x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right)\right)} - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
distribute-rgt-out [=>]1.13
\[ \left(\mathsf{fma}\left(x, z \cdot y - t \cdot a, \color{blue}{\mathsf{fma}\left(-a, t, t \cdot a\right) \cdot \left(x + x\right)}\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)
\]
Recombined 2 regimes into one program.
Final simplification6.9
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right) \leq -2 \cdot 10^{+284} \lor \neg \left(\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right) \leq 10^{+289}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + \left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(-a, t, t \cdot a\right) \cdot \left(x + x\right)\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\end{array}
\]
Alternatives
Alternative 1
Error
5.33%
Cost
19081
\[\begin{array}{l}
t_1 := a \cdot c - y \cdot i\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\\
t_3 := t_2 + j \cdot t_1\\
\mathbf{if}\;t_3 \leq -\infty \lor \neg \left(t_3 \leq 10^{+289}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + \left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;t_2 + \mathsf{fma}\left(j, t_1, \mathsf{fma}\left(-i, y, y \cdot i\right) \cdot \left(j + j\right)\right)\\
\end{array}
\]
Alternative 2
Error
5.32%
Cost
11977
\[\begin{array}{l}
t_1 := a \cdot c - y \cdot i\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\\
t_3 := t_2 + j \cdot t_1\\
\mathbf{if}\;t_3 \leq -\infty \lor \neg \left(t_3 \leq 10^{+289}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + \left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(j, t_1, t_2\right)\\
\end{array}
\]
Alternative 3
Error
5.32%
Cost
5833
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -\infty \lor \neg \left(t_1 \leq 10^{+289}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + \left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
Alternative 4
Error
8.98%
Cost
5705
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -\infty \lor \neg \left(t_1 \leq 10^{+297}\right):\\
\;\;\;\;t \cdot \left(b \cdot i - x \cdot a\right) + c \cdot \left(a \cdot j - z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
Alternative 5
Error
8.46%
Cost
5704
\[\begin{array}{l}
t_1 := t \cdot \left(b \cdot i - x \cdot a\right)\\
t_2 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_3 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + t_2\\
\mathbf{if}\;t_3 \leq -\infty:\\
\;\;\;\;\left(t_1 + t_2\right) - z \cdot \left(b \cdot c - x \cdot y\right)\\
\mathbf{elif}\;t_3 \leq 10^{+297}:\\
\;\;\;\;t_3\\
\mathbf{else}:\\
\;\;\;\;t_1 + c \cdot \left(a \cdot j - z \cdot b\right)\\
\end{array}
\]
Alternative 6
Error
41.05%
Cost
2932
\[\begin{array}{l}
t_1 := t \cdot \left(b \cdot i - x \cdot a\right)\\
t_2 := a \cdot \left(x \cdot t\right)\\
t_3 := i \cdot \left(t \cdot b - y \cdot j\right)\\
t_4 := c \cdot \left(a \cdot j - z \cdot b\right)\\
t_5 := t_1 + t_4\\
t_6 := t_4 - x \cdot \left(t \cdot a - y \cdot z\right)\\
t_7 := z \cdot \left(x \cdot y - b \cdot c\right)\\
t_8 := t_7 + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;c \leq -9.2 \cdot 10^{+48}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;c \leq -3.1 \cdot 10^{-50}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;c \leq -4.8 \cdot 10^{-62}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;c \leq -5 \cdot 10^{-128}:\\
\;\;\;\;t_8\\
\mathbf{elif}\;c \leq -1.35 \cdot 10^{-145}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;c \leq -2.7 \cdot 10^{-194}:\\
\;\;\;\;t_8\\
\mathbf{elif}\;c \leq -9.8 \cdot 10^{-244}:\\
\;\;\;\;b \cdot \left(t \cdot i - z \cdot c\right) - t_2\\
\mathbf{elif}\;c \leq -4.5 \cdot 10^{-272}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;c \leq 8.8 \cdot 10^{-287}:\\
\;\;\;\;x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c\right)\\
\mathbf{elif}\;c \leq 4.8 \cdot 10^{-240}:\\
\;\;\;\;t_8\\
\mathbf{elif}\;c \leq 4.5 \cdot 10^{-224}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;c \leq 2.08 \cdot 10^{-190}:\\
\;\;\;\;t_7 - t_2\\
\mathbf{elif}\;c \leq 8.5 \cdot 10^{-55}:\\
\;\;\;\;t_8\\
\mathbf{else}:\\
\;\;\;\;t_5\\
\end{array}
\]
herbie shell --seed 2023121
(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)))))