(FPCore (w0 M D h l d)
:precision binary64
(* w0 (sqrt (- 1.0 (* (pow (/ (* M D) (* 2.0 d)) 2.0) (/ h l))))))
↓
(FPCore (w0 M D h l d)
:precision binary64
(let* ((t_0 (* D (* 0.5 (/ M d)))))
(if (<= (/ h l) -5e-28)
(* w0 (sqrt (- 1.0 (* h (* t_0 (/ t_0 l))))))
(*
w0
(sqrt
(- 1.0 (/ (* M (/ (* D 0.5) (/ d h))) (* (/ (/ d D) M) (/ l 0.5)))))))))
(*.f64 h (/.f64 (pow.f64 (*.f64 D (/.f64 M (*.f64 2 d))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 M (*.f64 2 d)) D)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 M D) (*.f64 2 d))) 2) l)): 9 points increase in error, 14 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 M D)))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (neg.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 M D)))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 -1) (*.f64 M D))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (*.f64 (Rewrite=> metadata-eval 1) (*.f64 M D)) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (*.f64 2 d)) (*.f64 M D))) 2) l)): 7 points increase in error, 6 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (*.f64 2 d) (*.f64 M D)))) 2) l)): 10 points increase in error, 11 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 1 (Rewrite=> associate-/l*_binary64 (/.f64 2 (/.f64 (*.f64 M D) d)))) 2) l)): 3 points increase in error, 3 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 1 (/.f64 2 (Rewrite<= associate-*r/_binary64 (*.f64 M (/.f64 D d))))) 2) l)): 8 points increase in error, 9 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 2) (*.f64 M (/.f64 D d)))) 2) l)): 1 points increase in error, 3 points decrease in error
(*.f64 h (/.f64 (pow.f64 (*.f64 (Rewrite=> metadata-eval 1/2) (*.f64 M (/.f64 D d))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 M (/.f64 D d)) 1/2)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-*l*_binary64 (*.f64 M (*.f64 (/.f64 D d) 1/2))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (*.f64 M (Rewrite<= *-commutative_binary64 (*.f64 1/2 (/.f64 D d)))) 2) l)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 (*.f64 M (*.f64 1/2 (/.f64 D d))) 2) l) h)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 (*.f64 M (*.f64 1/2 (/.f64 D d))) 2) (/.f64 l h))): 32 points increase in error, 14 points decrease in error
(*.f64 h (/.f64 (pow.f64 (*.f64 D (/.f64 M (*.f64 2 d))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 M (*.f64 2 d)) D)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 M D) (*.f64 2 d))) 2) l)): 9 points increase in error, 14 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 M D)))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (neg.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 M D)))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 -1) (*.f64 M D))) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 (*.f64 (Rewrite=> metadata-eval 1) (*.f64 M D)) (*.f64 2 d)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (*.f64 2 d)) (*.f64 M D))) 2) l)): 7 points increase in error, 6 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (*.f64 2 d) (*.f64 M D)))) 2) l)): 10 points increase in error, 11 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 1 (Rewrite=> associate-/l*_binary64 (/.f64 2 (/.f64 (*.f64 M D) d)))) 2) l)): 3 points increase in error, 3 points decrease in error
(*.f64 h (/.f64 (pow.f64 (/.f64 1 (/.f64 2 (Rewrite<= associate-*r/_binary64 (*.f64 M (/.f64 D d))))) 2) l)): 8 points increase in error, 9 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 2) (*.f64 M (/.f64 D d)))) 2) l)): 1 points increase in error, 3 points decrease in error
(*.f64 h (/.f64 (pow.f64 (*.f64 (Rewrite=> metadata-eval 1/2) (*.f64 M (/.f64 D d))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 M (/.f64 D d)) 1/2)) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (Rewrite=> associate-*l*_binary64 (*.f64 M (*.f64 (/.f64 D d) 1/2))) 2) l)): 0 points increase in error, 0 points decrease in error
(*.f64 h (/.f64 (pow.f64 (*.f64 M (Rewrite<= *-commutative_binary64 (*.f64 1/2 (/.f64 D d)))) 2) l)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 (*.f64 M (*.f64 1/2 (/.f64 D d))) 2) l) h)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 (*.f64 M (*.f64 1/2 (/.f64 D d))) 2) (/.f64 l h))): 32 points increase in error, 14 points decrease in error
(/.f64 (*.f64 M (/.f64 (*.f64 1/2 D) (/.f64 d h))) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 M (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 D 1/2)) (/.f64 d h))) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 M (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D 1/2) h) d))) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 27 points increase in error, 17 points decrease in error
(/.f64 (*.f64 M (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 D (*.f64 1/2 h))) d)) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (*.f64 D (*.f64 1/2 h)) d) M)) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (*.f64 D (*.f64 1/2 h)) M) d)) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 18 points increase in error, 18 points decrease in error
(/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 M (*.f64 D (*.f64 1/2 h)))) d) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h)))) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 19 points increase in error, 17 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1)) (*.f64 (/.f64 (/.f64 d D) M) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1) (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 d (*.f64 D M))) (/.f64 l 1/2))): 14 points increase in error, 15 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1) (*.f64 (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 M D))) (/.f64 l 1/2))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1) (*.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 d M) D)) (/.f64 l 1/2))): 15 points increase in error, 11 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (/.f64 d M) l) (*.f64 D 1/2)))): 16 points increase in error, 14 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) 1) (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 d M) (/.f64 l (*.f64 D 1/2))))): 20 points increase in error, 21 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 (/.f64 M d) (*.f64 D (*.f64 1/2 h))) (/.f64 1 (*.f64 (/.f64 d M) (/.f64 l (*.f64 D 1/2)))))): 4 points increase in error, 5 points decrease in error