Average Error: 0.0 → 0.0
Time: 17.0s
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)\]
↓
\[\frac{\left(\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 \cdot 1 - {v}^{4}}}{4 \cdot \sqrt{1 + v \cdot v}} \cdot \sqrt{1 - v \cdot v}\]
\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)
↓
\frac{\left(\sqrt{2} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 \cdot 1 - {v}^{4}}}{4 \cdot \sqrt{1 + v \cdot v}} \cdot \sqrt{1 - v \cdot v}
double f(double v) {
        double r234625 = 2.0;
        double r234626 = sqrt(r234625);
        double r234627 = 4.0;
        double r234628 = r234626 / r234627;
        double r234629 = 1.0;
        double r234630 = 3.0;
        double r234631 = v;
        double r234632 = r234631 * r234631;
        double r234633 = r234630 * r234632;
        double r234634 = r234629 - r234633;
        double r234635 = sqrt(r234634);
        double r234636 = r234628 * r234635;
        double r234637 = r234629 - r234632;
        double r234638 = r234636 * r234637;
        return r234638;
}
↓
double f(double v) {
        double r234639 = 2.0;
        double r234640 = sqrt(r234639);
        double r234641 = 1.0;
        double r234642 = 3.0;
        double r234643 = v;
        double r234644 = r234643 * r234643;
        double r234645 = r234642 * r234644;
        double r234646 = r234641 - r234645;
        double r234647 = sqrt(r234646);
        double r234648 = r234640 * r234647;
        double r234649 = r234641 * r234641;
        double r234650 = 4.0;
        double r234651 = pow(r234643, r234650);
        double r234652 = r234649 - r234651;
        double r234653 = sqrt(r234652);
        double r234654 = r234648 * r234653;
        double r234655 = 4.0;
        double r234656 = r234641 + r234644;
        double r234657 = sqrt(r234656);
        double r234658 = r234655 * r234657;
        double r234659 = r234654 / r234658;
        double r234660 = r234641 - r234644;
        double r234661 = sqrt(r234660);
        double r234662 = r234659 * r234661;
        return r234662;
}

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 add-sqr-sqrt0.0

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

  4. Applied associate-*r*0.0

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

  6. Applied flip--0.0

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

  7. Applied sqrt-div0.0

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

  8. Applied associate-*l/0.0

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

  9. Applied frac-times0.0

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

  10. Simplified0.0

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

  11. Final simplification0.0

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

Reproduce

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