\[\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 := x \cdot z - i \cdot j\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\\
t_3 := t \cdot c - y \cdot i\\
t_4 := t_2 + j \cdot t_3\\
\mathbf{if}\;t_4 \leq -\infty:\\
\;\;\;\;\mathsf{fma}\left(y, t_1, t \cdot \left(c \cdot j - x \cdot a\right)\right)\\
\mathbf{elif}\;t_4 \leq 10^{+305}:\\
\;\;\;\;\mathsf{fma}\left(j, t_3, t_2\right)\\
\mathbf{else}:\\
\;\;\;\;y \cdot t_1 + \left(i \cdot \left(a \cdot b\right) - c \cdot \left(z \cdot b\right)\right)\\
\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 (- (* x z) (* i j)))
(t_2 (+ (* x (- (* y z) (* t a))) (* b (- (* a i) (* z c)))))
(t_3 (- (* t c) (* y i)))
(t_4 (+ t_2 (* j t_3))))
(if (<= t_4 (- INFINITY))
(fma y t_1 (* t (- (* c j) (* x a))))
(if (<= t_4 1e+305)
(fma j t_3 t_2)
(+ (* y t_1) (- (* i (* a b)) (* c (* z b))))))))
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)))) < -inf.0
Initial program 64.0
\[\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)
\]
Simplified64.0
\[\leadsto \color{blue}{\mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \cdot i\right)\right)}
\]
Proof
[Start]64.0
\[ \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)
\]
+-commutative [=>]64.0
\[ \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
fma-def [=>]64.0
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot t - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
*-commutative [=>]64.0
\[ \mathsf{fma}\left(j, \color{blue}{t \cdot c} - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]64.0
\[ \mathsf{fma}\left(j, t \cdot c - \color{blue}{y \cdot i}, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]64.0
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - i \cdot a\right)\right)
\]
*-commutative [=>]64.0
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - \color{blue}{a \cdot i}\right)\right)
\]
Taylor expanded in b around 0 57.8
\[\leadsto \color{blue}{\left(c \cdot t - i \cdot y\right) \cdot j + \left(y \cdot z - a \cdot t\right) \cdot x}
\]
Simplified25.4
\[\leadsto \color{blue}{\mathsf{fma}\left(y, z \cdot x - i \cdot j, t \cdot \left(c \cdot j - a \cdot x\right)\right)}
\]
Proof
[Start]57.8
\[ \left(c \cdot t - i \cdot y\right) \cdot j + \left(y \cdot z - a \cdot t\right) \cdot x
\]
+-commutative [=>]57.8
\[ \color{blue}{\left(y \cdot z - a \cdot t\right) \cdot x + \left(c \cdot t - i \cdot y\right) \cdot j}
\]
*-commutative [=>]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right)}
\]
*-commutative [<=]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + j \cdot \left(\color{blue}{t \cdot c} - i \cdot y\right)
\]
*-commutative [<=]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + j \cdot \left(t \cdot c - \color{blue}{y \cdot i}\right)
\]
sub-neg [=>]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + j \cdot \color{blue}{\left(t \cdot c + \left(-y \cdot i\right)\right)}
\]
distribute-lft-in [=>]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + \color{blue}{\left(j \cdot \left(t \cdot c\right) + j \cdot \left(-y \cdot i\right)\right)}
\]
*-commutative [<=]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + \left(\color{blue}{\left(t \cdot c\right) \cdot j} + j \cdot \left(-y \cdot i\right)\right)
\]
*-commutative [=>]57.8
\[ \left(y \cdot z - a \cdot t\right) \cdot x + \left(\color{blue}{\left(c \cdot t\right)} \cdot j + j \cdot \left(-y \cdot i\right)\right)
\]
associate-*r* [<=]49.9
\[ \left(y \cdot z - a \cdot t\right) \cdot x + \left(\color{blue}{c \cdot \left(t \cdot j\right)} + j \cdot \left(-y \cdot i\right)\right)
\]
associate-+r+ [=>]49.9
\[ \color{blue}{\left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(t \cdot j\right)\right) + j \cdot \left(-y \cdot i\right)}
\]
if -inf.0 < (+.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)))) < 9.9999999999999994e304
Initial program 0.9
\[\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)
\]
Simplified0.9
\[\leadsto \color{blue}{\mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \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 - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
+-commutative [=>]0.9
\[ \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
fma-def [=>]0.9
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot t - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, \color{blue}{t \cdot c} - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, t \cdot c - \color{blue}{y \cdot i}, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - i \cdot a\right)\right)
\]
*-commutative [=>]0.9
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - \color{blue}{a \cdot i}\right)\right)
\]
if 9.9999999999999994e304 < (+.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 61.3
\[\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)
\]
Simplified61.3
\[\leadsto \color{blue}{\mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \cdot i\right)\right)}
\]
Proof
[Start]61.3
\[ \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)
\]
+-commutative [=>]61.3
\[ \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
fma-def [=>]61.3
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot t - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
*-commutative [=>]61.3
\[ \mathsf{fma}\left(j, \color{blue}{t \cdot c} - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]61.3
\[ \mathsf{fma}\left(j, t \cdot c - \color{blue}{y \cdot i}, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]61.3
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - i \cdot a\right)\right)
\]
*-commutative [=>]61.3
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - \color{blue}{a \cdot i}\right)\right)
\]
\[\leadsto y \cdot \left(z \cdot x - i \cdot j\right) + \color{blue}{\left(i \cdot \left(a \cdot b\right) + -1 \cdot \left(c \cdot \left(z \cdot b\right)\right)\right)}
\]
Recombined 3 regimes into one program.
Final simplification5.5
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right) \leq -\infty:\\
\;\;\;\;\mathsf{fma}\left(y, x \cdot z - i \cdot j, t \cdot \left(c \cdot j - x \cdot a\right)\right)\\
\mathbf{elif}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right) \leq 10^{+305}:\\
\;\;\;\;\mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right)\\
\mathbf{else}:\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + \left(i \cdot \left(a \cdot b\right) - c \cdot \left(z \cdot b\right)\right)\\
\end{array}
\]
Alternatives
Alternative 1
Error
5.5
Cost
9412
\[\begin{array}{l}
t_1 := b \cdot \left(z \cdot c - a \cdot i\right)\\
t_2 := x \cdot z - i \cdot j\\
t_3 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_3 \leq -\infty:\\
\;\;\;\;\mathsf{fma}\left(y, t_2, t \cdot \left(c \cdot j - x \cdot a\right)\right)\\
\mathbf{elif}\;t_3 \leq 10^{+305}:\\
\;\;\;\;\left(t_1 - j \cdot \left(y \cdot i - t \cdot c\right)\right) - \left(t_1 \cdot 2 + x \cdot \left(t \cdot a - y \cdot z\right)\right)\\
\mathbf{else}:\\
\;\;\;\;y \cdot t_2 + \left(i \cdot \left(a \cdot b\right) - c \cdot \left(z \cdot b\right)\right)\\
\end{array}
\]
Alternative 2
Error
5.9
Cost
6472
\[\begin{array}{l}
t_1 := b \cdot \left(z \cdot c - a \cdot i\right)\\
t_2 := c \cdot \left(z \cdot b\right)\\
t_3 := j \cdot \left(t \cdot c - y \cdot i\right)\\
t_4 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + t_3\\
\mathbf{if}\;t_4 \leq -1 \cdot 10^{+304}:\\
\;\;\;\;\left(t_3 + \left(y \cdot \left(x \cdot z\right) + a \cdot \left(b \cdot i - x \cdot t\right)\right)\right) - t_2\\
\mathbf{elif}\;t_4 \leq 10^{+305}:\\
\;\;\;\;\left(t_1 - j \cdot \left(y \cdot i - t \cdot c\right)\right) - \left(t_1 \cdot 2 + x \cdot \left(t \cdot a - y \cdot z\right)\right)\\
\mathbf{else}:\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + \left(i \cdot \left(a \cdot b\right) - t_2\right)\\
\end{array}
\]
Alternative 3
Error
5.6
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 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + t_1\right) + t_2\\
\mathbf{if}\;t_3 \leq -\infty \lor \neg \left(t_3 \leq 10^{+305}\right):\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + \left(i \cdot \left(a \cdot b\right) - c \cdot \left(z \cdot b\right)\right)\\
\mathbf{else}:\\
\;\;\;\;t_2 + \left(\left(x \cdot \left(y \cdot z\right) - x \cdot \left(t \cdot a\right)\right) + t_1\right)\\
\end{array}
\]
Alternative 4
Error
5.9
Cost
5832
\[\begin{array}{l}
t_1 := b \cdot \left(a \cdot i - z \cdot c\right)\\
t_2 := c \cdot \left(z \cdot b\right)\\
t_3 := j \cdot \left(t \cdot c - y \cdot i\right)\\
t_4 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + t_1\right) + t_3\\
\mathbf{if}\;t_4 \leq -1 \cdot 10^{+304}:\\
\;\;\;\;\left(t_3 + \left(y \cdot \left(x \cdot z\right) + a \cdot \left(b \cdot i - x \cdot t\right)\right)\right) - t_2\\
\mathbf{elif}\;t_4 \leq 10^{+305}:\\
\;\;\;\;t_3 + \left(\left(x \cdot \left(y \cdot z\right) - x \cdot \left(t \cdot a\right)\right) + t_1\right)\\
\mathbf{else}:\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + \left(i \cdot \left(a \cdot b\right) - t_2\right)\\
\end{array}
\]
Alternative 5
Error
5.6
Cost
5705
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -\infty \lor \neg \left(t_1 \leq 10^{+305}\right):\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right) + \left(i \cdot \left(a \cdot b\right) - c \cdot \left(z \cdot b\right)\right)\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
herbie shell --seed 2023057
(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)))))