Average Error: 0.0 → 0.0
Time: 4.9s
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(\frac{\sqrt{2}}{4} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{\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(\frac{\sqrt{2}}{4} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{\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 r208110 = 2.0;
        double r208111 = sqrt(r208110);
        double r208112 = 4.0;
        double r208113 = r208111 / r208112;
        double r208114 = 1.0;
        double r208115 = 3.0;
        double r208116 = v;
        double r208117 = r208116 * r208116;
        double r208118 = r208115 * r208117;
        double r208119 = r208114 - r208118;
        double r208120 = sqrt(r208119);
        double r208121 = r208113 * r208120;
        double r208122 = r208114 - r208117;
        double r208123 = r208121 * r208122;
        return r208123;
}
↓
double f(double v) {
        double r208124 = 2.0;
        double r208125 = sqrt(r208124);
        double r208126 = 4.0;
        double r208127 = r208125 / r208126;
        double r208128 = 1.0;
        double r208129 = 3.0;
        double r208130 = pow(r208128, r208129);
        double r208131 = 3.0;
        double r208132 = v;
        double r208133 = r208132 * r208132;
        double r208134 = r208131 * r208133;
        double r208135 = pow(r208134, r208129);
        double r208136 = r208130 - r208135;
        double r208137 = sqrt(r208136);
        double r208138 = r208127 * r208137;
        double r208139 = r208128 - r208133;
        double r208140 = r208138 * r208139;
        double r208141 = r208128 * r208128;
        double r208142 = r208134 * r208134;
        double r208143 = r208128 * r208134;
        double r208144 = r208142 + r208143;
        double r208145 = r208141 + r208144;
        double r208146 = sqrt(r208145);
        double r208147 = r208140 / r208146;
        return r208147;
}

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 associate-*r/0.0

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

  6. Applied associate-*l/0.0

    \[\leadsto \color{blue}{\frac{\left(\frac{\sqrt{2}}{4} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{\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(\frac{\sqrt{2}}{4} \cdot \sqrt{{1}^{3} - {\left(3 \cdot \left(v \cdot v\right)\right)}^{3}}\right) \cdot \left(1 - v \cdot v\right)}{\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 2019353 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  :precision binary64
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))