Average Error: 1.0 → 0.0
Time: 19.9s
Precision: 64
\[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\]
\[\left(1 + v \cdot v\right) \cdot \frac{\frac{\frac{4}{3}}{\pi}}{\sqrt{2 - \left(v \cdot v\right) \cdot 6} \cdot \left(1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}\]
\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}
\left(1 + v \cdot v\right) \cdot \frac{\frac{\frac{4}{3}}{\pi}}{\sqrt{2 - \left(v \cdot v\right) \cdot 6} \cdot \left(1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}
double f(double v) {
        double r5733001 = 4.0;
        double r5733002 = 3.0;
        double r5733003 = atan2(1.0, 0.0);
        double r5733004 = r5733002 * r5733003;
        double r5733005 = 1.0;
        double r5733006 = v;
        double r5733007 = r5733006 * r5733006;
        double r5733008 = r5733005 - r5733007;
        double r5733009 = r5733004 * r5733008;
        double r5733010 = 2.0;
        double r5733011 = 6.0;
        double r5733012 = r5733011 * r5733007;
        double r5733013 = r5733010 - r5733012;
        double r5733014 = sqrt(r5733013);
        double r5733015 = r5733009 * r5733014;
        double r5733016 = r5733001 / r5733015;
        return r5733016;
}

double f(double v) {
        double r5733017 = 1.0;
        double r5733018 = v;
        double r5733019 = r5733018 * r5733018;
        double r5733020 = r5733017 + r5733019;
        double r5733021 = 1.3333333333333333;
        double r5733022 = atan2(1.0, 0.0);
        double r5733023 = r5733021 / r5733022;
        double r5733024 = 2.0;
        double r5733025 = 6.0;
        double r5733026 = r5733019 * r5733025;
        double r5733027 = r5733024 - r5733026;
        double r5733028 = sqrt(r5733027);
        double r5733029 = r5733019 * r5733019;
        double r5733030 = r5733017 - r5733029;
        double r5733031 = r5733028 * r5733030;
        double r5733032 = r5733023 / r5733031;
        double r5733033 = r5733020 * r5733032;
        return r5733033;
}

Error

Bits error versus v

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 1.0

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

    \[\leadsto \frac{4}{\left(\left(3 \cdot \pi\right) \cdot \color{blue}{\frac{1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)}{1 + v \cdot v}}\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\]
  4. Applied associate-*r/1.0

    \[\leadsto \frac{4}{\color{blue}{\frac{\left(3 \cdot \pi\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}{1 + v \cdot v}} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}\]
  5. Applied associate-*l/1.0

    \[\leadsto \frac{4}{\color{blue}{\frac{\left(\left(3 \cdot \pi\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}{1 + v \cdot v}}}\]
  6. Applied associate-/r/1.0

    \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 \cdot 1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \cdot \left(1 + v \cdot v\right)}\]
  7. Simplified0.0

    \[\leadsto \color{blue}{\frac{\frac{\frac{4}{3}}{\pi}}{\sqrt{2 - \left(v \cdot v\right) \cdot 6} \cdot \left(1 - \left(v \cdot v\right) \cdot \left(v \cdot v\right)\right)}} \cdot \left(1 + v \cdot v\right)\]
  8. Final simplification0.0

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

Reproduce

herbie shell --seed 2019132 
(FPCore (v)
  :name "Falkner and Boettcher, Equation (22+)"
  (/ 4 (* (* (* 3 PI) (- 1 (* v v))) (sqrt (- 2 (* 6 (* v v)))))))