\[\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 := x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\\
t_2 := a \cdot c - y \cdot i\\
t_3 := j \cdot t_2 + t_1\\
\mathbf{if}\;t_3 \leq -\infty \lor \neg \left(t_3 \leq 4 \cdot 10^{+307}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + c \cdot \left(a \cdot j\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(j, t_2, t_1\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 (- (* x (- (* y z) (* t a))) (* b (- (* z c) (* t i)))))
(t_2 (- (* a c) (* y i)))
(t_3 (+ (* j t_2) t_1)))
(if (or (<= t_3 (- INFINITY)) (not (<= t_3 4e+307)))
(+ (+ (* t (- (* b i) (* x a))) (* c (* a j))) (* z (- (* x y) (* b c))))
(fma j t_2 t_1))))
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)))) < -inf.0 or 3.99999999999999994e307 < (+.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.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)
\]
Simplified63.8
\[\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]63.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)
\]
associate-+l- [=>]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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- [<=]63.8
\[ \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 [<=]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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 [<=]63.8
\[ \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 [=>]63.8
\[ \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 [=>]63.8
\[ \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]29.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 [=>]29.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 [=>]29.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 [=>]29.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}{c \cdot \left(a \cdot j\right)}\right) - z \cdot \left(c \cdot b - y \cdot x\right)
\]
if -inf.0 < (+.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)))) < 3.99999999999999994e307
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}{\mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right)}
\]
Proof
[Start]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)
\]
+-commutative [=>]0.9
\[ \color{blue}{j \cdot \left(c \cdot a - y \cdot i\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)}
\]
fma-def [=>]0.9
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot a - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)}
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, \color{blue}{a \cdot c} - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - t \cdot i\right)\right)
\]
Recombined 2 regimes into one program.
Final simplification3.7
\[\leadsto \begin{array}{l}
\mathbf{if}\;j \cdot \left(a \cdot c - y \cdot i\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) \leq -\infty \lor \neg \left(j \cdot \left(a \cdot c - y \cdot i\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) \leq 4 \cdot 10^{+307}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + c \cdot \left(a \cdot j\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right)\\
\end{array}
\]
Alternatives
Alternative 1
Error
3.7
Cost
5705
\[\begin{array}{l}
t_1 := j \cdot \left(a \cdot c - y \cdot i\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right)\\
\mathbf{if}\;t_1 \leq -\infty \lor \neg \left(t_1 \leq 4 \cdot 10^{+307}\right):\\
\;\;\;\;\left(t \cdot \left(b \cdot i - x \cdot a\right) + c \cdot \left(a \cdot j\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
Alternative 2
Error
21.2
Cost
3052
\[\begin{array}{l}
t_1 := c \cdot \left(a \cdot j\right)\\
t_2 := \left(t \cdot \left(b \cdot i - x \cdot a\right) + t_1\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
t_3 := \left(y \cdot \left(x \cdot z\right) + j \cdot \left(a \cdot c - y \cdot i\right)\right) - c \cdot \left(z \cdot b\right)\\
t_4 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_5 := \left(t_1 - a \cdot \left(x \cdot t\right)\right) + t_4\\
t_6 := y \cdot \left(x \cdot z - i \cdot j\right) + t_4\\
t_7 := \left(j \cdot \left(a \cdot c\right) - x \cdot \left(t \cdot a\right)\right) - z \cdot \left(b \cdot c - x \cdot y\right)\\
\mathbf{if}\;t \leq -7.2 \cdot 10^{+67}:\\
\;\;\;\;t_2\\
\mathbf{elif}\;t \leq -1.45 \cdot 10^{-108}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;t \leq -7.2 \cdot 10^{-155}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;t \leq 4.5 \cdot 10^{-297}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;t \leq 1.3 \cdot 10^{-225}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;t \leq 1.25 \cdot 10^{-191}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;t \leq 1.65 \cdot 10^{-90}:\\
\;\;\;\;t_7\\
\mathbf{elif}\;t \leq 1.2 \cdot 10^{-35}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;t \leq 16200:\\
\;\;\;\;t_6\\
\mathbf{elif}\;t \leq 4 \cdot 10^{+23}:\\
\;\;\;\;t_7\\
\mathbf{elif}\;t \leq 6 \cdot 10^{+59}:\\
\;\;\;\;t_5\\
\mathbf{else}:\\
\;\;\;\;t_2\\
\end{array}
\]
Alternative 3
Error
22.4
Cost
2800
\[\begin{array}{l}
t_1 := t \cdot \left(b \cdot i - x \cdot a\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
t_2 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_3 := \left(c \cdot \left(a \cdot j\right) - a \cdot \left(x \cdot t\right)\right) + t_2\\
t_4 := \left(j \cdot \left(a \cdot c\right) - x \cdot \left(t \cdot a\right)\right) - z \cdot \left(b \cdot c - x \cdot y\right)\\
t_5 := x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\\
t_6 := i \cdot \left(t \cdot b - y \cdot j\right) + c \cdot \left(a \cdot j - z \cdot b\right)\\
t_7 := y \cdot \left(x \cdot z - i \cdot j\right) + t_2\\
\mathbf{if}\;i \leq -4.4 \cdot 10^{+105}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;i \leq -1.6 \cdot 10^{-76}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;i \leq -5 \cdot 10^{-123}:\\
\;\;\;\;t_7\\
\mathbf{elif}\;i \leq -2.1 \cdot 10^{-144}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;i \leq -1.26 \cdot 10^{-173}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;i \leq -7 \cdot 10^{-235}:\\
\;\;\;\;t_4\\
\mathbf{elif}\;i \leq 2.05 \cdot 10^{-237}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;i \leq 6.2 \cdot 10^{-181}:\\
\;\;\;\;t_4\\
\mathbf{elif}\;i \leq 2 \cdot 10^{-73}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;i \leq 4.5 \cdot 10^{-39}:\\
\;\;\;\;t_7\\
\mathbf{elif}\;i \leq 1.4 \cdot 10^{-14}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;i \leq 0.0037:\\
\;\;\;\;t_5\\
\mathbf{else}:\\
\;\;\;\;t_6\\
\end{array}
\]
Alternative 4
Error
23.6
Cost
2669
\[\begin{array}{l}
t_1 := i \cdot \left(t \cdot b - y \cdot j\right) + c \cdot \left(a \cdot j - z \cdot b\right)\\
t_2 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_3 := x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\\
t_4 := t \cdot \left(b \cdot i - x \cdot a\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;x \leq -5.1 \cdot 10^{+151}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;x \leq -4.8 \cdot 10^{+23}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;x \leq -3.8 \cdot 10^{-5}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;x \leq -1.85 \cdot 10^{-175}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;x \leq -2.5 \cdot 10^{-215}:\\
\;\;\;\;c \cdot \left(a \cdot j\right) + t_2\\
\mathbf{elif}\;x \leq 3 \cdot 10^{-279}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;x \leq 6.4 \cdot 10^{-190}:\\
\;\;\;\;t_4\\
\mathbf{elif}\;x \leq 7 \cdot 10^{-110}:\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + t_2\\
\mathbf{elif}\;x \leq 2.9 \cdot 10^{-75} \lor \neg \left(x \leq 1.3 \cdot 10^{+99}\right) \land x \leq 1.75 \cdot 10^{+140}:\\
\;\;\;\;t_4\\
\mathbf{else}:\\
\;\;\;\;t_3\\
\end{array}
\]
Alternative 5
Error
23.8
Cost
2668
\[\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 := t_1 + t_2\\
t_4 := i \cdot \left(t \cdot b - y \cdot j\right) + c \cdot \left(a \cdot j - z \cdot b\right)\\
t_5 := y \cdot \left(x \cdot z - i \cdot j\right) + b \cdot \left(t \cdot i - z \cdot c\right)\\
t_6 := \left(t_1 + j \cdot \left(a \cdot c\right)\right) - b \cdot \left(z \cdot c\right)\\
\mathbf{if}\;i \leq -4.3 \cdot 10^{+105}:\\
\;\;\;\;t_4\\
\mathbf{elif}\;i \leq -3.8 \cdot 10^{-78}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;i \leq -3.2 \cdot 10^{-120}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;i \leq -2.6 \cdot 10^{-145}:\\
\;\;\;\;t_3\\
\mathbf{elif}\;i \leq -1.25 \cdot 10^{-184}:\\
\;\;\;\;x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\\
\mathbf{elif}\;i \leq -8.6 \cdot 10^{-235}:\\
\;\;\;\;z \cdot \left(x \cdot y - b \cdot c\right)\\
\mathbf{elif}\;i \leq 1.35 \cdot 10^{-237}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;i \leq 2.1 \cdot 10^{-194}:\\
\;\;\;\;\left(y \cdot \left(x \cdot z\right) + t_2\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{elif}\;i \leq 1.02 \cdot 10^{-122}:\\
\;\;\;\;t_6\\
\mathbf{elif}\;i \leq 9 \cdot 10^{-39}:\\
\;\;\;\;t_5\\
\mathbf{elif}\;i \leq 1.4 \cdot 10^{-5}:\\
\;\;\;\;t_3\\
\mathbf{else}:\\
\;\;\;\;t_4\\
\end{array}
\]
herbie shell --seed 2023018
(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)))))