Ian Simplification

Percentage Accurate: 6.8% → 8.3%
Time: 6.2s
Alternatives: 7
Speedup: 1.3×

Specification

?
\[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
(FPCore (x)
  :precision binary64
  (- (/ PI 2.0) (* 2.0 (asin (sqrt (/ (- 1.0 x) 2.0))))))
double code(double x) {
	return (((double) M_PI) / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
}
public static double code(double x) {
	return (Math.PI / 2.0) - (2.0 * Math.asin(Math.sqrt(((1.0 - x) / 2.0))));
}
def code(x):
	return (math.pi / 2.0) - (2.0 * math.asin(math.sqrt(((1.0 - x) / 2.0))))
function code(x)
	return Float64(Float64(pi / 2.0) - Float64(2.0 * asin(sqrt(Float64(Float64(1.0 - x) / 2.0)))))
end
function tmp = code(x)
	tmp = (pi / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
end
code[x_] := N[(N[(Pi / 2.0), $MachinePrecision] - N[(2.0 * N[ArcSin[N[Sqrt[N[(N[(1.0 - x), $MachinePrecision] / 2.0), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 7 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 6.8% accurate, 1.0× speedup?

\[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
(FPCore (x)
  :precision binary64
  (- (/ PI 2.0) (* 2.0 (asin (sqrt (/ (- 1.0 x) 2.0))))))
double code(double x) {
	return (((double) M_PI) / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
}
public static double code(double x) {
	return (Math.PI / 2.0) - (2.0 * Math.asin(Math.sqrt(((1.0 - x) / 2.0))));
}
def code(x):
	return (math.pi / 2.0) - (2.0 * math.asin(math.sqrt(((1.0 - x) / 2.0))))
function code(x)
	return Float64(Float64(pi / 2.0) - Float64(2.0 * asin(sqrt(Float64(Float64(1.0 - x) / 2.0)))))
end
function tmp = code(x)
	tmp = (pi / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
end
code[x_] := N[(N[(Pi / 2.0), $MachinePrecision] - N[(2.0 * N[ArcSin[N[Sqrt[N[(N[(1.0 - x), $MachinePrecision] / 2.0), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)

Alternative 1: 8.3% accurate, 0.3× speedup?

\[\begin{array}{l} t_0 := \sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\\ t_1 := \cos^{-1} t\_0\\ \left(\frac{\frac{1}{\mathsf{fma}\left(\frac{\pi}{t\_1}, 0.5, -1\right)} - 1}{t\_1} \cdot \sin^{-1} t\_0\right) \cdot t\_1 \end{array} \]
(FPCore (x)
  :precision binary64
  (let* ((t_0 (sqrt (fma x -0.5 0.5))) (t_1 (acos t_0)))
  (*
   (* (/ (- (/ 1.0 (fma (/ PI t_1) 0.5 -1.0)) 1.0) t_1) (asin t_0))
   t_1)))
double code(double x) {
	double t_0 = sqrt(fma(x, -0.5, 0.5));
	double t_1 = acos(t_0);
	return ((((1.0 / fma((((double) M_PI) / t_1), 0.5, -1.0)) - 1.0) / t_1) * asin(t_0)) * t_1;
}
function code(x)
	t_0 = sqrt(fma(x, -0.5, 0.5))
	t_1 = acos(t_0)
	return Float64(Float64(Float64(Float64(Float64(1.0 / fma(Float64(pi / t_1), 0.5, -1.0)) - 1.0) / t_1) * asin(t_0)) * t_1)
end
code[x_] := Block[{t$95$0 = N[Sqrt[N[(x * -0.5 + 0.5), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[ArcCos[t$95$0], $MachinePrecision]}, N[(N[(N[(N[(N[(1.0 / N[(N[(Pi / t$95$1), $MachinePrecision] * 0.5 + -1.0), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision] / t$95$1), $MachinePrecision] * N[ArcSin[t$95$0], $MachinePrecision]), $MachinePrecision] * t$95$1), $MachinePrecision]]]
\begin{array}{l}
t_0 := \sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\\
t_1 := \cos^{-1} t\_0\\
\left(\frac{\frac{1}{\mathsf{fma}\left(\frac{\pi}{t\_1}, 0.5, -1\right)} - 1}{t\_1} \cdot \sin^{-1} t\_0\right) \cdot t\_1
\end{array}
Derivation
  1. Initial program 6.8%

    \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
  2. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    3. count-2-revN/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) + \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]
    4. associate--r+N/A

      \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    5. lift-/.f64N/A

      \[\leadsto \left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    6. lift-PI.f64N/A

      \[\leadsto \left(\frac{\color{blue}{\mathsf{PI}\left(\right)}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    7. lift-asin.f64N/A

      \[\leadsto \left(\frac{\mathsf{PI}\left(\right)}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    8. acos-asinN/A

      \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    9. sub-to-multN/A

      \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    10. lower-unsound-*.f64N/A

      \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
  3. Applied rewrites6.9%

    \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)} \]
  4. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \left(1 - \color{blue}{\frac{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    2. lift-asin.f64N/A

      \[\leadsto \left(1 - \frac{\color{blue}{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    3. asin-acosN/A

      \[\leadsto \left(1 - \frac{\color{blue}{\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    4. lift-PI.f64N/A

      \[\leadsto \left(1 - \frac{\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    5. lift-/.f64N/A

      \[\leadsto \left(1 - \frac{\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    6. lift-acos.f64N/A

      \[\leadsto \left(1 - \frac{\frac{\pi}{2} - \color{blue}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    7. div-subN/A

      \[\leadsto \left(1 - \color{blue}{\left(\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    8. lower--.f64N/A

      \[\leadsto \left(1 - \color{blue}{\left(\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    9. lower-/.f64N/A

      \[\leadsto \left(1 - \left(\color{blue}{\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    10. lift-/.f64N/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{\pi}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    11. mult-flipN/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\pi \cdot \frac{1}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    12. metadata-evalN/A

      \[\leadsto \left(1 - \left(\frac{\pi \cdot \color{blue}{\frac{1}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    13. *-commutativeN/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{1}{2} \cdot \pi}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    14. lift-*.f64N/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{1}{2} \cdot \pi}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    15. lift-fma.f64N/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{x \cdot \frac{-1}{2} + \frac{1}{2}}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    16. *-commutativeN/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{\frac{-1}{2} \cdot x} + \frac{1}{2}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    17. lower-fma.f64N/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    18. lower-/.f648.2%

      \[\leadsto \left(1 - \left(\frac{0.5 \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)} - \color{blue}{\frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  5. Applied rewrites8.2%

    \[\leadsto \left(1 - \color{blue}{\left(\frac{0.5 \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  6. Applied rewrites8.2%

    \[\leadsto \color{blue}{\left(\frac{\frac{1}{\mathsf{fma}\left(\frac{\pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}, 0.5, -1\right)} - 1}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)} \cdot \sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\right)} \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  7. Add Preprocessing

Alternative 2: 8.2% accurate, 0.6× speedup?

\[\begin{array}{l} t_0 := \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\\ \left(-\mathsf{fma}\left(\frac{\pi}{t\_0}, 0.5, -2\right)\right) \cdot t\_0 \end{array} \]
(FPCore (x)
  :precision binary64
  (let* ((t_0 (acos (sqrt (fma x -0.5 0.5)))))
  (* (- (fma (/ PI t_0) 0.5 -2.0)) t_0)))
double code(double x) {
	double t_0 = acos(sqrt(fma(x, -0.5, 0.5)));
	return -fma((((double) M_PI) / t_0), 0.5, -2.0) * t_0;
}
function code(x)
	t_0 = acos(sqrt(fma(x, -0.5, 0.5)))
	return Float64(Float64(-fma(Float64(pi / t_0), 0.5, -2.0)) * t_0)
end
code[x_] := Block[{t$95$0 = N[ArcCos[N[Sqrt[N[(x * -0.5 + 0.5), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]}, N[((-N[(N[(Pi / t$95$0), $MachinePrecision] * 0.5 + -2.0), $MachinePrecision]) * t$95$0), $MachinePrecision]]
\begin{array}{l}
t_0 := \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\\
\left(-\mathsf{fma}\left(\frac{\pi}{t\_0}, 0.5, -2\right)\right) \cdot t\_0
\end{array}
Derivation
  1. Initial program 6.8%

    \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
  2. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    3. count-2-revN/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) + \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]
    4. associate--r+N/A

      \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    5. lift-/.f64N/A

      \[\leadsto \left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    6. lift-PI.f64N/A

      \[\leadsto \left(\frac{\color{blue}{\mathsf{PI}\left(\right)}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    7. lift-asin.f64N/A

      \[\leadsto \left(\frac{\mathsf{PI}\left(\right)}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    8. acos-asinN/A

      \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    9. sub-to-multN/A

      \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
    10. lower-unsound-*.f64N/A

      \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}{\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]
  3. Applied rewrites6.9%

    \[\leadsto \color{blue}{\left(1 - \frac{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)} \]
  4. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \left(1 - \color{blue}{\frac{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    2. lift-asin.f64N/A

      \[\leadsto \left(1 - \frac{\color{blue}{\sin^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    3. asin-acosN/A

      \[\leadsto \left(1 - \frac{\color{blue}{\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    4. lift-PI.f64N/A

      \[\leadsto \left(1 - \frac{\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    5. lift-/.f64N/A

      \[\leadsto \left(1 - \frac{\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    6. lift-acos.f64N/A

      \[\leadsto \left(1 - \frac{\frac{\pi}{2} - \color{blue}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    7. div-subN/A

      \[\leadsto \left(1 - \color{blue}{\left(\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    8. lower--.f64N/A

      \[\leadsto \left(1 - \color{blue}{\left(\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    9. lower-/.f64N/A

      \[\leadsto \left(1 - \left(\color{blue}{\frac{\frac{\pi}{2}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    10. lift-/.f64N/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{\pi}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    11. mult-flipN/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\pi \cdot \frac{1}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    12. metadata-evalN/A

      \[\leadsto \left(1 - \left(\frac{\pi \cdot \color{blue}{\frac{1}{2}}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    13. *-commutativeN/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{1}{2} \cdot \pi}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    14. lift-*.f64N/A

      \[\leadsto \left(1 - \left(\frac{\color{blue}{\frac{1}{2} \cdot \pi}}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    15. lift-fma.f64N/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{x \cdot \frac{-1}{2} + \frac{1}{2}}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    16. *-commutativeN/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{\frac{-1}{2} \cdot x} + \frac{1}{2}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    17. lower-fma.f64N/A

      \[\leadsto \left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\color{blue}{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    18. lower-/.f648.2%

      \[\leadsto \left(1 - \left(\frac{0.5 \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)} - \color{blue}{\frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}}\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  5. Applied rewrites8.2%

    \[\leadsto \left(1 - \color{blue}{\left(\frac{0.5 \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(-0.5, x, 0.5\right)}\right)}\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  6. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\left(1 - \left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}\right)\right)} \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    2. sub-negate-revN/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}\right) - 1\right)\right)\right)} \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    3. lower-neg.f64N/A

      \[\leadsto \color{blue}{\left(-\left(\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}\right) - 1\right)\right)} \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    4. lift--.f64N/A

      \[\leadsto \left(-\left(\color{blue}{\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} - \frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}\right)} - 1\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    5. sub-flipN/A

      \[\leadsto \left(-\left(\color{blue}{\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} + \left(\mathsf{neg}\left(\frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}\right)\right)\right)} - 1\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    6. lift-/.f64N/A

      \[\leadsto \left(-\left(\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} + \left(\mathsf{neg}\left(\color{blue}{\frac{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)}}\right)\right)\right) - 1\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    7. *-inversesN/A

      \[\leadsto \left(-\left(\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} + \left(\mathsf{neg}\left(\color{blue}{1}\right)\right)\right) - 1\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    8. metadata-evalN/A

      \[\leadsto \left(-\left(\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} + \color{blue}{-1}\right) - 1\right)\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
    9. associate--l+N/A

      \[\leadsto \left(-\color{blue}{\left(\frac{\frac{1}{2} \cdot \pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} + \left(-1 - 1\right)\right)}\right) \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \]
  7. Applied rewrites8.2%

    \[\leadsto \color{blue}{\left(-\mathsf{fma}\left(\frac{\pi}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)}, 0.5, -2\right)\right)} \cdot \cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right) \]
  8. Add Preprocessing

Alternative 3: 8.2% accurate, 0.9× speedup?

\[\left(1 - \frac{\mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right)}{1.5707963267948966}\right) \cdot 1.5707963267948966 \]
(FPCore (x)
  :precision binary64
  (*
 (-
  1.0
  (/ (fma (acos (sqrt (fma x -0.5 0.5))) -2.0 PI) 1.5707963267948966))
 1.5707963267948966))
double code(double x) {
	return (1.0 - (fma(acos(sqrt(fma(x, -0.5, 0.5))), -2.0, ((double) M_PI)) / 1.5707963267948966)) * 1.5707963267948966;
}
function code(x)
	return Float64(Float64(1.0 - Float64(fma(acos(sqrt(fma(x, -0.5, 0.5))), -2.0, pi) / 1.5707963267948966)) * 1.5707963267948966)
end
code[x_] := N[(N[(1.0 - N[(N[(N[ArcCos[N[Sqrt[N[(x * -0.5 + 0.5), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * -2.0 + Pi), $MachinePrecision] / 1.5707963267948966), $MachinePrecision]), $MachinePrecision] * 1.5707963267948966), $MachinePrecision]
\left(1 - \frac{\mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right)}{1.5707963267948966}\right) \cdot 1.5707963267948966
Derivation
  1. Initial program 6.8%

    \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
  2. Applied rewrites8.3%

    \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\right) \cdot 2\right)} \]
  3. Evaluated real constant8.3%

    \[\leadsto \color{blue}{1.5707963267948966} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\right) \cdot 2\right) \]
  4. Step-by-step derivation
    1. lift--.f64N/A

      \[\leadsto \color{blue}{\frac{884279719003555}{562949953421312} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2\right)} \]
    2. sub-to-multN/A

      \[\leadsto \color{blue}{\left(1 - \frac{\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2}{\frac{884279719003555}{562949953421312}}\right) \cdot \frac{884279719003555}{562949953421312}} \]
    3. lower-unsound-*.f64N/A

      \[\leadsto \color{blue}{\left(1 - \frac{\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2}{\frac{884279719003555}{562949953421312}}\right) \cdot \frac{884279719003555}{562949953421312}} \]
  5. Applied rewrites8.2%

    \[\leadsto \color{blue}{\left(1 - \frac{\mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right)}{1.5707963267948966}\right) \cdot 1.5707963267948966} \]
  6. Add Preprocessing

Alternative 4: 8.2% accurate, 1.2× speedup?

\[1.5707963267948966 - \mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right) \]
(FPCore (x)
  :precision binary64
  (- 1.5707963267948966 (fma (acos (sqrt (fma x -0.5 0.5))) -2.0 PI)))
double code(double x) {
	return 1.5707963267948966 - fma(acos(sqrt(fma(x, -0.5, 0.5))), -2.0, ((double) M_PI));
}
function code(x)
	return Float64(1.5707963267948966 - fma(acos(sqrt(fma(x, -0.5, 0.5))), -2.0, pi))
end
code[x_] := N[(1.5707963267948966 - N[(N[ArcCos[N[Sqrt[N[(x * -0.5 + 0.5), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * -2.0 + Pi), $MachinePrecision]), $MachinePrecision]
1.5707963267948966 - \mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right)
Derivation
  1. Initial program 6.8%

    \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
  2. Applied rewrites8.3%

    \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\right) \cdot 2\right)} \]
  3. Evaluated real constant8.3%

    \[\leadsto \color{blue}{1.5707963267948966} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right)\right) \cdot 2\right) \]
  4. Step-by-step derivation
    1. lift-+.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2\right)} \]
    2. +-commutativeN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \color{blue}{\left(\left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2 + \pi\right)} \]
    3. lift-*.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\color{blue}{\left(-\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right) \cdot 2} + \pi\right) \]
    4. lift-neg.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\color{blue}{\left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)\right)\right)} \cdot 2 + \pi\right) \]
    5. distribute-lft-neg-outN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\color{blue}{\left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right) \cdot 2\right)\right)} + \pi\right) \]
    6. lift-sqrt.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \color{blue}{\left(\sqrt{\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)}\right)} \cdot 2\right)\right) + \pi\right) \]
    7. pow1/2N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \color{blue}{\left({\left(\mathsf{fma}\left(x, \frac{-1}{2}, \frac{1}{2}\right)\right)}^{\frac{1}{2}}\right)} \cdot 2\right)\right) + \pi\right) \]
    8. lift-fma.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \left({\color{blue}{\left(x \cdot \frac{-1}{2} + \frac{1}{2}\right)}}^{\frac{1}{2}}\right) \cdot 2\right)\right) + \pi\right) \]
    9. add-flipN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \left({\color{blue}{\left(x \cdot \frac{-1}{2} - \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)}}^{\frac{1}{2}}\right) \cdot 2\right)\right) + \pi\right) \]
    10. *-commutativeN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \left({\left(\color{blue}{\frac{-1}{2} \cdot x} - \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)}^{\frac{1}{2}}\right) \cdot 2\right)\right) + \pi\right) \]
    11. add-flipN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \left({\color{blue}{\left(\frac{-1}{2} \cdot x + \frac{1}{2}\right)}}^{\frac{1}{2}}\right) \cdot 2\right)\right) + \pi\right) \]
    12. lift-fma.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \left({\color{blue}{\left(\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)\right)}}^{\frac{1}{2}}\right) \cdot 2\right)\right) + \pi\right) \]
    13. pow1/2N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \color{blue}{\left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} \cdot 2\right)\right) + \pi\right) \]
    14. lift-sqrt.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\left(\mathsf{neg}\left(\cos^{-1} \color{blue}{\left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right)} \cdot 2\right)\right) + \pi\right) \]
    15. distribute-rgt-neg-inN/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \left(\color{blue}{\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right) \cdot \left(\mathsf{neg}\left(2\right)\right)} + \pi\right) \]
    16. lower-fma.f64N/A

      \[\leadsto \frac{884279719003555}{562949953421312} - \color{blue}{\mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(\frac{-1}{2}, x, \frac{1}{2}\right)}\right), \mathsf{neg}\left(2\right), \pi\right)} \]
  5. Applied rewrites8.3%

    \[\leadsto 1.5707963267948966 - \color{blue}{\mathsf{fma}\left(\cos^{-1} \left(\sqrt{\mathsf{fma}\left(x, -0.5, 0.5\right)}\right), -2, \pi\right)} \]
  6. Add Preprocessing

Alternative 5: 6.8% accurate, 1.3× speedup?

\[\mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5 \cdot \left(1 - x\right)}\right), -2, 1.5707963267948966\right) \]
(FPCore (x)
  :precision binary64
  (fma (asin (sqrt (* 0.5 (- 1.0 x)))) -2.0 1.5707963267948966))
double code(double x) {
	return fma(asin(sqrt((0.5 * (1.0 - x)))), -2.0, 1.5707963267948966);
}
function code(x)
	return fma(asin(sqrt(Float64(0.5 * Float64(1.0 - x)))), -2.0, 1.5707963267948966)
end
code[x_] := N[(N[ArcSin[N[Sqrt[N[(0.5 * N[(1.0 - x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * -2.0 + 1.5707963267948966), $MachinePrecision]
\mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5 \cdot \left(1 - x\right)}\right), -2, 1.5707963267948966\right)
Derivation
  1. Initial program 6.8%

    \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
  2. Taylor expanded in x around 0

    \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{\frac{1}{2}}}\right) \]
  3. Step-by-step derivation
    1. Applied rewrites4.1%

      \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{0.5}}\right) \]
    2. Evaluated real constant4.1%

      \[\leadsto \color{blue}{1.5707963267948966} - 2 \cdot \sin^{-1} \left(\sqrt{0.5}\right) \]
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \color{blue}{\frac{884279719003555}{562949953421312} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{884279719003555}{562949953421312} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
      3. fp-cancel-sub-sign-invN/A

        \[\leadsto \color{blue}{\frac{884279719003555}{562949953421312} + \left(\mathsf{neg}\left(2\right)\right) \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
      4. +-commutativeN/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(2\right)\right) \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) + \frac{884279719003555}{562949953421312}} \]
      5. *-commutativeN/A

        \[\leadsto \color{blue}{\sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \cdot \left(\mathsf{neg}\left(2\right)\right)} + \frac{884279719003555}{562949953421312} \]
      6. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\sin^{-1} \left(\sqrt{\frac{1}{2}}\right), \mathsf{neg}\left(2\right), \frac{884279719003555}{562949953421312}\right)} \]
      7. metadata-eval4.1%

        \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), \color{blue}{-2}, 1.5707963267948966\right) \]
    4. Applied rewrites4.1%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), -2, 1.5707963267948966\right)} \]
    5. Taylor expanded in x around 0

      \[\leadsto \mathsf{fma}\left(\color{blue}{\sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)}, -2, 1.5707963267948966\right) \]
    6. Step-by-step derivation
      1. lower-asin.f64N/A

        \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right), -2, \frac{884279719003555}{562949953421312}\right) \]
      2. lower-sqrt.f64N/A

        \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right), -2, \frac{884279719003555}{562949953421312}\right) \]
      3. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right), -2, \frac{884279719003555}{562949953421312}\right) \]
      4. lower--.f646.8%

        \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5 \cdot \left(1 - x\right)}\right), -2, 1.5707963267948966\right) \]
    7. Applied rewrites6.8%

      \[\leadsto \mathsf{fma}\left(\color{blue}{\sin^{-1} \left(\sqrt{0.5 \cdot \left(1 - x\right)}\right)}, -2, 1.5707963267948966\right) \]
    8. Add Preprocessing

    Alternative 6: 4.1% accurate, 1.5× speedup?

    \[\cos^{-1} \left(\sqrt{0.5}\right) - \sin^{-1} \left(\sqrt{0.5}\right) \]
    (FPCore (x)
      :precision binary64
      (- (acos (sqrt 0.5)) (asin (sqrt 0.5))))
    double code(double x) {
    	return acos(sqrt(0.5)) - asin(sqrt(0.5));
    }
    
    module fmin_fmax_functions
        implicit none
        private
        public fmax
        public fmin
    
        interface fmax
            module procedure fmax88
            module procedure fmax44
            module procedure fmax84
            module procedure fmax48
        end interface
        interface fmin
            module procedure fmin88
            module procedure fmin44
            module procedure fmin84
            module procedure fmin48
        end interface
    contains
        real(8) function fmax88(x, y) result (res)
            real(8), intent (in) :: x
            real(8), intent (in) :: y
            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
        end function
        real(4) function fmax44(x, y) result (res)
            real(4), intent (in) :: x
            real(4), intent (in) :: y
            res = merge(y, merge(x, max(x, y), y /= y), x /= x)
        end function
        real(8) function fmax84(x, y) result(res)
            real(8), intent (in) :: x
            real(4), intent (in) :: y
            res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
        end function
        real(8) function fmax48(x, y) result(res)
            real(4), intent (in) :: x
            real(8), intent (in) :: y
            res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
        end function
        real(8) function fmin88(x, y) result (res)
            real(8), intent (in) :: x
            real(8), intent (in) :: y
            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
        end function
        real(4) function fmin44(x, y) result (res)
            real(4), intent (in) :: x
            real(4), intent (in) :: y
            res = merge(y, merge(x, min(x, y), y /= y), x /= x)
        end function
        real(8) function fmin84(x, y) result(res)
            real(8), intent (in) :: x
            real(4), intent (in) :: y
            res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
        end function
        real(8) function fmin48(x, y) result(res)
            real(4), intent (in) :: x
            real(8), intent (in) :: y
            res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
        end function
    end module
    
    real(8) function code(x)
    use fmin_fmax_functions
        real(8), intent (in) :: x
        code = acos(sqrt(0.5d0)) - asin(sqrt(0.5d0))
    end function
    
    public static double code(double x) {
    	return Math.acos(Math.sqrt(0.5)) - Math.asin(Math.sqrt(0.5));
    }
    
    def code(x):
    	return math.acos(math.sqrt(0.5)) - math.asin(math.sqrt(0.5))
    
    function code(x)
    	return Float64(acos(sqrt(0.5)) - asin(sqrt(0.5)))
    end
    
    function tmp = code(x)
    	tmp = acos(sqrt(0.5)) - asin(sqrt(0.5));
    end
    
    code[x_] := N[(N[ArcCos[N[Sqrt[0.5], $MachinePrecision]], $MachinePrecision] - N[ArcSin[N[Sqrt[0.5], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
    
    \cos^{-1} \left(\sqrt{0.5}\right) - \sin^{-1} \left(\sqrt{0.5}\right)
    
    Derivation
    1. Initial program 6.8%

      \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
    2. Taylor expanded in x around 0

      \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{\frac{1}{2}}}\right) \]
    3. Step-by-step derivation
      1. Applied rewrites4.1%

        \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{0.5}}\right) \]
      2. Step-by-step derivation
        1. lift--.f64N/A

          \[\leadsto \color{blue}{\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
        3. count-2-revN/A

          \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1}{2}}\right) + \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)\right)} \]
        4. associate--r+N/A

          \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
        5. lift-/.f64N/A

          \[\leadsto \left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]
        6. lift-PI.f64N/A

          \[\leadsto \left(\frac{\color{blue}{\mathsf{PI}\left(\right)}}{2} - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)\right) - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]
        7. lift-asin.f64N/A

          \[\leadsto \left(\frac{\mathsf{PI}\left(\right)}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1}{2}}\right)}\right) - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]
        8. acos-asinN/A

          \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{\frac{1}{2}}\right)} - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]
        9. lower--.f64N/A

          \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{\frac{1}{2}}\right) - \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
        10. lower-acos.f644.1%

          \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{0.5}\right)} - \sin^{-1} \left(\sqrt{0.5}\right) \]
      3. Applied rewrites4.1%

        \[\leadsto \color{blue}{\cos^{-1} \left(\sqrt{0.5}\right) - \sin^{-1} \left(\sqrt{0.5}\right)} \]
      4. Add Preprocessing

      Alternative 7: 4.1% accurate, 1.9× speedup?

      \[\mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), -2, 1.5707963267948966\right) \]
      (FPCore (x)
        :precision binary64
        (fma (asin (sqrt 0.5)) -2.0 1.5707963267948966))
      double code(double x) {
      	return fma(asin(sqrt(0.5)), -2.0, 1.5707963267948966);
      }
      
      function code(x)
      	return fma(asin(sqrt(0.5)), -2.0, 1.5707963267948966)
      end
      
      code[x_] := N[(N[ArcSin[N[Sqrt[0.5], $MachinePrecision]], $MachinePrecision] * -2.0 + 1.5707963267948966), $MachinePrecision]
      
      \mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), -2, 1.5707963267948966\right)
      
      Derivation
      1. Initial program 6.8%

        \[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]
      2. Taylor expanded in x around 0

        \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{\frac{1}{2}}}\right) \]
      3. Step-by-step derivation
        1. Applied rewrites4.1%

          \[\leadsto \frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\color{blue}{0.5}}\right) \]
        2. Evaluated real constant4.1%

          \[\leadsto \color{blue}{1.5707963267948966} - 2 \cdot \sin^{-1} \left(\sqrt{0.5}\right) \]
        3. Step-by-step derivation
          1. lift--.f64N/A

            \[\leadsto \color{blue}{\frac{884279719003555}{562949953421312} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{884279719003555}{562949953421312} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
          3. fp-cancel-sub-sign-invN/A

            \[\leadsto \color{blue}{\frac{884279719003555}{562949953421312} + \left(\mathsf{neg}\left(2\right)\right) \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right)} \]
          4. +-commutativeN/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(2\right)\right) \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) + \frac{884279719003555}{562949953421312}} \]
          5. *-commutativeN/A

            \[\leadsto \color{blue}{\sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \cdot \left(\mathsf{neg}\left(2\right)\right)} + \frac{884279719003555}{562949953421312} \]
          6. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\sin^{-1} \left(\sqrt{\frac{1}{2}}\right), \mathsf{neg}\left(2\right), \frac{884279719003555}{562949953421312}\right)} \]
          7. metadata-eval4.1%

            \[\leadsto \mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), \color{blue}{-2}, 1.5707963267948966\right) \]
        4. Applied rewrites4.1%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\sin^{-1} \left(\sqrt{0.5}\right), -2, 1.5707963267948966\right)} \]
        5. Add Preprocessing

        Reproduce

        ?
        herbie shell --seed 2025212 
        (FPCore (x)
          :name "Ian Simplification"
          :precision binary64
          (- (/ PI 2.0) (* 2.0 (asin (sqrt (/ (- 1.0 x) 2.0))))))