(FPCore (n U t l Om U*)
:precision binary64
(sqrt
(*
(* (* 2.0 n) U)
(- (- t (* 2.0 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2.0)) (- U U*))))))
↓
(FPCore (n U t l Om U*)
:precision binary64
(let* ((t_1
(*
(* (* 2.0 n) U)
(+
(+ t (* (/ (* l l) Om) -2.0))
(* (* n (pow (/ l Om) 2.0)) (- U* U))))))
(if (<= t_1 0.0)
(sqrt
(*
2.0
(*
n
(*
U
(+
t
(+ (* (/ n Om) (/ (* l (* l U*)) Om)) (* -2.0 (/ l (/ Om l)))))))))
(if (<= t_1 1e+297)
(sqrt t_1)
(-
(* (/ (sqrt 2.0) (fabs (/ Om (* n l)))) (sqrt (* U (- U* U))))
(* (sqrt 2.0) (* l (sqrt (/ U (- U* U))))))))))
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (/.f64 l (/.f64 Om l))) (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) Om))) (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 7 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite=> sub-neg_binary64 (+.f64 t (neg.f64 (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))))): 0 points increase in error, 1 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite<= sub-neg_binary64 (-.f64 t (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite<= associate--l-_binary64 (-.f64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 1 points increase in error, 1 points decrease in error
(sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 1 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 l (/.f64 Om l))) (*.f64 (/.f64 (*.f64 (*.f64 n l) l) Om) (/.f64 U* Om)))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) Om))) (*.f64 (/.f64 (*.f64 (*.f64 n l) l) Om) (/.f64 U* Om)))) (*.f64 n U)))): 5 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) Om)) (*.f64 (/.f64 (*.f64 (*.f64 n l) l) Om) (/.f64 U* Om)))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (*.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 n (*.f64 l l))) Om) (/.f64 U* Om)))) (*.f64 n U)))): 0 points increase in error, 1 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (*.f64 (/.f64 (*.f64 n (Rewrite<= unpow2_binary64 (pow.f64 l 2))) Om) (/.f64 U* Om)))) (*.f64 n U)))): 1 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 n (pow.f64 l 2)) U*) (*.f64 Om Om))))) (*.f64 n U)))): 0 points increase in error, 12 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 n (*.f64 (pow.f64 l 2) U*))) (*.f64 Om Om)))) (*.f64 n U)))): 12 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (-.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (Rewrite<= unpow2_binary64 (pow.f64 Om 2))))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (neg.f64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)))))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (+.f64 (*.f64 2 (/.f64 (pow.f64 l 2) Om)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)))))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om))))) (*.f64 n U)))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 (-.f64 t (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om)))) (Rewrite=> *-commutative_binary64 (*.f64 U n))))): 0 points increase in error, 14 points decrease in error
(sqrt.f64 (*.f64 2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 t (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om)))) U) n)))): 14 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 n (*.f64 (-.f64 t (+.f64 (*.f64 -1 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om)))) U))))): 0 points increase in error, 14 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (*.f64 (/.f64 n Om) (/.f64 (*.f64 l (*.f64 l U*)) Om)) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (*.f64 (/.f64 n Om) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 l l) U*)) Om)) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 2 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 n (*.f64 (*.f64 l l) U*)) (*.f64 Om Om))) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (Rewrite=> associate-/l*_binary64 (/.f64 n (/.f64 (*.f64 Om Om) (*.f64 (*.f64 l l) U*)))) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 1 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (/.f64 n (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 Om 2)) (*.f64 (*.f64 l l) U*))) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 1 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (/.f64 n (/.f64 (pow.f64 Om 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) U*))) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 -2 (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)) (*.f64 (Rewrite<= metadata-eval (neg.f64 2)) (/.f64 l (/.f64 Om l))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)) (*.f64 (neg.f64 2) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) Om))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (+.f64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)) (*.f64 (neg.f64 2) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 l 2)) Om)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (+.f64 t (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2)) (*.f64 2 (/.f64 (pow.f64 l 2) Om))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (*.f64 U (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om)))))))): 0 points increase in error, 13 points decrease in error
(sqrt.f64 (*.f64 2 (*.f64 n (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (+.f64 t (/.f64 (*.f64 n (*.f64 (pow.f64 l 2) U*)) (pow.f64 Om 2))) (*.f64 2 (/.f64 (pow.f64 l 2) Om))) U))))): 13 points increase in error, 0 points decrease in error
if 0.0 < (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))) < 1e297
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (/.f64 l (/.f64 Om l))) (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 l l) Om))) (*.f64 n (*.f64 (pow.f64 (/.f64 l Om) 2) (-.f64 U U*)))))))): 7 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (-.f64 t (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite=> sub-neg_binary64 (+.f64 t (neg.f64 (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))))): 0 points increase in error, 1 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite<= sub-neg_binary64 (-.f64 t (+.f64 (*.f64 2 (/.f64 (*.f64 l l) Om)) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 2 n) (*.f64 U (Rewrite<= associate--l-_binary64 (-.f64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*))))))): 1 points increase in error, 1 points decrease in error
(sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 2 n) U) (-.f64 (-.f64 t (*.f64 2 (/.f64 (*.f64 l l) Om))) (*.f64 (*.f64 n (pow.f64 (/.f64 l Om) 2)) (-.f64 U U*)))))): 1 points increase in error, 0 points decrease in error
herbie shell --seed 2022343
(FPCore (n U t l Om U*)
:name "Toniolo and Linder, Equation (13)"
:precision binary64
(sqrt (* (* (* 2.0 n) U) (- (- t (* 2.0 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2.0)) (- U U*))))))