Average Error: 0.0 → 0.0
Time: 19.1s
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(\left(\frac{\sqrt{2}}{4} \cdot \sqrt{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right) \cdot \sqrt{\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 \left(1 - v \cdot v\right)
↓
\left(\left(\frac{\sqrt{2}}{4} \cdot \sqrt{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right) \cdot \sqrt{\sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right) \cdot \left(1 - v \cdot v\right)
double f(double v) {
        double r192082 = 2.0;
        double r192083 = sqrt(r192082);
        double r192084 = 4.0;
        double r192085 = r192083 / r192084;
        double r192086 = 1.0;
        double r192087 = 3.0;
        double r192088 = v;
        double r192089 = r192088 * r192088;
        double r192090 = r192087 * r192089;
        double r192091 = r192086 - r192090;
        double r192092 = sqrt(r192091);
        double r192093 = r192085 * r192092;
        double r192094 = r192086 - r192089;
        double r192095 = r192093 * r192094;
        return r192095;
}
↓
double f(double v) {
        double r192096 = 2.0;
        double r192097 = sqrt(r192096);
        double r192098 = 4.0;
        double r192099 = r192097 / r192098;
        double r192100 = 1.0;
        double r192101 = 3.0;
        double r192102 = v;
        double r192103 = r192102 * r192102;
        double r192104 = r192101 * r192103;
        double r192105 = r192100 - r192104;
        double r192106 = sqrt(r192105);
        double r192107 = sqrt(r192106);
        double r192108 = r192099 * r192107;
        double r192109 = r192108 * r192107;
        double r192110 = r192100 - r192103;
        double r192111 = r192109 * r192110;
        return r192111;
}

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

  4. Applied sqrt-prod0.0

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

  5. Applied associate-*r*0.0

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

  6. Final simplification0.0

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

Reproduce

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