Average Error: 0.0 → 0.0
Time: 17.8s
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} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{4 \cdot \sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\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)
↓
\frac{\left(\sqrt{2} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{4 \cdot \sqrt{1 \cdot 1 + \left(\left(3 \cdot \left(v \cdot v\right)\right) \cdot \left(3 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(3 \cdot \left(v \cdot v\right)\right)\right)}}
double f(double v) {
        double r255186 = 2.0;
        double r255187 = sqrt(r255186);
        double r255188 = 4.0;
        double r255189 = r255187 / r255188;
        double r255190 = 1.0;
        double r255191 = 3.0;
        double r255192 = v;
        double r255193 = r255192 * r255192;
        double r255194 = r255191 * r255193;
        double r255195 = r255190 - r255194;
        double r255196 = sqrt(r255195);
        double r255197 = r255189 * r255196;
        double r255198 = r255190 - r255193;
        double r255199 = r255197 * r255198;
        return r255199;
}
↓
double f(double v) {
        double r255200 = 2.0;
        double r255201 = sqrt(r255200);
        double r255202 = 1.0;
        double r255203 = 3.0;
        double r255204 = pow(r255202, r255203);
        double r255205 = 3.0;
        double r255206 = v;
        double r255207 = r255206 * r255206;
        double r255208 = r255205 * r255207;
        double r255209 = pow(r255208, r255203);
        double r255210 = r255204 - r255209;
        double r255211 = sqrt(r255210);
        double r255212 = r255201 * r255211;
        double r255213 = r255202 - r255207;
        double r255214 = r255212 * r255213;
        double r255215 = 4.0;
        double r255216 = r255202 * r255202;
        double r255217 = r255208 * r255208;
        double r255218 = r255202 * r255208;
        double r255219 = r255217 + r255218;
        double r255220 = r255216 + r255219;
        double r255221 = sqrt(r255220);
        double r255222 = r255215 * r255221;
        double r255223 = r255214 / r255222;
        return r255223;
}

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 flip3--0.0

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

  4. Applied sqrt-div0.0

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

  5. Applied frac-times0.0

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

  6. Applied associate-*l/0.0

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

  7. Final simplification0.0

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

Reproduce

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