Falkner and Boettcher, Equation (20:1,3)

Percentage Accurate: 99.4% → 99.5%

Time: 4.4s

Alternatives: 4

Speedup: N/A×

Specification

Math

\[\begin{array}{l} \\ \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)} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (/
  (- 1.0 (* 5.0 (* v v)))
  (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))

C

double code(double v, double t) {
	return (1.0 - (5.0 * (v * v))) / (((((double) M_PI) * t) * sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
}

Java

public static double code(double v, double t) {
	return (1.0 - (5.0 * (v * v))) / (((Math.PI * t) * Math.sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
}

Python

def code(v, t):
	return (1.0 - (5.0 * (v * v))) / (((math.pi * t) * math.sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)))

Julia

function code(v, t)
	return Float64(Float64(1.0 - Float64(5.0 * Float64(v * v))) / Float64(Float64(Float64(pi * t) * sqrt(Float64(2.0 * Float64(1.0 - Float64(3.0 * Float64(v * v)))))) * Float64(1.0 - Float64(v * v))))
end

MATLAB

function tmp = code(v, t)
	tmp = (1.0 - (5.0 * (v * v))) / (((pi * t) * sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
end

Wolfram

code[v_, t_] := N[(N[(1.0 - N[(5.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(N[(Pi * t), $MachinePrecision] * N[Sqrt[N[(2.0 * N[(1.0 - N[(3.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Initial Program: 99.4% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \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)} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (/
  (- 1.0 (* 5.0 (* v v)))
  (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))

C

double code(double v, double t) {
	return (1.0 - (5.0 * (v * v))) / (((((double) M_PI) * t) * sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
}

Java

public static double code(double v, double t) {
	return (1.0 - (5.0 * (v * v))) / (((Math.PI * t) * Math.sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
}

Python

def code(v, t):
	return (1.0 - (5.0 * (v * v))) / (((math.pi * t) * math.sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)))

Julia

function code(v, t)
	return Float64(Float64(1.0 - Float64(5.0 * Float64(v * v))) / Float64(Float64(Float64(pi * t) * sqrt(Float64(2.0 * Float64(1.0 - Float64(3.0 * Float64(v * v)))))) * Float64(1.0 - Float64(v * v))))
end

MATLAB

function tmp = code(v, t)
	tmp = (1.0 - (5.0 * (v * v))) / (((pi * t) * sqrt((2.0 * (1.0 - (3.0 * (v * v)))))) * (1.0 - (v * v)));
end

Wolfram

code[v_, t_] := N[(N[(1.0 - N[(5.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(N[(Pi * t), $MachinePrecision] * N[Sqrt[N[(2.0 * N[(1.0 - N[(3.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Alternative 1: 99.5% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{0.5} \cdot \left(\left({2}^{0.5} \cdot \pi\right) \cdot t\right)\right) \cdot \left(1 - v \cdot v\right)} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (/
  (- 1.0 (* 5.0 (* v v)))
  (*
   (* (pow (fma -3.0 (* v v) 1.0) 0.5) (* (* (pow 2.0 0.5) PI) t))
   (- 1.0 (* v v)))))

C

double code(double v, double t) {
	return (1.0 - (5.0 * (v * v))) / ((pow(fma(-3.0, (v * v), 1.0), 0.5) * ((pow(2.0, 0.5) * ((double) M_PI)) * t)) * (1.0 - (v * v)));
}

Julia

function code(v, t)
	return Float64(Float64(1.0 - Float64(5.0 * Float64(v * v))) / Float64(Float64((fma(-3.0, Float64(v * v), 1.0) ^ 0.5) * Float64(Float64((2.0 ^ 0.5) * pi) * t)) * Float64(1.0 - Float64(v * v))))
end

Wolfram

code[v_, t_] := N[(N[(1.0 - N[(5.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(N[Power[N[(-3.0 * N[(v * v), $MachinePrecision] + 1.0), $MachinePrecision], 0.5], $MachinePrecision] * N[(N[(N[Power[2.0, 0.5], $MachinePrecision] * Pi), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 99.3%

   \[\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. Add Preprocessing

3. Taylor expanded in t around 0

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\left(\left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right) \cdot \sqrt{1 - 3 \cdot {v}^{2}}\right)} \cdot \left(1 - v \cdot v\right)} \]
4. Step-by-step derivation

   1. *-commutative N/A

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

   2. lower-*.f64 N/A

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

   3. pow1/2 N/A

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

   4. pow2 N/A

      \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(1 - 3 \cdot \left(v \cdot v\right)\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   5. lower-pow.f64 N/A

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

   6. pow2 N/A

      \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(1 - 3 \cdot {v}^{2}\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   7. fp-cancel-sub-sign-inv N/A

      \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(1 + \left(\mathsf{neg}\left(3\right)\right) \cdot {v}^{2}\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   8. metadata-eval N/A

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

   9. +-commutative N/A

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

   10. lower-fma.f64 N/A

       \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, {v}^{2}, 1\right)\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   11. pow2 N/A

       \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   12. lift-*.f64 N/A

       \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{\frac{1}{2}} \cdot \left(t \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right)\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   13. *-commutative N/A

       \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{\frac{1}{2}} \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right) \cdot \color{blue}{t}\right)\right) \cdot \left(1 - v \cdot v\right)} \]

   14. lower-*.f64 N/A

       \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{\frac{1}{2}} \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \sqrt{2}\right) \cdot \color{blue}{t}\right)\right) \cdot \left(1 - v \cdot v\right)} \]

5. Applied rewrites 99.5%

   \[\leadsto \frac{1 - 5 \cdot \left(v \cdot v\right)}{\color{blue}{\left({\left(\mathsf{fma}\left(-3, v \cdot v, 1\right)\right)}^{0.5} \cdot \left(\left({2}^{0.5} \cdot \pi\right) \cdot t\right)\right)} \cdot \left(1 - v \cdot v\right)} \]
6. Add Preprocessing

Alternative 2: 99.5% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \frac{\frac{\mathsf{fma}\left({v}^{6}, -125, 1\right)}{t}}{\left({2}^{0.5} \cdot \pi\right) \cdot \left(\left(\mathsf{fma}\left(v \cdot 5, v, {v}^{4} \cdot 25\right) + 1\right) \cdot \frac{1 - {v}^{4}}{1 + v \cdot v}\right)} \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (*
  (/
   (/ (fma (pow v 6.0) -125.0 1.0) t)
   (*
    (* (pow 2.0 0.5) PI)
    (*
     (+ (fma (* v 5.0) v (* (pow v 4.0) 25.0)) 1.0)
     (/ (- 1.0 (pow v 4.0)) (+ 1.0 (* v v))))))
  (pow (pow (fma (* v v) -3.0 1.0) -1.0) 0.5)))

C

double code(double v, double t) {
	return ((fma(pow(v, 6.0), -125.0, 1.0) / t) / ((pow(2.0, 0.5) * ((double) M_PI)) * ((fma((v * 5.0), v, (pow(v, 4.0) * 25.0)) + 1.0) * ((1.0 - pow(v, 4.0)) / (1.0 + (v * v)))))) * pow(pow(fma((v * v), -3.0, 1.0), -1.0), 0.5);
}

Julia

function code(v, t)
	return Float64(Float64(Float64(fma((v ^ 6.0), -125.0, 1.0) / t) / Float64(Float64((2.0 ^ 0.5) * pi) * Float64(Float64(fma(Float64(v * 5.0), v, Float64((v ^ 4.0) * 25.0)) + 1.0) * Float64(Float64(1.0 - (v ^ 4.0)) / Float64(1.0 + Float64(v * v)))))) * ((fma(Float64(v * v), -3.0, 1.0) ^ -1.0) ^ 0.5))
end

Wolfram

code[v_, t_] := N[(N[(N[(N[(N[Power[v, 6.0], $MachinePrecision] * -125.0 + 1.0), $MachinePrecision] / t), $MachinePrecision] / N[(N[(N[Power[2.0, 0.5], $MachinePrecision] * Pi), $MachinePrecision] * N[(N[(N[(N[(v * 5.0), $MachinePrecision] * v + N[(N[Power[v, 4.0], $MachinePrecision] * 25.0), $MachinePrecision]), $MachinePrecision] + 1.0), $MachinePrecision] * N[(N[(1.0 - N[Power[v, 4.0], $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Power[N[Power[N[(N[(v * v), $MachinePrecision] * -3.0 + 1.0), $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 99.3%

   \[\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. Add Preprocessing
3. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \frac{\color{blue}{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. flip3-- N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   3. lower-/.f64 N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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. metadata-eval N/A

      \[\leadsto \frac{\frac{\color{blue}{1} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   5. lower--.f64 N/A

      \[\leadsto \frac{\frac{\color{blue}{1 - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   6. lower-pow.f64 N/A

      \[\leadsto \frac{\frac{1 - \color{blue}{{\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   7. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(5 \cdot \left(v \cdot v\right)\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   8. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\left(5 \cdot \color{blue}{\left(v \cdot v\right)}\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   9. associate-*r* N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   10. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   11. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\color{blue}{\left(5 \cdot v\right)} \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   12. metadata-eval N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1} + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   13. lower-+.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   14. lower-fma.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \color{blue}{\mathsf{fma}\left(5 \cdot \left(v \cdot v\right), 5 \cdot \left(v \cdot v\right), 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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 rewrites 99.3%

   \[\leadsto \frac{\color{blue}{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \mathsf{fma}\left(\left(5 \cdot v\right) \cdot v, \left(5 \cdot v\right) \cdot v, 1 \cdot \left(\left(5 \cdot v\right) \cdot v\right)\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)} \]

5. Taylor expanded in t around 0

   \[\leadsto \color{blue}{\frac{1 - 125 \cdot {v}^{6}}{t \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\sqrt{2} \cdot \left(\left(1 + \left(5 \cdot {v}^{2} + 25 \cdot {v}^{4}\right)\right) \cdot \left(1 - {v}^{2}\right)\right)\right)\right)} \cdot \sqrt{\frac{1}{1 - 3 \cdot {v}^{2}}}} \]

7. Applied rewrites 99.4%

   \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left({v}^{6}, -125, 1\right)}{t}}{\left({2}^{0.5} \cdot \pi\right) \cdot \left(\left(\mathsf{fma}\left(v \cdot 5, v, {v}^{4} \cdot 25\right) + 1\right) \cdot \frac{1 - {v}^{4}}{1 + v \cdot v}\right)} \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5}} \]
8. Add Preprocessing

Alternative 3: 99.3% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := {\left({4}^{0.125}\right)}^{2} \cdot \pi\\ t_2 := {\left(t\_1 \cdot t\right)}^{-1}\\ \mathsf{fma}\left({t\_1}^{-1}, {t}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(t\_2, -4, \frac{-4 \cdot \frac{v \cdot v}{t}}{t\_1}\right), v \cdot v, t\_2 \cdot -4\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5} \end{array} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (let* ((t_1 (* (pow (pow 4.0 0.125) 2.0) PI)) (t_2 (pow (* t_1 t) -1.0)))
   (*
    (fma
     (pow t_1 -1.0)
     (pow t -1.0)
     (*
      (fma (fma t_2 -4.0 (/ (* -4.0 (/ (* v v) t)) t_1)) (* v v) (* t_2 -4.0))
      (* v v)))
    (pow (pow (fma (* v v) -3.0 1.0) -1.0) 0.5))))

C

double code(double v, double t) {
	double t_1 = pow(pow(4.0, 0.125), 2.0) * ((double) M_PI);
	double t_2 = pow((t_1 * t), -1.0);
	return fma(pow(t_1, -1.0), pow(t, -1.0), (fma(fma(t_2, -4.0, ((-4.0 * ((v * v) / t)) / t_1)), (v * v), (t_2 * -4.0)) * (v * v))) * pow(pow(fma((v * v), -3.0, 1.0), -1.0), 0.5);
}

Julia

function code(v, t)
	t_1 = Float64(((4.0 ^ 0.125) ^ 2.0) * pi)
	t_2 = Float64(t_1 * t) ^ -1.0
	return Float64(fma((t_1 ^ -1.0), (t ^ -1.0), Float64(fma(fma(t_2, -4.0, Float64(Float64(-4.0 * Float64(Float64(v * v) / t)) / t_1)), Float64(v * v), Float64(t_2 * -4.0)) * Float64(v * v))) * ((fma(Float64(v * v), -3.0, 1.0) ^ -1.0) ^ 0.5))
end

Wolfram

code[v_, t_] := Block[{t$95$1 = N[(N[Power[N[Power[4.0, 0.125], $MachinePrecision], 2.0], $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$2 = N[Power[N[(t$95$1 * t), $MachinePrecision], -1.0], $MachinePrecision]}, N[(N[(N[Power[t$95$1, -1.0], $MachinePrecision] * N[Power[t, -1.0], $MachinePrecision] + N[(N[(N[(t$95$2 * -4.0 + N[(N[(-4.0 * N[(N[(v * v), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision] / t$95$1), $MachinePrecision]), $MachinePrecision] * N[(v * v), $MachinePrecision] + N[(t$95$2 * -4.0), $MachinePrecision]), $MachinePrecision] * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Power[N[Power[N[(N[(v * v), $MachinePrecision] * -3.0 + 1.0), $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Initial program 99.3%

   \[\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. Add Preprocessing
3. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \frac{\color{blue}{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. flip3-- N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   3. lower-/.f64 N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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. metadata-eval N/A

      \[\leadsto \frac{\frac{\color{blue}{1} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   5. lower--.f64 N/A

      \[\leadsto \frac{\frac{\color{blue}{1 - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   6. lower-pow.f64 N/A

      \[\leadsto \frac{\frac{1 - \color{blue}{{\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   7. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(5 \cdot \left(v \cdot v\right)\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   8. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\left(5 \cdot \color{blue}{\left(v \cdot v\right)}\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   9. associate-*r* N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   10. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   11. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\color{blue}{\left(5 \cdot v\right)} \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   12. metadata-eval N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1} + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   13. lower-+.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   14. lower-fma.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \color{blue}{\mathsf{fma}\left(5 \cdot \left(v \cdot v\right), 5 \cdot \left(v \cdot v\right), 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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 rewrites 99.3%

   \[\leadsto \frac{\color{blue}{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \mathsf{fma}\left(\left(5 \cdot v\right) \cdot v, \left(5 \cdot v\right) \cdot v, 1 \cdot \left(\left(5 \cdot v\right) \cdot v\right)\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)} \]

5. Taylor expanded in t around 0

   \[\leadsto \color{blue}{\frac{1 - 125 \cdot {v}^{6}}{t \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\sqrt{2} \cdot \left(\left(1 + \left(5 \cdot {v}^{2} + 25 \cdot {v}^{4}\right)\right) \cdot \left(1 - {v}^{2}\right)\right)\right)\right)} \cdot \sqrt{\frac{1}{1 - 3 \cdot {v}^{2}}}} \]

7. Applied rewrites 99.4%

   \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left({v}^{6}, -125, 1\right)}{t}}{\left({2}^{0.5} \cdot \pi\right) \cdot \left(\left(\mathsf{fma}\left(v \cdot 5, v, {v}^{4} \cdot 25\right) + 1\right) \cdot \frac{1 - {v}^{4}}{1 + v \cdot v}\right)} \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5}} \]

8. Taylor expanded in v around 0

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

10. Applied rewrites 98.6%

    \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({\left({4}^{0.125}\right)}^{2}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{0.125}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\color{blue}{\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}}^{0.5} \]

12. Applied rewrites 99.1%

    \[\leadsto \mathsf{fma}\left({\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right)}^{-1}, {t}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left({\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}, -4, \frac{-4 \cdot \frac{v \cdot v}{t}}{{\left({4}^{0.125}\right)}^{2} \cdot \pi}\right), v \cdot v, {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1} \cdot -4\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{\color{blue}{-1}}\right)}^{0.5} \]
13. Add Preprocessing

Alternative 4: 99.0% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := {\left({4}^{0.125}\right)}^{2} \cdot \pi\\ t_2 := -4 \cdot {\left(t\_1 \cdot t\right)}^{-1}\\ \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({4}^{0.25}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{t\_1}, t\_2\right), v \cdot v, t\_2\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5} \end{array} \end{array} \]

FPCore

(FPCore (v t)
 :precision binary64
 (let* ((t_1 (* (pow (pow 4.0 0.125) 2.0) PI))
        (t_2 (* -4.0 (pow (* t_1 t) -1.0))))
   (*
    (fma
     (pow (* t PI) -1.0)
     (pow (pow 4.0 0.25) -1.0)
     (* (fma (fma -4.0 (/ (/ (* v v) t) t_1) t_2) (* v v) t_2) (* v v)))
    (pow (pow (fma (* v v) -3.0 1.0) -1.0) 0.5))))

C

double code(double v, double t) {
	double t_1 = pow(pow(4.0, 0.125), 2.0) * ((double) M_PI);
	double t_2 = -4.0 * pow((t_1 * t), -1.0);
	return fma(pow((t * ((double) M_PI)), -1.0), pow(pow(4.0, 0.25), -1.0), (fma(fma(-4.0, (((v * v) / t) / t_1), t_2), (v * v), t_2) * (v * v))) * pow(pow(fma((v * v), -3.0, 1.0), -1.0), 0.5);
}

Julia

function code(v, t)
	t_1 = Float64(((4.0 ^ 0.125) ^ 2.0) * pi)
	t_2 = Float64(-4.0 * (Float64(t_1 * t) ^ -1.0))
	return Float64(fma((Float64(t * pi) ^ -1.0), ((4.0 ^ 0.25) ^ -1.0), Float64(fma(fma(-4.0, Float64(Float64(Float64(v * v) / t) / t_1), t_2), Float64(v * v), t_2) * Float64(v * v))) * ((fma(Float64(v * v), -3.0, 1.0) ^ -1.0) ^ 0.5))
end

Wolfram

code[v_, t_] := Block[{t$95$1 = N[(N[Power[N[Power[4.0, 0.125], $MachinePrecision], 2.0], $MachinePrecision] * Pi), $MachinePrecision]}, Block[{t$95$2 = N[(-4.0 * N[Power[N[(t$95$1 * t), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[Power[N[(t * Pi), $MachinePrecision], -1.0], $MachinePrecision] * N[Power[N[Power[4.0, 0.25], $MachinePrecision], -1.0], $MachinePrecision] + N[(N[(N[(-4.0 * N[(N[(N[(v * v), $MachinePrecision] / t), $MachinePrecision] / t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision] * N[(v * v), $MachinePrecision] + t$95$2), $MachinePrecision] * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Power[N[Power[N[(N[(v * v), $MachinePrecision] * -3.0 + 1.0), $MachinePrecision], -1.0], $MachinePrecision], 0.5], $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Initial program 99.3%

   \[\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. Add Preprocessing
3. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \frac{\color{blue}{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. flip3-- N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   3. lower-/.f64 N/A

      \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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. metadata-eval N/A

      \[\leadsto \frac{\frac{\color{blue}{1} - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   5. lower--.f64 N/A

      \[\leadsto \frac{\frac{\color{blue}{1 - {\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   6. lower-pow.f64 N/A

      \[\leadsto \frac{\frac{1 - \color{blue}{{\left(5 \cdot \left(v \cdot v\right)\right)}^{3}}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   7. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(5 \cdot \left(v \cdot v\right)\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   8. lift-*.f64 N/A

      \[\leadsto \frac{\frac{1 - {\left(5 \cdot \color{blue}{\left(v \cdot v\right)}\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   9. associate-*r* N/A

      \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   10. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\color{blue}{\left(\left(5 \cdot v\right) \cdot v\right)}}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   11. lower-*.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\color{blue}{\left(5 \cdot v\right)} \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   12. metadata-eval N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1} + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   13. lower-+.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{\color{blue}{1 + \left(\left(5 \cdot \left(v \cdot v\right)\right) \cdot \left(5 \cdot \left(v \cdot v\right)\right) + 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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)} \]

   14. lower-fma.f64 N/A

       \[\leadsto \frac{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \color{blue}{\mathsf{fma}\left(5 \cdot \left(v \cdot v\right), 5 \cdot \left(v \cdot v\right), 1 \cdot \left(5 \cdot \left(v \cdot v\right)\right)\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 rewrites 99.3%

   \[\leadsto \frac{\color{blue}{\frac{1 - {\left(\left(5 \cdot v\right) \cdot v\right)}^{3}}{1 + \mathsf{fma}\left(\left(5 \cdot v\right) \cdot v, \left(5 \cdot v\right) \cdot v, 1 \cdot \left(\left(5 \cdot v\right) \cdot v\right)\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)} \]

5. Taylor expanded in t around 0

   \[\leadsto \color{blue}{\frac{1 - 125 \cdot {v}^{6}}{t \cdot \left(\mathsf{PI}\left(\right) \cdot \left(\sqrt{2} \cdot \left(\left(1 + \left(5 \cdot {v}^{2} + 25 \cdot {v}^{4}\right)\right) \cdot \left(1 - {v}^{2}\right)\right)\right)\right)} \cdot \sqrt{\frac{1}{1 - 3 \cdot {v}^{2}}}} \]

7. Applied rewrites 99.4%

   \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left({v}^{6}, -125, 1\right)}{t}}{\left({2}^{0.5} \cdot \pi\right) \cdot \left(\left(\mathsf{fma}\left(v \cdot 5, v, {v}^{4} \cdot 25\right) + 1\right) \cdot \frac{1 - {v}^{4}}{1 + v \cdot v}\right)} \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5}} \]

8. Taylor expanded in v around 0

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

10. Applied rewrites 98.6%

    \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({\left({4}^{0.125}\right)}^{2}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{0.125}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\color{blue}{\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}}^{0.5} \]
11. Step-by-step derivation

    1. lift-pow.f64 N/A

       \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({\left({4}^{\frac{1}{8}}\right)}^{2}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{\frac{1}{2}} \]

    2. lift-pow.f64 N/A

       \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({\left({4}^{\frac{1}{8}}\right)}^{2}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{\frac{1}{2}} \]

    3. pow-pow N/A

       \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({4}^{\left(\frac{1}{8} \cdot 2\right)}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{\frac{1}{2}} \]

    4. metadata-eval N/A

       \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({4}^{\frac{1}{4}}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{\frac{1}{8}}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{\frac{1}{2}} \]

    5. lower-pow.f64 98.8

       \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({4}^{0.25}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{0.125}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5} \]

12. Applied rewrites 98.8%

    \[\leadsto \mathsf{fma}\left({\left(t \cdot \pi\right)}^{-1}, {\left({4}^{0.25}\right)}^{-1}, \mathsf{fma}\left(\mathsf{fma}\left(-4, \frac{\frac{v \cdot v}{t}}{{\left({4}^{0.125}\right)}^{2} \cdot \pi}, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right), v \cdot v, -4 \cdot {\left(\left({\left({4}^{0.125}\right)}^{2} \cdot \pi\right) \cdot t\right)}^{-1}\right) \cdot \left(v \cdot v\right)\right) \cdot {\left({\left(\mathsf{fma}\left(v \cdot v, -3, 1\right)\right)}^{-1}\right)}^{0.5} \]
13. Add Preprocessing

Reproduce

herbie shell --seed 2025065 
(FPCore (v t)
  :name "Falkner and Boettcher, Equation (20:1,3)"
  :precision binary64
  (/ (- 1.0 (* 5.0 (* v v))) (* (* (* PI t) (sqrt (* 2.0 (- 1.0 (* 3.0 (* v v)))))) (- 1.0 (* v v)))))