(FPCore (x y z t a b c i j k)
:precision binary64
(-
(-
(+ (- (* (* (* (* x 18.0) y) z) t) (* (* a 4.0) t)) (* b c))
(* (* x 4.0) i))
(* (* j 27.0) k)))
↓
(FPCore (x y z t a b c i j k)
:precision binary64
(let* ((t_1 (* k (* j -27.0))))
(if (<= t -200000000000.0)
(+
(+ (* t (+ (* (* x 18.0) (* y z)) (* a -4.0))) (* b c))
(+ (* x (* i -4.0)) (* j (* k -27.0))))
(if (<= t 5e+68)
(+
(+
(* b c)
(+ (* x (+ (* y (* t (* 18.0 z))) (* i -4.0))) (* -4.0 (* t a))))
t_1)
(+
t_1
(+
(+ (* b c) (+ (* t (* z (* (* x 18.0) y))) (* t (* a -4.0))))
(* i (* x -4.0))))))))
(-.f64 (+.f64 (*.f64 t (-.f64 (*.f64 (*.f64 x 18) (*.f64 y z)) (*.f64 a 4))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 t (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 x 18) y) z)) (*.f64 a 4))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 4 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 4 points decrease in error
(-.f64 (+.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (neg.f64 (*.f64 (*.f64 a 4) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 (*.f64 a 4) t)) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 15 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 (*.f64 a 4) t))) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 15 points decrease in error
(-.f64 (+.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 (*.f64 a 4) t)) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 (*.f64 a 4) t))) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (neg.f64 (*.f64 (*.f64 a 4) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> associate-+l-_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c)))) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 1 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c))) (+.f64 (*.f64 x (*.f64 4 i)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 j 27) k)))): 0 points increase in error, 1 points decrease in error
(-.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c))) (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c))) (+.f64 (*.f64 (*.f64 x 4) i) (*.f64 (*.f64 j 27) k))): 16 points increase in error, 0 points decrease in error
(Rewrite<= associate--l-_binary64 (-.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 16 points decrease in error
\[\leadsto \color{blue}{\mathsf{fma}\left(t, \mathsf{fma}\left(x \cdot 18, y \cdot z, a \cdot -4\right), \mathsf{fma}\left(b, c, i \cdot \left(x \cdot -4\right)\right)\right) + k \cdot \left(j \cdot -27\right)}
\]
Proof
(-.f64 (+.f64 (*.f64 t (-.f64 (*.f64 (*.f64 x 18) (*.f64 y z)) (*.f64 a 4))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (*.f64 t (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 x 18) y) z)) (*.f64 a 4))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 4 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 4 points decrease in error
(-.f64 (+.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (neg.f64 (*.f64 (*.f64 a 4) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 (*.f64 a 4) t)) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 15 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 (*.f64 a 4) t))) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 15 points decrease in error
(-.f64 (+.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 (*.f64 a 4) t)) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 (*.f64 a 4) t))) (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t)) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (neg.f64 (*.f64 (*.f64 a 4) t)))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t))) (*.f64 b c)) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> associate-+l-_binary64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c)))) (+.f64 (*.f64 x (*.f64 4 i)) (*.f64 j (*.f64 27 k)))): 1 points increase in error, 0 points decrease in error
(-.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c))) (+.f64 (*.f64 x (*.f64 4 i)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 j 27) k)))): 0 points increase in error, 1 points decrease in error
(-.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (-.f64 (*.f64 (*.f64 a 4) t) (*.f64 b c))) (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c))) (+.f64 (*.f64 (*.f64 x 4) i) (*.f64 (*.f64 j 27) k))): 16 points increase in error, 0 points decrease in error
(Rewrite<= associate--l-_binary64 (-.f64 (-.f64 (+.f64 (-.f64 (*.f64 (*.f64 (*.f64 (*.f64 x 18) y) z) t) (*.f64 (*.f64 a 4) t)) (*.f64 b c)) (*.f64 (*.f64 x 4) i)) (*.f64 (*.f64 j 27) k))): 0 points increase in error, 16 points decrease in error
(+.f64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (*.f64 y (*.f64 t (*.f64 18 z))) (*.f64 -4 i)) x) (*.f64 -4 (*.f64 a t)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (*.f64 y (*.f64 t (Rewrite<= *-commutative_binary64 (*.f64 z 18)))) (*.f64 -4 i)) x) (*.f64 -4 (*.f64 a t)))) (*.f64 k (*.f64 j -27))): 5 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y t) (*.f64 z 18))) (*.f64 -4 i)) x) (*.f64 -4 (*.f64 a t)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 5 points decrease in error
(+.f64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (*.f64 (*.f64 y t) (*.f64 z 18))))) (*.f64 -4 i)) x) (*.f64 -4 (*.f64 a t)))) (*.f64 k (*.f64 j -27))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 c b) (+.f64 (*.f64 (+.f64 (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (*.f64 (*.f64 y t) (*.f64 z 18)))) 1)) (*.f64 -4 i)) x) (*.f64 -4 (*.f64 a t)))) (*.f64 k (*.f64 j -27))): 5 points increase in error, 0 points decrease in error
herbie shell --seed 2022340
(FPCore (x y z t a b c i j k)
:name "Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, E"
:precision binary64
:herbie-target
(if (< t -1.6210815397541398e-69) (- (- (* (* 18.0 t) (* (* x y) z)) (* (+ (* a t) (* i x)) 4.0)) (- (* (* k j) 27.0) (* c b))) (if (< t 165.68027943805222) (+ (- (* (* 18.0 y) (* x (* z t))) (* (+ (* a t) (* i x)) 4.0)) (- (* c b) (* 27.0 (* k j)))) (- (- (* (* 18.0 t) (* (* x y) z)) (* (+ (* a t) (* i x)) 4.0)) (- (* (* k j) 27.0) (* c b)))))
(- (- (+ (- (* (* (* (* x 18.0) y) z) t) (* (* a 4.0) t)) (* b c)) (* (* x 4.0) i)) (* (* j 27.0) k)))