Average Error: 0.0 → 0.0
Time: 18.7s
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(\sqrt{1} - v\right) \cdot \left(\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\sqrt{1} + v\right)\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(\sqrt{1} - v\right) \cdot \left(\left(\sqrt{1 - \left(v \cdot v\right) \cdot 3} \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\sqrt{1} + v\right)\right)
double f(double v) {
        double r8318758 = 2.0;
        double r8318759 = sqrt(r8318758);
        double r8318760 = 4.0;
        double r8318761 = r8318759 / r8318760;
        double r8318762 = 1.0;
        double r8318763 = 3.0;
        double r8318764 = v;
        double r8318765 = r8318764 * r8318764;
        double r8318766 = r8318763 * r8318765;
        double r8318767 = r8318762 - r8318766;
        double r8318768 = sqrt(r8318767);
        double r8318769 = r8318761 * r8318768;
        double r8318770 = r8318762 - r8318765;
        double r8318771 = r8318769 * r8318770;
        return r8318771;
}
↓
double f(double v) {
        double r8318772 = 1.0;
        double r8318773 = sqrt(r8318772);
        double r8318774 = v;
        double r8318775 = r8318773 - r8318774;
        double r8318776 = r8318774 * r8318774;
        double r8318777 = 3.0;
        double r8318778 = r8318776 * r8318777;
        double r8318779 = r8318772 - r8318778;
        double r8318780 = sqrt(r8318779);
        double r8318781 = 2.0;
        double r8318782 = sqrt(r8318781);
        double r8318783 = 4.0;
        double r8318784 = r8318782 / r8318783;
        double r8318785 = r8318780 * r8318784;
        double r8318786 = r8318773 + r8318774;
        double r8318787 = r8318785 * r8318786;
        double r8318788 = r8318775 * r8318787;
        return r8318788;
}

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 \left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - v \cdot v\right)\]

  4. Applied difference-of-squares0.0

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

  5. 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 \left(\sqrt{1} + v\right)\right) \cdot \left(\sqrt{1} - v\right)}\]

  6. Final simplification0.0

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

Reproduce

herbie shell --seed 2019172 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2.0) 4.0) (sqrt (- 1.0 (* 3.0 (* v v))))) (- 1.0 (* v v))))