Average Error: 0.0 → 0.0
Time: 3.4s
Precision: 64
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
↓
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(-v \cdot v\right)\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(-v \cdot v\right)
double f(double v) {
        double r324642 = 2.0;
        double r324643 = sqrt(r324642);
        double r324644 = 4.0;
        double r324645 = r324643 / r324644;
        double r324646 = 1.0;
        double r324647 = 3.0;
        double r324648 = v;
        double r324649 = r324648 * r324648;
        double r324650 = r324647 * r324649;
        double r324651 = r324646 - r324650;
        double r324652 = sqrt(r324651);
        double r324653 = r324645 * r324652;
        double r324654 = r324646 - r324649;
        double r324655 = r324653 * r324654;
        return r324655;
}
↓
double f(double v) {
        double r324656 = 2.0;
        double r324657 = sqrt(r324656);
        double r324658 = 4.0;
        double r324659 = r324657 / r324658;
        double r324660 = 1.0;
        double r324661 = 3.0;
        double r324662 = v;
        double r324663 = r324662 * r324662;
        double r324664 = r324661 * r324663;
        double r324665 = r324660 - r324664;
        double r324666 = sqrt(r324665);
        double r324667 = r324659 * r324666;
        double r324668 = r324667 * r324660;
        double r324669 = -r324663;
        double r324670 = r324667 * r324669;
        double r324671 = r324668 + r324670;
        return r324671;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.0

    \[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
  2. Using strategy rm

  3. Applied sub-neg0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \color{blue}{\left(1 + \left(-v \cdot v\right)\right)}\]

  4. Applied distribute-lft-in0.0

    \[\leadsto \color{blue}{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(-v \cdot v\right)}\]

  5. Final simplification0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot 1 + \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(-v \cdot v\right)\]

Reproduce

herbie shell --seed 2019346 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))