Average Error: 0.5 → 0.1
Time: 1.6m
Precision: 64
\[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
↓
\[\frac{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\sqrt{\left(v \cdot v\right) \cdot -6 + 2}}}{\pi}}{t} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}\]
double f(double v, double t) {
        double r40792792 = 1.0;
        double r40792793 = 5.0;
        double r40792794 = v;
        double r40792795 = r40792794 * r40792794;
        double r40792796 = r40792793 * r40792795;
        double r40792797 = r40792792 - r40792796;
        double r40792798 = atan2(1.0, 0.0);
        double r40792799 = t;
        double r40792800 = r40792798 * r40792799;
        double r40792801 = 2.0;
        double r40792802 = 3.0;
        double r40792803 = r40792802 * r40792795;
        double r40792804 = r40792792 - r40792803;
        double r40792805 = r40792801 * r40792804;
        double r40792806 = sqrt(r40792805);
        double r40792807 = r40792800 * r40792806;
        double r40792808 = r40792792 - r40792795;
        double r40792809 = r40792807 * r40792808;
        double r40792810 = r40792797 / r40792809;
        return r40792810;
}
↓
double f(double v, double t) {
        double r40792811 = 1.0;
        double r40792812 = v;
        double r40792813 = r40792812 * r40792812;
        double r40792814 = 5.0;
        double r40792815 = r40792813 * r40792814;
        double r40792816 = r40792811 - r40792815;
        double r40792817 = sqrt(r40792816);
        double r40792818 = -6.0;
        double r40792819 = r40792813 * r40792818;
        double r40792820 = 2.0;
        double r40792821 = r40792819 + r40792820;
        double r40792822 = sqrt(r40792821);
        double r40792823 = r40792817 / r40792822;
        double r40792824 = atan2(1.0, 0.0);
        double r40792825 = r40792823 / r40792824;
        double r40792826 = t;
        double r40792827 = r40792825 / r40792826;
        double r40792828 = r40792811 - r40792813;
        double r40792829 = r40792817 / r40792828;
        double r40792830 = r40792827 * r40792829;
        return r40792830;
}


\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}
↓
\frac{\frac{\frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{\sqrt{\left(v \cdot v\right) \cdot -6 + 2}}}{\pi}}{t} \cdot \frac{\sqrt{1 - \left(v \cdot v\right) \cdot 5}}{1 - v \cdot v}

Error

Bits error versus v

Bits error versus t

Derivation

  1. Initial program 0.5

    \[\frac{1 - 5 \cdot \left(v \cdot v\right)}{\left(\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}\right) \cdot \left(1 - v \cdot v\right)}\]
  2. Using strategy rm

  3. Applied add-sqr-sqrt0.5

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

  4. Applied times-frac0.5

    \[\leadsto \color{blue}{\frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{\left(\pi \cdot t\right) \cdot \sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{1 - v \cdot v}}\]
  5. Using strategy rm

  6. Applied *-un-lft-identity0.5

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

  7. Applied sqrt-prod0.5

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

  8. Applied times-frac0.6

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

  9. Simplified0.3

    \[\leadsto \left(\color{blue}{\frac{\frac{1}{\pi}}{t}} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{\sqrt{2 \cdot \left(1 - 3 \cdot \left(v \cdot v\right)\right)}}\right) \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{1 - v \cdot v}\]
  10. Using strategy rm

  11. Applied associate-*l/0.2

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

  12. Simplified0.1

    \[\leadsto \frac{\color{blue}{\frac{\frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{\sqrt{\left(v \cdot v\right) \cdot -6 + 2}}}{\pi}}}{t} \cdot \frac{\sqrt{1 - 5 \cdot \left(v \cdot v\right)}}{1 - v \cdot v}\]

  13. Final simplification0.1

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

Reproduce

herbie shell --seed 2019101 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  (/ (- 1 (* 5 (* v v))) (* (* (* PI t) (sqrt (* 2 (- 1 (* 3 (* v v)))))) (- 1 (* v v)))))