Ian Simplification

Percentage Accurate: 6.8% → 8.3%

Time: 1.5min

Alternatives: 8

Speedup: 1.1×

Specification

Math

\[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

FPCore

(FPCore (x)
  :precision binary64
  (- (/ PI 2) (* 2 (asin (sqrt (/ (- 1 x) 2))))))

C

double code(double x) {
	return (((double) M_PI) / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
}

Java

public static double code(double x) {
	return (Math.PI / 2.0) - (2.0 * Math.asin(Math.sqrt(((1.0 - x) / 2.0))));
}

Python

def code(x):
	return (math.pi / 2.0) - (2.0 * math.asin(math.sqrt(((1.0 - x) / 2.0))))

Julia

function code(x)
	return Float64(Float64(pi / 2.0) - Float64(2.0 * asin(sqrt(Float64(Float64(1.0 - x) / 2.0)))))
end

MATLAB

function tmp = code(x)
	tmp = (pi / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
end

Wolfram

code[x_] := N[(N[(Pi / 2), $MachinePrecision] - N[(2 * N[ArcSin[N[Sqrt[N[(N[(1 - x), $MachinePrecision] / 2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Initial Program: 6.8% accurate, 1.0× speedup

Math

\[\frac{\pi}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

FPCore

(FPCore (x)
  :precision binary64
  (- (/ PI 2) (* 2 (asin (sqrt (/ (- 1 x) 2))))))

C

double code(double x) {
	return (((double) M_PI) / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
}

Java

public static double code(double x) {
	return (Math.PI / 2.0) - (2.0 * Math.asin(Math.sqrt(((1.0 - x) / 2.0))));
}

Python

def code(x):
	return (math.pi / 2.0) - (2.0 * math.asin(math.sqrt(((1.0 - x) / 2.0))))

Julia

function code(x)
	return Float64(Float64(pi / 2.0) - Float64(2.0 * asin(sqrt(Float64(Float64(1.0 - x) / 2.0)))))
end

MATLAB

function tmp = code(x)
	tmp = (pi / 2.0) - (2.0 * asin(sqrt(((1.0 - x) / 2.0))));
end

Wolfram

code[x_] := N[(N[(Pi / 2), $MachinePrecision] - N[(2 * N[ArcSin[N[Sqrt[N[(N[(1 - x), $MachinePrecision] / 2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Alternative 1: 8.3% accurate, 0.1× speedup

Math

\[\begin{array}{l} t_0 := 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\\ t_1 := t\_0 - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\\ \frac{{\left(\pi - t\_0\right)}^{2} \cdot t\_1 - t\_1 \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{t\_1}^{2}} \end{array} \]

FPCore

(FPCore (x)
  :precision binary64
  (let* ((t_0 (* 2 (acos (sqrt (* (- x 1) -1/2)))))
       (t_1 (- t_0 (* (pow PI 2/3) (* (cbrt PI) 3/2)))))
  (/
   (- (* (pow (- PI t_0) 2) t_1) (* t_1 (* (* 1/4 PI) PI)))
   (pow t_1 2))))

C

double code(double x) {
	double t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (pow(((double) M_PI), 0.6666666666666666) * (cbrt(((double) M_PI)) * 1.5));
	return ((pow((((double) M_PI) - t_0), 2.0) * t_1) - (t_1 * ((0.25 * ((double) M_PI)) * ((double) M_PI)))) / pow(t_1, 2.0);
}

Java

public static double code(double x) {
	double t_0 = 2.0 * Math.acos(Math.sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (Math.pow(Math.PI, 0.6666666666666666) * (Math.cbrt(Math.PI) * 1.5));
	return ((Math.pow((Math.PI - t_0), 2.0) * t_1) - (t_1 * ((0.25 * Math.PI) * Math.PI))) / Math.pow(t_1, 2.0);
}

Julia

function code(x)
	t_0 = Float64(2.0 * acos(sqrt(Float64(Float64(x - 1.0) * -0.5))))
	t_1 = Float64(t_0 - Float64((pi ^ 0.6666666666666666) * Float64(cbrt(pi) * 1.5)))
	return Float64(Float64(Float64((Float64(pi - t_0) ^ 2.0) * t_1) - Float64(t_1 * Float64(Float64(0.25 * pi) * pi))) / (t_1 ^ 2.0))
end

Wolfram

code[x_] := Block[{t$95$0 = N[(2 * N[ArcCos[N[Sqrt[N[(N[(x - 1), $MachinePrecision] * -1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 - N[(N[Power[Pi, 2/3], $MachinePrecision] * N[(N[Power[Pi, 1/3], $MachinePrecision] * 3/2), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[Power[N[(Pi - t$95$0), $MachinePrecision], 2], $MachinePrecision] * t$95$1), $MachinePrecision] - N[(t$95$1 * N[(N[(1/4 * Pi), $MachinePrecision] * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[Power[t$95$1, 2], $MachinePrecision]), $MachinePrecision]]]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. sub-flip N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right)} \]

   3. +-commutative N/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) + \frac{\pi}{2}} \]

   4. flip-+ N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

   5. lower-unsound-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

5. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) \cdot \left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \left(\frac{1}{2} \cdot \pi\right) \cdot \left(\frac{1}{2} \cdot \pi\right)}{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \frac{1}{2} \cdot \pi}} \]

7. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}} \]
8. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\frac{3}{2} \cdot \pi}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   2. *-commutative N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\pi \cdot \frac{3}{2}}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   3. lift-PI.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \frac{3}{2}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   4. add-cube-cbrt N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} \cdot \frac{3}{2}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   5. lift-PI.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \frac{3}{2}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   6. lift-cbrt.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \color{blue}{\sqrt[3]{\pi}}\right) \cdot \frac{3}{2}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   7. associate-*l* N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   8. lower-*.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   9. lift-PI.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\sqrt[3]{\color{blue}{\pi}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   10. pow1/3 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\color{blue}{{\pi}^{\frac{1}{3}}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   11. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   12. pow1/3 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \color{blue}{{\pi}^{\frac{1}{3}}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   13. pow-prod-up N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   14. lower-pow.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   15. metadata-eval N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\color{blue}{\frac{2}{3}}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

   16. lower-*.f64 6.6%

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \color{blue}{\left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

9. Applied rewrites 6.6%

   \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]
10. Step-by-step derivation

    1. lift-*.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\frac{3}{2} \cdot \pi}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    2. *-commutative N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\pi \cdot \frac{3}{2}}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    3. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \frac{3}{2}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    4. add-cube-cbrt N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} \cdot \frac{3}{2}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    5. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \frac{3}{2}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    6. lift-cbrt.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \color{blue}{\sqrt[3]{\pi}}\right) \cdot \frac{3}{2}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    7. associate-*l* N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    8. lower-*.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    9. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\sqrt[3]{\color{blue}{\pi}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    10. pow1/3 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\color{blue}{{\pi}^{\frac{1}{3}}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    11. lift-PI.f64 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    12. pow1/3 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \color{blue}{{\pi}^{\frac{1}{3}}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    13. pow-prod-up N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    14. lower-pow.f64 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    15. metadata-eval N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\color{blue}{\frac{2}{3}}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

    16. lower-*.f64 8.3%

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \color{blue}{\left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]

11. Applied rewrites 8.3%

    \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}} \]
12. Step-by-step derivation

    1. lift-*.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\frac{3}{2} \cdot \pi}\right)}^{2}} \]

    2. *-commutative N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\pi \cdot \frac{3}{2}}\right)}^{2}} \]

    3. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \frac{3}{2}\right)}^{2}} \]

    4. add-cube-cbrt N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right)} \cdot \frac{3}{2}\right)}^{2}} \]

    5. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \frac{3}{2}\right)}^{2}} \]

    6. lift-cbrt.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \color{blue}{\sqrt[3]{\pi}}\right) \cdot \frac{3}{2}\right)}^{2}} \]

    7. associate-*l* N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right)}^{2}} \]

    8. lower-*.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{\left(\sqrt[3]{\mathsf{PI}\left(\right)} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right)}^{2}} \]

    9. lift-PI.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\sqrt[3]{\color{blue}{\pi}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    10. pow1/3 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left(\color{blue}{{\pi}^{\frac{1}{3}}} \cdot \sqrt[3]{\mathsf{PI}\left(\right)}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    11. lift-PI.f64 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \sqrt[3]{\color{blue}{\pi}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    12. pow1/3 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \left({\pi}^{\frac{1}{3}} \cdot \color{blue}{{\pi}^{\frac{1}{3}}}\right) \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    13. pow-prod-up N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    14. lower-pow.f64 N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\left(\frac{1}{3} + \frac{1}{3}\right)}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    15. metadata-eval N/A

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\color{blue}{\frac{2}{3}}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right)}^{2}} \]

    16. lower-*.f64 8.3%

        \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \color{blue}{\left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right)}^{2}} \]

13. Applied rewrites 8.3%

    \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - {\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \color{blue}{{\pi}^{\frac{2}{3}} \cdot \left(\sqrt[3]{\pi} \cdot \frac{3}{2}\right)}\right)}^{2}} \]
14. Add Preprocessing

Alternative 2: 8.3% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\\ t_1 := t\_0 - \frac{3}{2} \cdot \pi\\ \frac{{\left(\pi - t\_0\right)}^{2} \cdot t\_1 - t\_1 \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{{\left(\cos^{-1} \left(\sqrt{\frac{-1}{2} \cdot \left(x - 1\right)}\right) \cdot 2 - \frac{3}{2} \cdot \pi\right)}^{-2}}} \end{array} \]

FPCore

(FPCore (x)
  :precision binary64
  (let* ((t_0 (* 2 (acos (sqrt (* (- x 1) -1/2)))))
       (t_1 (- t_0 (* 3/2 PI))))
  (/
   (- (* (pow (- PI t_0) 2) t_1) (* t_1 (* (* 1/4 PI) PI)))
   (/
    1
    (pow (- (* (acos (sqrt (* -1/2 (- x 1)))) 2) (* 3/2 PI)) -2)))))

C

double code(double x) {
	double t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (1.5 * ((double) M_PI));
	return ((pow((((double) M_PI) - t_0), 2.0) * t_1) - (t_1 * ((0.25 * ((double) M_PI)) * ((double) M_PI)))) / (1.0 / pow(((acos(sqrt((-0.5 * (x - 1.0)))) * 2.0) - (1.5 * ((double) M_PI))), -2.0));
}

Java

public static double code(double x) {
	double t_0 = 2.0 * Math.acos(Math.sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (1.5 * Math.PI);
	return ((Math.pow((Math.PI - t_0), 2.0) * t_1) - (t_1 * ((0.25 * Math.PI) * Math.PI))) / (1.0 / Math.pow(((Math.acos(Math.sqrt((-0.5 * (x - 1.0)))) * 2.0) - (1.5 * Math.PI)), -2.0));
}

Python

def code(x):
	t_0 = 2.0 * math.acos(math.sqrt(((x - 1.0) * -0.5)))
	t_1 = t_0 - (1.5 * math.pi)
	return ((math.pow((math.pi - t_0), 2.0) * t_1) - (t_1 * ((0.25 * math.pi) * math.pi))) / (1.0 / math.pow(((math.acos(math.sqrt((-0.5 * (x - 1.0)))) * 2.0) - (1.5 * math.pi)), -2.0))

Julia

function code(x)
	t_0 = Float64(2.0 * acos(sqrt(Float64(Float64(x - 1.0) * -0.5))))
	t_1 = Float64(t_0 - Float64(1.5 * pi))
	return Float64(Float64(Float64((Float64(pi - t_0) ^ 2.0) * t_1) - Float64(t_1 * Float64(Float64(0.25 * pi) * pi))) / Float64(1.0 / (Float64(Float64(acos(sqrt(Float64(-0.5 * Float64(x - 1.0)))) * 2.0) - Float64(1.5 * pi)) ^ -2.0)))
end

MATLAB

function tmp = code(x)
	t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	t_1 = t_0 - (1.5 * pi);
	tmp = ((((pi - t_0) ^ 2.0) * t_1) - (t_1 * ((0.25 * pi) * pi))) / (1.0 / (((acos(sqrt((-0.5 * (x - 1.0)))) * 2.0) - (1.5 * pi)) ^ -2.0));
end

Wolfram

code[x_] := Block[{t$95$0 = N[(2 * N[ArcCos[N[Sqrt[N[(N[(x - 1), $MachinePrecision] * -1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 - N[(3/2 * Pi), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[Power[N[(Pi - t$95$0), $MachinePrecision], 2], $MachinePrecision] * t$95$1), $MachinePrecision] - N[(t$95$1 * N[(N[(1/4 * Pi), $MachinePrecision] * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(1 / N[Power[N[(N[(N[ArcCos[N[Sqrt[N[(-1/2 * N[(x - 1), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * 2), $MachinePrecision] - N[(3/2 * Pi), $MachinePrecision]), $MachinePrecision], -2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. sub-flip N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right)} \]

   3. +-commutative N/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) + \frac{\pi}{2}} \]

   4. flip-+ N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

   5. lower-unsound-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

5. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) \cdot \left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \left(\frac{1}{2} \cdot \pi\right) \cdot \left(\frac{1}{2} \cdot \pi\right)}{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \frac{1}{2} \cdot \pi}} \]

7. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}} \]
8. Step-by-step derivation

   1. lift-pow.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}} \]

   2. metadata-eval N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{\color{blue}{\left(\mathsf{neg}\left(-2\right)\right)}}} \]

   3. pow-neg N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\color{blue}{\frac{1}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{-2}}}} \]

   4. lower-unsound-pow.f32 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{-2}}}} \]

   5. lower-pow.f32 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{-2}}}} \]

   6. metadata-eval N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{\color{blue}{\left(\mathsf{neg}\left(2\right)\right)}}}} \]

   7. pow-flip N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\color{blue}{\frac{1}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}}}} \]

   8. lift-pow.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\frac{1}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}}}} \]

   9. lower-unsound-/.f64 N/A

      \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\color{blue}{\frac{1}{\frac{1}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}}}} \]

   10. lift-pow.f64 N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\frac{1}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{2}}}}} \]

   11. pow-flip N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{\color{blue}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{\left(\mathsf{neg}\left(2\right)\right)}}}} \]

   12. metadata-eval N/A

       \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\frac{1}{{\left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right)}^{\color{blue}{-2}}}} \]

9. Applied rewrites 8.3%

   \[\leadsto \frac{{\left(\pi - 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\right)}^{2} \cdot \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) - \left(2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right) - \frac{3}{2} \cdot \pi\right) \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{\color{blue}{\frac{1}{{\left(\cos^{-1} \left(\sqrt{\frac{-1}{2} \cdot \left(x - 1\right)}\right) \cdot 2 - \frac{3}{2} \cdot \pi\right)}^{-2}}}} \]
10. Add Preprocessing

Alternative 3: 8.3% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\\ t_1 := t\_0 - \frac{3}{2} \cdot \pi\\ \frac{{\left(\pi - t\_0\right)}^{2} \cdot t\_1 - t\_1 \cdot \left(\left(\frac{1}{4} \cdot \pi\right) \cdot \pi\right)}{{t\_1}^{2}} \end{array} \]

FPCore

(FPCore (x)
  :precision binary64
  (let* ((t_0 (* 2 (acos (sqrt (* (- x 1) -1/2)))))
       (t_1 (- t_0 (* 3/2 PI))))
  (/
   (- (* (pow (- PI t_0) 2) t_1) (* t_1 (* (* 1/4 PI) PI)))
   (pow t_1 2))))

C

double code(double x) {
	double t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (1.5 * ((double) M_PI));
	return ((pow((((double) M_PI) - t_0), 2.0) * t_1) - (t_1 * ((0.25 * ((double) M_PI)) * ((double) M_PI)))) / pow(t_1, 2.0);
}

Java

public static double code(double x) {
	double t_0 = 2.0 * Math.acos(Math.sqrt(((x - 1.0) * -0.5)));
	double t_1 = t_0 - (1.5 * Math.PI);
	return ((Math.pow((Math.PI - t_0), 2.0) * t_1) - (t_1 * ((0.25 * Math.PI) * Math.PI))) / Math.pow(t_1, 2.0);
}

Python

def code(x):
	t_0 = 2.0 * math.acos(math.sqrt(((x - 1.0) * -0.5)))
	t_1 = t_0 - (1.5 * math.pi)
	return ((math.pow((math.pi - t_0), 2.0) * t_1) - (t_1 * ((0.25 * math.pi) * math.pi))) / math.pow(t_1, 2.0)

Julia

function code(x)
	t_0 = Float64(2.0 * acos(sqrt(Float64(Float64(x - 1.0) * -0.5))))
	t_1 = Float64(t_0 - Float64(1.5 * pi))
	return Float64(Float64(Float64((Float64(pi - t_0) ^ 2.0) * t_1) - Float64(t_1 * Float64(Float64(0.25 * pi) * pi))) / (t_1 ^ 2.0))
end

MATLAB

function tmp = code(x)
	t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	t_1 = t_0 - (1.5 * pi);
	tmp = ((((pi - t_0) ^ 2.0) * t_1) - (t_1 * ((0.25 * pi) * pi))) / (t_1 ^ 2.0);
end

Wolfram

code[x_] := Block[{t$95$0 = N[(2 * N[ArcCos[N[Sqrt[N[(N[(x - 1), $MachinePrecision] * -1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 - N[(3/2 * Pi), $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[Power[N[(Pi - t$95$0), $MachinePrecision], 2], $MachinePrecision] * t$95$1), $MachinePrecision] - N[(t$95$1 * N[(N[(1/4 * Pi), $MachinePrecision] * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[Power[t$95$1, 2], $MachinePrecision]), $MachinePrecision]]]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. sub-flip N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right)} \]

   3. +-commutative N/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) + \frac{\pi}{2}} \]

   4. flip-+ N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

   5. lower-unsound-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

5. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) \cdot \left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \left(\frac{1}{2} \cdot \pi\right) \cdot \left(\frac{1}{2} \cdot \pi\right)}{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \frac{1}{2} \cdot \pi}} \]

7. Applied rewrites 8.3%

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

Alternative 4: 8.3% accurate, 0.4× speedup

Math

\[\begin{array}{l} t_0 := 2 \cdot \cos^{-1} \left(\sqrt{\left(x - 1\right) \cdot \frac{-1}{2}}\right)\\ \frac{{\left(\pi - t\_0\right)}^{2} - \left(\frac{1}{4} \cdot \pi\right) \cdot \pi}{t\_0 - \frac{3}{2} \cdot \pi} \end{array} \]

FPCore

(FPCore (x)
  :precision binary64
  (let* ((t_0 (* 2 (acos (sqrt (* (- x 1) -1/2))))))
  (/ (- (pow (- PI t_0) 2) (* (* 1/4 PI) PI)) (- t_0 (* 3/2 PI)))))

C

double code(double x) {
	double t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	return (pow((((double) M_PI) - t_0), 2.0) - ((0.25 * ((double) M_PI)) * ((double) M_PI))) / (t_0 - (1.5 * ((double) M_PI)));
}

Java

public static double code(double x) {
	double t_0 = 2.0 * Math.acos(Math.sqrt(((x - 1.0) * -0.5)));
	return (Math.pow((Math.PI - t_0), 2.0) - ((0.25 * Math.PI) * Math.PI)) / (t_0 - (1.5 * Math.PI));
}

Python

def code(x):
	t_0 = 2.0 * math.acos(math.sqrt(((x - 1.0) * -0.5)))
	return (math.pow((math.pi - t_0), 2.0) - ((0.25 * math.pi) * math.pi)) / (t_0 - (1.5 * math.pi))

Julia

function code(x)
	t_0 = Float64(2.0 * acos(sqrt(Float64(Float64(x - 1.0) * -0.5))))
	return Float64(Float64((Float64(pi - t_0) ^ 2.0) - Float64(Float64(0.25 * pi) * pi)) / Float64(t_0 - Float64(1.5 * pi)))
end

MATLAB

function tmp = code(x)
	t_0 = 2.0 * acos(sqrt(((x - 1.0) * -0.5)));
	tmp = (((pi - t_0) ^ 2.0) - ((0.25 * pi) * pi)) / (t_0 - (1.5 * pi));
end

Wolfram

code[x_] := Block[{t$95$0 = N[(2 * N[ArcCos[N[Sqrt[N[(N[(x - 1), $MachinePrecision] * -1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[Power[N[(Pi - t$95$0), $MachinePrecision], 2], $MachinePrecision] - N[(N[(1/4 * Pi), $MachinePrecision] * Pi), $MachinePrecision]), $MachinePrecision] / N[(t$95$0 - N[(3/2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. sub-flip N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right)} \]

   3. +-commutative N/A

      \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) + \frac{\pi}{2}} \]

   4. flip-+ N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

   5. lower-unsound-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2} \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)\right)\right) - \frac{\pi}{2}}} \]

5. Applied rewrites 8.3%

   \[\leadsto \color{blue}{\frac{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) \cdot \left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \left(\frac{1}{2} \cdot \pi\right) \cdot \left(\frac{1}{2} \cdot \pi\right)}{\left(\cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2 - \pi\right) - \frac{1}{2} \cdot \pi}} \]

7. Applied rewrites 8.3%

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

Alternative 5: 8.3% accurate, 0.9× speedup

Math

\[\left(1 - \frac{\pi - \cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot 2}{\frac{1}{2} \cdot \pi}\right) \cdot \left(\frac{1}{2} \cdot \pi\right) \]

FPCore

(FPCore (x)
  :precision binary64
  (*
 (- 1 (/ (- PI (* (acos (sqrt (* (- 1 x) 1/2))) 2)) (* 1/2 PI)))
 (* 1/2 PI)))

C

double code(double x) {
	return (1.0 - ((((double) M_PI) - (acos(sqrt(((1.0 - x) * 0.5))) * 2.0)) / (0.5 * ((double) M_PI)))) * (0.5 * ((double) M_PI));
}

Java

public static double code(double x) {
	return (1.0 - ((Math.PI - (Math.acos(Math.sqrt(((1.0 - x) * 0.5))) * 2.0)) / (0.5 * Math.PI))) * (0.5 * Math.PI);
}

Python

def code(x):
	return (1.0 - ((math.pi - (math.acos(math.sqrt(((1.0 - x) * 0.5))) * 2.0)) / (0.5 * math.pi))) * (0.5 * math.pi)

Julia

function code(x)
	return Float64(Float64(1.0 - Float64(Float64(pi - Float64(acos(sqrt(Float64(Float64(1.0 - x) * 0.5))) * 2.0)) / Float64(0.5 * pi))) * Float64(0.5 * pi))
end

MATLAB

function tmp = code(x)
	tmp = (1.0 - ((pi - (acos(sqrt(((1.0 - x) * 0.5))) * 2.0)) / (0.5 * pi))) * (0.5 * pi);
end

Wolfram

code[x_] := N[(N[(1 - N[(N[(Pi - N[(N[ArcCos[N[Sqrt[N[(N[(1 - x), $MachinePrecision] * 1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * 2), $MachinePrecision]), $MachinePrecision] / N[(1/2 * Pi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(1/2 * Pi), $MachinePrecision]), $MachinePrecision]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. sub-to-mult N/A

      \[\leadsto \color{blue}{\left(1 - \frac{\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2}{\frac{\pi}{2}}\right) \cdot \frac{\pi}{2}} \]

   3. lower-unsound-*.f64 N/A

      \[\leadsto \color{blue}{\left(1 - \frac{\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2}{\frac{\pi}{2}}\right) \cdot \frac{\pi}{2}} \]

5. Applied rewrites 8.3%

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

Alternative 6: 8.3% accurate, 1.1× speedup

Math

\[\left(\frac{1}{2} \cdot \pi - \pi\right) - \cos^{-1} \left(\sqrt{\left(1 - x\right) \cdot \frac{1}{2}}\right) \cdot -2 \]

FPCore

(FPCore (x)
  :precision binary64
  (- (- (* 1/2 PI) PI) (* (acos (sqrt (* (- 1 x) 1/2))) -2)))

C

double code(double x) {
	return ((0.5 * ((double) M_PI)) - ((double) M_PI)) - (acos(sqrt(((1.0 - x) * 0.5))) * -2.0);
}

Java

public static double code(double x) {
	return ((0.5 * Math.PI) - Math.PI) - (Math.acos(Math.sqrt(((1.0 - x) * 0.5))) * -2.0);
}

Python

def code(x):
	return ((0.5 * math.pi) - math.pi) - (math.acos(math.sqrt(((1.0 - x) * 0.5))) * -2.0)

Julia

function code(x)
	return Float64(Float64(Float64(0.5 * pi) - pi) - Float64(acos(sqrt(Float64(Float64(1.0 - x) * 0.5))) * -2.0))
end

MATLAB

function tmp = code(x)
	tmp = ((0.5 * pi) - pi) - (acos(sqrt(((1.0 - x) * 0.5))) * -2.0);
end

Wolfram

code[x_] := N[(N[(N[(1/2 * Pi), $MachinePrecision] - Pi), $MachinePrecision] - N[(N[ArcCos[N[Sqrt[N[(N[(1 - x), $MachinePrecision] * 1/2), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * -2), $MachinePrecision]), $MachinePrecision]

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-*.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   2. lift-asin.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   3. asin-acos N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)} \]

   4. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\color{blue}{\pi}}{2} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\color{blue}{\frac{\pi}{2}} - \cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right) \]

   6. sub-flip-reverse N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \color{blue}{\left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)} \]

   7. acos-asin N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)}\right)\right)\right) \]

   8. lift-PI.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\color{blue}{\pi}}{2} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\color{blue}{\frac{\pi}{2}} - \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)\right)\right)\right)\right) \]

   10. lift-asin.f64 N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \left(\mathsf{neg}\left(\left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)}\right)\right)\right)\right) \]

   11. sub-negate-rev N/A

       \[\leadsto \frac{\pi}{2} - 2 \cdot \left(\frac{\pi}{2} + \color{blue}{\left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right)}\right) \]

   12. distribute-rgt-in N/A

       \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} \cdot 2 + \left(\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) - \frac{\pi}{2}\right) \cdot 2\right)} \]

3. Applied rewrites 8.3%

   \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]
4. Step-by-step derivation

   1. lift--.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2} - \left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   2. lift-+.f64 N/A

      \[\leadsto \frac{\pi}{2} - \color{blue}{\left(\pi + \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2\right)} \]

   3. associate--r+ N/A

      \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2} \]

   4. lower--.f64 N/A

      \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2} \]

   5. lower--.f64 8.3%

      \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \pi\right)} - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   6. lift-/.f64 N/A

      \[\leadsto \left(\color{blue}{\frac{\pi}{2}} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   7. mult-flip N/A

      \[\leadsto \left(\color{blue}{\pi \cdot \frac{1}{2}} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   8. metadata-eval N/A

      \[\leadsto \left(\pi \cdot \color{blue}{\frac{1}{2}} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   9. *-commutative N/A

      \[\leadsto \left(\color{blue}{\frac{1}{2} \cdot \pi} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   10. lower-*.f64 8.3%

       \[\leadsto \left(\color{blue}{\frac{1}{2} \cdot \pi} - \pi\right) - \left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2 \]

   11. lift-*.f64 N/A

       \[\leadsto \left(\frac{1}{2} \cdot \pi - \pi\right) - \color{blue}{\left(-\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right) \cdot 2} \]

   12. lift-neg.f64 N/A

       \[\leadsto \left(\frac{1}{2} \cdot \pi - \pi\right) - \color{blue}{\left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right)\right)\right)} \cdot 2 \]

   13. distribute-lft-neg-out N/A

       \[\leadsto \left(\frac{1}{2} \cdot \pi - \pi\right) - \color{blue}{\left(\mathsf{neg}\left(\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right) \cdot 2\right)\right)} \]

   14. distribute-rgt-neg-in N/A

       \[\leadsto \left(\frac{1}{2} \cdot \pi - \pi\right) - \color{blue}{\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right) \cdot \left(\mathsf{neg}\left(2\right)\right)} \]

   15. lower-*.f64 N/A

       \[\leadsto \left(\frac{1}{2} \cdot \pi - \pi\right) - \color{blue}{\cos^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right) \cdot \left(\mathsf{neg}\left(2\right)\right)} \]

5. Applied rewrites 8.3%

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

Alternative 7: 6.8% accurate, 1.1× speedup

Math

\[\frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right) \cdot 2 \]

FPCore

(FPCore (x)
  :precision binary64
  (- (* 1/2 PI) (* (asin (sqrt (* 1/2 (- 1 x)))) 2)))

C

double code(double x) {
	return (0.5 * ((double) M_PI)) - (asin(sqrt((0.5 * (1.0 - x)))) * 2.0);
}

Java

public static double code(double x) {
	return (0.5 * Math.PI) - (Math.asin(Math.sqrt((0.5 * (1.0 - x)))) * 2.0);
}

Python

def code(x):
	return (0.5 * math.pi) - (math.asin(math.sqrt((0.5 * (1.0 - x)))) * 2.0)

Julia

function code(x)
	return Float64(Float64(0.5 * pi) - Float64(asin(sqrt(Float64(0.5 * Float64(1.0 - x)))) * 2.0))
end

MATLAB

function tmp = code(x)
	tmp = (0.5 * pi) - (asin(sqrt((0.5 * (1.0 - x)))) * 2.0);
end

Wolfram

code[x_] := N[(N[(1/2 * Pi), $MachinePrecision] - N[(N[ArcSin[N[Sqrt[N[(1/2 * N[(1 - x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] * 2), $MachinePrecision]), $MachinePrecision]

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-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

   2. mult-flip N/A

      \[\leadsto \color{blue}{\pi \cdot \frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

   3. metadata-eval N/A

      \[\leadsto \pi \cdot \color{blue}{\frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

   4. *-commutative N/A

      \[\leadsto \color{blue}{\frac{1}{2} \cdot \pi} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

   5. lower-*.f64 6.8%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot \pi} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \]

   6. lift-*.f64 N/A

      \[\leadsto \frac{1}{2} \cdot \pi - \color{blue}{2 \cdot \sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right)} \]

   7. *-commutative N/A

      \[\leadsto \frac{1}{2} \cdot \pi - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \cdot 2} \]

   8. lower-*.f64 6.8%

      \[\leadsto \frac{1}{2} \cdot \pi - \color{blue}{\sin^{-1} \left(\sqrt{\frac{1 - x}{2}}\right) \cdot 2} \]

   9. lift-/.f64 N/A

      \[\leadsto \frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\color{blue}{\frac{1 - x}{2}}}\right) \cdot 2 \]

   10. mult-flip N/A

       \[\leadsto \frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\color{blue}{\left(1 - x\right) \cdot \frac{1}{2}}}\right) \cdot 2 \]

   11. metadata-eval N/A

       \[\leadsto \frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\left(1 - x\right) \cdot \color{blue}{\frac{1}{2}}}\right) \cdot 2 \]

   12. *-commutative N/A

       \[\leadsto \frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\color{blue}{\frac{1}{2} \cdot \left(1 - x\right)}}\right) \cdot 2 \]

   13. lower-*.f64 6.8%

       \[\leadsto \frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\color{blue}{\frac{1}{2} \cdot \left(1 - x\right)}}\right) \cdot 2 \]

3. Applied rewrites 6.8%

   \[\leadsto \color{blue}{\frac{1}{2} \cdot \pi - \sin^{-1} \left(\sqrt{\frac{1}{2} \cdot \left(1 - x\right)}\right) \cdot 2} \]
4. Add Preprocessing

Alternative 8: 4.1% accurate, 1.2× speedup

Math

\[\pi \cdot \frac{1}{2} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]

FPCore

(FPCore (x)
  :precision binary64
  (- (* PI 1/2) (* 2 (asin (sqrt 1/2)))))

C

double code(double x) {
	return (((double) M_PI) * 0.5) - (2.0 * asin(sqrt(0.5)));
}

Java

public static double code(double x) {
	return (Math.PI * 0.5) - (2.0 * Math.asin(Math.sqrt(0.5)));
}

Python

def code(x):
	return (math.pi * 0.5) - (2.0 * math.asin(math.sqrt(0.5)))

Julia

function code(x)
	return Float64(Float64(pi * 0.5) - Float64(2.0 * asin(sqrt(0.5))))
end

MATLAB

function tmp = code(x)
	tmp = (pi * 0.5) - (2.0 * asin(sqrt(0.5)));
end

Wolfram

code[x_] := N[(N[(Pi * 1/2), $MachinePrecision] - N[(2 * N[ArcSin[N[Sqrt[1/2], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

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

4. Applied rewrites 4.1%

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

   1. lift-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\pi}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]

   2. mult-flip N/A

      \[\leadsto \color{blue}{\pi \cdot \frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]

   3. metadata-eval N/A

      \[\leadsto \pi \cdot \color{blue}{\frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]

   4. lower-*.f64 4.1%

      \[\leadsto \color{blue}{\pi \cdot \frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]

6. Applied rewrites 4.1%

   \[\leadsto \color{blue}{\pi \cdot \frac{1}{2}} - 2 \cdot \sin^{-1} \left(\sqrt{\frac{1}{2}}\right) \]
7. Add Preprocessing

Reproduce

herbie shell --seed 2025271 -o generate:evaluate
(FPCore (x)
  :name "Ian Simplification"
  :precision binary64
  (- (/ PI 2) (* 2 (asin (sqrt (/ (- 1 x) 2))))))