\[\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 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right) + t_1\\
t_3 := t_2 + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_3 \leq -\infty:\\
\;\;\;\;i \cdot \left(t \cdot b\right) + y \cdot \left(x \cdot z - i \cdot j\right)\\
\mathbf{elif}\;t_3 \leq 5 \cdot 10^{+294}:\\
\;\;\;\;t_2 + \left(j \cdot \left(a \cdot c\right) - j \cdot \left(y \cdot i\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right) + \left(y \cdot \left(x \cdot z\right) + 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 (* b (- (* t i) (* z c))))
(t_2 (+ (* x (- (* y z) (* t a))) t_1))
(t_3 (+ t_2 (* j (- (* a c) (* y i))))))
(if (<= t_3 (- INFINITY))
(+ (* i (* t b)) (* y (- (* x z) (* i j))))
(if (<= t_3 5e+294)
(+ t_2 (- (* j (* a c)) (* j (* y i))))
(+ (- (* c (* a j)) (* y (* i j))) (+ (* y (* x z)) 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
Initial program 0.0%
\[\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.0%
\[\leadsto \color{blue}{\mathsf{fma}\left(b, t \cdot i - z \cdot c, \mathsf{fma}\left(x, y \cdot z - t \cdot a, j \cdot \left(a \cdot c - y \cdot i\right)\right)\right)}
\]
Proof
[Start]0.0
\[ \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 [=>]0.0
\[ \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) + \left(-b \cdot \left(c \cdot z - t \cdot i\right)\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)
\]
+-commutative [=>]0.0
\[ \color{blue}{\left(\left(-b \cdot \left(c \cdot z - t \cdot i\right)\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)
\]
associate-+l+ [=>]0.0
\[ \color{blue}{\left(-b \cdot \left(c \cdot z - t \cdot i\right)\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right)}
\]
distribute-rgt-neg-in [=>]0.0
\[ \color{blue}{b \cdot \left(-\left(c \cdot z - t \cdot i\right)\right)} + \left(x \cdot \left(y \cdot z - t \cdot a\right) + j \cdot \left(c \cdot a - y \cdot i\right)\right)
\]
+-commutative [<=]0.0
\[ b \cdot \left(-\left(c \cdot z - t \cdot i\right)\right) + \color{blue}{\left(j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)}
\]
fma-def [=>]0.0
\[ \color{blue}{\mathsf{fma}\left(b, -\left(c \cdot z - t \cdot i\right), j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)}
\]
sub-neg [=>]0.0
\[ \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) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
+-commutative [=>]0.0
\[ \mathsf{fma}\left(b, -\color{blue}{\left(\left(-t \cdot i\right) + c \cdot z\right)}, j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
distribute-neg-in [=>]0.0
\[ \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) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
unsub-neg [=>]0.0
\[ \mathsf{fma}\left(b, \color{blue}{\left(-\left(-t \cdot i\right)\right) - c \cdot z}, j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
remove-double-neg [=>]0.0
\[ \mathsf{fma}\left(b, \color{blue}{t \cdot i} - c \cdot z, j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
*-commutative [=>]0.0
\[ \mathsf{fma}\left(b, t \cdot i - \color{blue}{z \cdot c}, j \cdot \left(c \cdot a - y \cdot i\right) + x \cdot \left(y \cdot z - t \cdot a\right)\right)
\]
Taylor expanded in c around 0 33.6%
\[\leadsto \color{blue}{i \cdot \left(t \cdot b\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + -1 \cdot \left(y \cdot \left(i \cdot j\right)\right)\right)}
\]
Taylor expanded in y around inf 44.1%
\[\leadsto i \cdot \left(t \cdot b\right) + \color{blue}{\left(z \cdot x + -1 \cdot \left(i \cdot j\right)\right) \cdot y}
\]
Simplified44.1%
\[\leadsto i \cdot \left(t \cdot b\right) + \color{blue}{\left(x \cdot z - i \cdot j\right) \cdot y}
\]
Proof
[Start]44.1
\[ i \cdot \left(t \cdot b\right) + \left(z \cdot x + -1 \cdot \left(i \cdot j\right)\right) \cdot y
\]
neg-mul-1 [<=]44.1
\[ i \cdot \left(t \cdot b\right) + \left(z \cdot x + \color{blue}{\left(-i \cdot j\right)}\right) \cdot y
\]
unsub-neg [=>]44.1
\[ i \cdot \left(t \cdot b\right) + \color{blue}{\left(z \cdot x - i \cdot j\right)} \cdot y
\]
*-commutative [=>]44.1
\[ i \cdot \left(t \cdot b\right) + \left(\color{blue}{x \cdot z} - i \cdot j\right) \cdot y
\]
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)))) < 4.9999999999999999e294
Initial program 98.6%
\[\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)
\]
Simplified98.6%
\[\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]98.6
\[ \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)
\]
cancel-sign-sub [<=]98.6
\[ \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(-j\right) \cdot \left(c \cdot a - y \cdot i\right)}
\]
cancel-sign-sub-inv [=>]98.6
\[ \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(-j\right)\right) \cdot \left(c \cdot a - y \cdot i\right)}
\]
*-commutative [=>]98.6
\[ \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(-j\right)\right) \cdot \left(c \cdot a - y \cdot i\right)
\]
remove-double-neg [=>]98.6
\[ \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 - y \cdot i\right)
\]
*-commutative [=>]98.6
\[ \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(\color{blue}{a \cdot c} - y \cdot i\right)
\]
Applied egg-rr98.6%
\[\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(\left(a \cdot c\right) \cdot j + \left(y \cdot \left(-i\right)\right) \cdot j\right)}
\]
Proof
[Start]98.6
\[ \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)
\]
sub-neg [=>]98.6
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \color{blue}{\left(a \cdot c + \left(-y \cdot i\right)\right)}
\]
distribute-rgt-in [=>]98.6
\[ \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(a \cdot c\right) \cdot j + \left(-y \cdot i\right) \cdot j\right)}
\]
distribute-rgt-neg-in [=>]98.6
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \left(\left(a \cdot c\right) \cdot j + \color{blue}{\left(y \cdot \left(-i\right)\right)} \cdot j\right)
\]
if 4.9999999999999999e294 < (+.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 14.7%
\[\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)
\]
Simplified14.7%
\[\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]14.7
\[ \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)
\]
cancel-sign-sub [<=]14.7
\[ \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(-j\right) \cdot \left(c \cdot a - y \cdot i\right)}
\]
cancel-sign-sub-inv [=>]14.7
\[ \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(-j\right)\right) \cdot \left(c \cdot a - y \cdot i\right)}
\]
*-commutative [=>]14.7
\[ \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(-j\right)\right) \cdot \left(c \cdot a - y \cdot i\right)
\]
remove-double-neg [=>]14.7
\[ \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 - y \cdot i\right)
\]
*-commutative [=>]14.7
\[ \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(\color{blue}{a \cdot c} - y \cdot i\right)
\]
Taylor expanded in y around 0 36.6%
\[\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(-1 \cdot \left(y \cdot \left(i \cdot j\right)\right) + c \cdot \left(a \cdot j\right)\right)}
\]
Taylor expanded in y around inf 47.4%
\[\leadsto \left(\color{blue}{y \cdot \left(z \cdot x\right)} - b \cdot \left(z \cdot c - t \cdot i\right)\right) + \left(-1 \cdot \left(y \cdot \left(i \cdot j\right)\right) + c \cdot \left(a \cdot j\right)\right)
\]
Recombined 3 regimes into one program.
Final simplification88.1%
\[\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 -\infty:\\
\;\;\;\;i \cdot \left(t \cdot b\right) + y \cdot \left(x \cdot z - i \cdot j\right)\\
\mathbf{elif}\;\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 5 \cdot 10^{+294}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right) + \left(j \cdot \left(a \cdot c\right) - j \cdot \left(y \cdot i\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right) + \left(y \cdot \left(x \cdot z\right) + b \cdot \left(t \cdot i - z \cdot c\right)\right)\\
\end{array}
\]
Alternatives
Alternative 1
Accuracy
90.0%
Cost
5704
\[\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:\\
\;\;\;\;i \cdot \left(t \cdot b\right) + y \cdot \left(x \cdot z - i \cdot j\right)\\
\mathbf{elif}\;t_1 \leq 2 \cdot 10^{+307}:\\
\;\;\;\;t_1\\
\mathbf{else}:\\
\;\;\;\;\left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right) + z \cdot \left(x \cdot y - b \cdot c\right)\\
\end{array}
\]
Alternative 2
Accuracy
88.1%
Cost
5704
\[\begin{array}{l}
t_1 := b \cdot \left(t \cdot i - z \cdot c\right)\\
t_2 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + t_1\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_2 \leq -\infty:\\
\;\;\;\;i \cdot \left(t \cdot b\right) + y \cdot \left(x \cdot z - i \cdot j\right)\\
\mathbf{elif}\;t_2 \leq 5 \cdot 10^{+294}:\\
\;\;\;\;t_2\\
\mathbf{else}:\\
\;\;\;\;\left(c \cdot \left(a \cdot j\right) - y \cdot \left(i \cdot j\right)\right) + \left(y \cdot \left(x \cdot z\right) + t_1\right)\\
\end{array}
\]
herbie shell --seed 2023147
(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)))))