NMSE Section 6.1 mentioned, B

Percentage Accurate: 78.4% → 99.7%
Time: 10.1s
Alternatives: 10
Speedup: 2.4×

Specification

?
\[\begin{array}{l} \\ \left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \end{array} \]
(FPCore (a b)
 :precision binary64
 (* (* (/ PI 2.0) (/ 1.0 (- (* b b) (* a a)))) (- (/ 1.0 a) (/ 1.0 b))))
double code(double a, double b) {
	return ((((double) M_PI) / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
}
public static double code(double a, double b) {
	return ((Math.PI / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
}
def code(a, b):
	return ((math.pi / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b))
function code(a, b)
	return Float64(Float64(Float64(pi / 2.0) * Float64(1.0 / Float64(Float64(b * b) - Float64(a * a)))) * Float64(Float64(1.0 / a) - Float64(1.0 / b)))
end
function tmp = code(a, b)
	tmp = ((pi / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
end
code[a_, b_] := N[(N[(N[(Pi / 2.0), $MachinePrecision] * N[(1.0 / N[(N[(b * b), $MachinePrecision] - N[(a * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[(1.0 / a), $MachinePrecision] - N[(1.0 / b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 10 alternatives:

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

Initial Program: 78.4% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \end{array} \]
(FPCore (a b)
 :precision binary64
 (* (* (/ PI 2.0) (/ 1.0 (- (* b b) (* a a)))) (- (/ 1.0 a) (/ 1.0 b))))
double code(double a, double b) {
	return ((((double) M_PI) / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
}
public static double code(double a, double b) {
	return ((Math.PI / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
}
def code(a, b):
	return ((math.pi / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b))
function code(a, b)
	return Float64(Float64(Float64(pi / 2.0) * Float64(1.0 / Float64(Float64(b * b) - Float64(a * a)))) * Float64(Float64(1.0 / a) - Float64(1.0 / b)))
end
function tmp = code(a, b)
	tmp = ((pi / 2.0) * (1.0 / ((b * b) - (a * a)))) * ((1.0 / a) - (1.0 / b));
end
code[a_, b_] := N[(N[(N[(Pi / 2.0), $MachinePrecision] * N[(1.0 / N[(N[(b * b), $MachinePrecision] - N[(a * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[(1.0 / a), $MachinePrecision] - N[(1.0 / b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)
\end{array}

Alternative 1: 99.7% accurate, 2.0× speedup?

\[\begin{array}{l} \\ \frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a} \end{array} \]
(FPCore (a b) :precision binary64 (/ (/ PI (* (+ b a) 2.0)) (* b a)))
double code(double a, double b) {
	return (((double) M_PI) / ((b + a) * 2.0)) / (b * a);
}
public static double code(double a, double b) {
	return (Math.PI / ((b + a) * 2.0)) / (b * a);
}
def code(a, b):
	return (math.pi / ((b + a) * 2.0)) / (b * a)
function code(a, b)
	return Float64(Float64(pi / Float64(Float64(b + a) * 2.0)) / Float64(b * a))
end
function tmp = code(a, b)
	tmp = (pi / ((b + a) * 2.0)) / (b * a);
end
code[a_, b_] := N[(N[(Pi / N[(N[(b + a), $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision] / N[(b * a), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a}
\end{array}
Derivation
  1. Initial program 81.8%

    \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
    2. *-commutativeN/A

      \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
    3. lift-*.f64N/A

      \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
    4. lift-/.f64N/A

      \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
    5. un-div-invN/A

      \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
    6. associate-*r/N/A

      \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
    7. lift--.f64N/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
    8. lift-*.f64N/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
    9. lift-*.f64N/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
    10. difference-of-squaresN/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
    11. *-rgt-identityN/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
    12. *-lft-identityN/A

      \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
    13. times-fracN/A

      \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
    14. lower-*.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
  4. Applied rewrites99.6%

    \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
  5. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    2. lift-/.f64N/A

      \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    3. div-invN/A

      \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    4. lift-*.f64N/A

      \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    5. *-commutativeN/A

      \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    6. associate-/r*N/A

      \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    7. lift-/.f64N/A

      \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    8. un-div-invN/A

      \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    9. lift-/.f64N/A

      \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    10. associate-/l*N/A

      \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    11. lower-*.f64N/A

      \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    12. lower-/.f64N/A

      \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    13. lift-/.f64N/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    14. lift-/.f64N/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    15. frac-timesN/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    16. metadata-evalN/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    17. *-commutativeN/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    18. lift-*.f64N/A

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
    19. lower-/.f6499.6

      \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
  6. Applied rewrites99.6%

    \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
  7. Applied rewrites99.6%

    \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
  8. Add Preprocessing

Alternative 2: 96.4% accurate, 1.8× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\ \;\;\;\;\frac{\frac{\pi \cdot 0.5}{b \cdot a}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \end{array} \]
(FPCore (a b)
 :precision binary64
 (if (<= a -8.6e+121)
   (/ (/ (* PI 0.5) (* b a)) a)
   (/ (* PI 0.5) (* b (* a (+ b a))))))
double code(double a, double b) {
	double tmp;
	if (a <= -8.6e+121) {
		tmp = ((((double) M_PI) * 0.5) / (b * a)) / a;
	} else {
		tmp = (((double) M_PI) * 0.5) / (b * (a * (b + a)));
	}
	return tmp;
}
public static double code(double a, double b) {
	double tmp;
	if (a <= -8.6e+121) {
		tmp = ((Math.PI * 0.5) / (b * a)) / a;
	} else {
		tmp = (Math.PI * 0.5) / (b * (a * (b + a)));
	}
	return tmp;
}
def code(a, b):
	tmp = 0
	if a <= -8.6e+121:
		tmp = ((math.pi * 0.5) / (b * a)) / a
	else:
		tmp = (math.pi * 0.5) / (b * (a * (b + a)))
	return tmp
function code(a, b)
	tmp = 0.0
	if (a <= -8.6e+121)
		tmp = Float64(Float64(Float64(pi * 0.5) / Float64(b * a)) / a);
	else
		tmp = Float64(Float64(pi * 0.5) / Float64(b * Float64(a * Float64(b + a))));
	end
	return tmp
end
function tmp_2 = code(a, b)
	tmp = 0.0;
	if (a <= -8.6e+121)
		tmp = ((pi * 0.5) / (b * a)) / a;
	else
		tmp = (pi * 0.5) / (b * (a * (b + a)));
	end
	tmp_2 = tmp;
end
code[a_, b_] := If[LessEqual[a, -8.6e+121], N[(N[(N[(Pi * 0.5), $MachinePrecision] / N[(b * a), $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision], N[(N[(Pi * 0.5), $MachinePrecision] / N[(b * N[(a * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\
\;\;\;\;\frac{\frac{\pi \cdot 0.5}{b \cdot a}}{a}\\

\mathbf{else}:\\
\;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if a < -8.5999999999999994e121

    1. Initial program 71.8%

      \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
    2. Add Preprocessing
    3. Taylor expanded in b around 0

      \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
    4. Step-by-step derivation
      1. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
      2. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
      3. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
      4. lower-PI.f64N/A

        \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
      5. unpow2N/A

        \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
      6. associate-*l*N/A

        \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
      7. lower-*.f64N/A

        \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
      8. lower-*.f6498.1

        \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
    5. Applied rewrites98.1%

      \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]
    6. Step-by-step derivation
      1. Applied rewrites99.9%

        \[\leadsto \frac{\frac{\pi \cdot 0.5}{b \cdot a}}{\color{blue}{a}} \]

      if -8.5999999999999994e121 < a

      1. Initial program 83.1%

        \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
        2. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
        3. lift-*.f64N/A

          \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
        4. lift-/.f64N/A

          \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
        5. un-div-invN/A

          \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
        6. associate-*r/N/A

          \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
        7. lift--.f64N/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
        8. lift-*.f64N/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
        9. lift-*.f64N/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
        10. difference-of-squaresN/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
        11. *-rgt-identityN/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
        12. *-lft-identityN/A

          \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
        13. times-fracN/A

          \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
        14. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
      4. Applied rewrites99.6%

        \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
      5. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        2. lift-/.f64N/A

          \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        3. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        4. lift-*.f64N/A

          \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        5. *-commutativeN/A

          \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        6. associate-/r*N/A

          \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        7. lift-/.f64N/A

          \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        8. un-div-invN/A

          \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        9. lift-/.f64N/A

          \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        10. associate-/l*N/A

          \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        11. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        12. lower-/.f64N/A

          \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        13. lift-/.f64N/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        14. lift-/.f64N/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        15. frac-timesN/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        16. metadata-evalN/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        17. *-commutativeN/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        18. lift-*.f64N/A

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
        19. lower-/.f6499.6

          \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
      6. Applied rewrites99.6%

        \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
      7. Applied rewrites94.1%

        \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
    7. Recombined 2 regimes into one program.
    8. Add Preprocessing

    Alternative 3: 96.4% accurate, 1.8× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\ \;\;\;\;\frac{\pi \cdot \frac{0.5}{b \cdot a}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \end{array} \]
    (FPCore (a b)
     :precision binary64
     (if (<= a -8.6e+121)
       (/ (* PI (/ 0.5 (* b a))) a)
       (/ (* PI 0.5) (* b (* a (+ b a))))))
    double code(double a, double b) {
    	double tmp;
    	if (a <= -8.6e+121) {
    		tmp = (((double) M_PI) * (0.5 / (b * a))) / a;
    	} else {
    		tmp = (((double) M_PI) * 0.5) / (b * (a * (b + a)));
    	}
    	return tmp;
    }
    
    public static double code(double a, double b) {
    	double tmp;
    	if (a <= -8.6e+121) {
    		tmp = (Math.PI * (0.5 / (b * a))) / a;
    	} else {
    		tmp = (Math.PI * 0.5) / (b * (a * (b + a)));
    	}
    	return tmp;
    }
    
    def code(a, b):
    	tmp = 0
    	if a <= -8.6e+121:
    		tmp = (math.pi * (0.5 / (b * a))) / a
    	else:
    		tmp = (math.pi * 0.5) / (b * (a * (b + a)))
    	return tmp
    
    function code(a, b)
    	tmp = 0.0
    	if (a <= -8.6e+121)
    		tmp = Float64(Float64(pi * Float64(0.5 / Float64(b * a))) / a);
    	else
    		tmp = Float64(Float64(pi * 0.5) / Float64(b * Float64(a * Float64(b + a))));
    	end
    	return tmp
    end
    
    function tmp_2 = code(a, b)
    	tmp = 0.0;
    	if (a <= -8.6e+121)
    		tmp = (pi * (0.5 / (b * a))) / a;
    	else
    		tmp = (pi * 0.5) / (b * (a * (b + a)));
    	end
    	tmp_2 = tmp;
    end
    
    code[a_, b_] := If[LessEqual[a, -8.6e+121], N[(N[(Pi * N[(0.5 / N[(b * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision], N[(N[(Pi * 0.5), $MachinePrecision] / N[(b * N[(a * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\
    \;\;\;\;\frac{\pi \cdot \frac{0.5}{b \cdot a}}{a}\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if a < -8.5999999999999994e121

      1. Initial program 71.8%

        \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
      2. Add Preprocessing
      3. Taylor expanded in b around 0

        \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
      4. Step-by-step derivation
        1. associate-*r/N/A

          \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
        2. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
        3. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
        4. lower-PI.f64N/A

          \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
        5. unpow2N/A

          \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
        6. associate-*l*N/A

          \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
        7. lower-*.f64N/A

          \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
        8. lower-*.f6498.1

          \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
      5. Applied rewrites98.1%

        \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]
      6. Step-by-step derivation
        1. Applied rewrites85.6%

          \[\leadsto \pi \cdot \color{blue}{\frac{0.5}{b \cdot \left(a \cdot a\right)}} \]
        2. Step-by-step derivation
          1. Applied rewrites99.9%

            \[\leadsto \frac{\pi \cdot \frac{0.5}{b \cdot a}}{\color{blue}{a}} \]

          if -8.5999999999999994e121 < a

          1. Initial program 83.1%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
            2. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            4. lift-/.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. un-div-invN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            6. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
            8. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
            9. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
            10. difference-of-squaresN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. *-rgt-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
            12. *-lft-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
            13. times-fracN/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            14. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
          4. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
          5. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            2. lift-/.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            3. div-invN/A

              \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            4. lift-*.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            5. *-commutativeN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            6. associate-/r*N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            7. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            8. un-div-invN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            9. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            10. associate-/l*N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            11. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            12. lower-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            13. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            14. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            15. frac-timesN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            16. metadata-evalN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            17. *-commutativeN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            18. lift-*.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            19. lower-/.f6499.6

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
          6. Applied rewrites99.6%

            \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
          7. Applied rewrites94.1%

            \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
        3. Recombined 2 regimes into one program.
        4. Add Preprocessing

        Alternative 4: 96.4% accurate, 1.8× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\ \;\;\;\;\frac{0.5}{b \cdot a} \cdot \frac{\pi}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \end{array} \]
        (FPCore (a b)
         :precision binary64
         (if (<= a -8.6e+121)
           (* (/ 0.5 (* b a)) (/ PI a))
           (/ (* PI 0.5) (* b (* a (+ b a))))))
        double code(double a, double b) {
        	double tmp;
        	if (a <= -8.6e+121) {
        		tmp = (0.5 / (b * a)) * (((double) M_PI) / a);
        	} else {
        		tmp = (((double) M_PI) * 0.5) / (b * (a * (b + a)));
        	}
        	return tmp;
        }
        
        public static double code(double a, double b) {
        	double tmp;
        	if (a <= -8.6e+121) {
        		tmp = (0.5 / (b * a)) * (Math.PI / a);
        	} else {
        		tmp = (Math.PI * 0.5) / (b * (a * (b + a)));
        	}
        	return tmp;
        }
        
        def code(a, b):
        	tmp = 0
        	if a <= -8.6e+121:
        		tmp = (0.5 / (b * a)) * (math.pi / a)
        	else:
        		tmp = (math.pi * 0.5) / (b * (a * (b + a)))
        	return tmp
        
        function code(a, b)
        	tmp = 0.0
        	if (a <= -8.6e+121)
        		tmp = Float64(Float64(0.5 / Float64(b * a)) * Float64(pi / a));
        	else
        		tmp = Float64(Float64(pi * 0.5) / Float64(b * Float64(a * Float64(b + a))));
        	end
        	return tmp
        end
        
        function tmp_2 = code(a, b)
        	tmp = 0.0;
        	if (a <= -8.6e+121)
        		tmp = (0.5 / (b * a)) * (pi / a);
        	else
        		tmp = (pi * 0.5) / (b * (a * (b + a)));
        	end
        	tmp_2 = tmp;
        end
        
        code[a_, b_] := If[LessEqual[a, -8.6e+121], N[(N[(0.5 / N[(b * a), $MachinePrecision]), $MachinePrecision] * N[(Pi / a), $MachinePrecision]), $MachinePrecision], N[(N[(Pi * 0.5), $MachinePrecision] / N[(b * N[(a * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\
        \;\;\;\;\frac{0.5}{b \cdot a} \cdot \frac{\pi}{a}\\
        
        \mathbf{else}:\\
        \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if a < -8.5999999999999994e121

          1. Initial program 71.8%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Taylor expanded in b around 0

            \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
          4. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            2. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            3. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            4. lower-PI.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            5. unpow2N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
            6. associate-*l*N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            7. lower-*.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            8. lower-*.f6498.1

              \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
          5. Applied rewrites98.1%

            \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]
          6. Step-by-step derivation
            1. Applied rewrites99.8%

              \[\leadsto \frac{\pi}{a} \cdot \color{blue}{\frac{0.5}{b \cdot a}} \]

            if -8.5999999999999994e121 < a

            1. Initial program 83.1%

              \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              3. lift-*.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              4. lift-/.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. un-div-invN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              6. associate-*r/N/A

                \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
              8. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
              9. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
              10. difference-of-squaresN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. *-rgt-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
              12. *-lft-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
              13. times-fracN/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
              14. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            4. Applied rewrites99.6%

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
            5. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              2. lift-/.f64N/A

                \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              3. div-invN/A

                \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              4. lift-*.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              5. *-commutativeN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              6. associate-/r*N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              7. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              8. un-div-invN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              9. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              10. associate-/l*N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              11. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              12. lower-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              13. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              14. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              15. frac-timesN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              16. metadata-evalN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              17. *-commutativeN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              18. lift-*.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              19. lower-/.f6499.6

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
            6. Applied rewrites99.6%

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
            7. Applied rewrites94.1%

              \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
          7. Recombined 2 regimes into one program.
          8. Final simplification94.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -8.6 \cdot 10^{+121}:\\ \;\;\;\;\frac{0.5}{b \cdot a} \cdot \frac{\pi}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \]
          9. Add Preprocessing

          Alternative 5: 96.0% accurate, 2.0× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \leq 10^{+43}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \end{array} \]
          (FPCore (a b)
           :precision binary64
           (if (<= b 1e+43)
             (/ (* PI 0.5) (* a (* b (+ b a))))
             (/ (* PI 0.5) (* b (* a (+ b a))))))
          double code(double a, double b) {
          	double tmp;
          	if (b <= 1e+43) {
          		tmp = (((double) M_PI) * 0.5) / (a * (b * (b + a)));
          	} else {
          		tmp = (((double) M_PI) * 0.5) / (b * (a * (b + a)));
          	}
          	return tmp;
          }
          
          public static double code(double a, double b) {
          	double tmp;
          	if (b <= 1e+43) {
          		tmp = (Math.PI * 0.5) / (a * (b * (b + a)));
          	} else {
          		tmp = (Math.PI * 0.5) / (b * (a * (b + a)));
          	}
          	return tmp;
          }
          
          def code(a, b):
          	tmp = 0
          	if b <= 1e+43:
          		tmp = (math.pi * 0.5) / (a * (b * (b + a)))
          	else:
          		tmp = (math.pi * 0.5) / (b * (a * (b + a)))
          	return tmp
          
          function code(a, b)
          	tmp = 0.0
          	if (b <= 1e+43)
          		tmp = Float64(Float64(pi * 0.5) / Float64(a * Float64(b * Float64(b + a))));
          	else
          		tmp = Float64(Float64(pi * 0.5) / Float64(b * Float64(a * Float64(b + a))));
          	end
          	return tmp
          end
          
          function tmp_2 = code(a, b)
          	tmp = 0.0;
          	if (b <= 1e+43)
          		tmp = (pi * 0.5) / (a * (b * (b + a)));
          	else
          		tmp = (pi * 0.5) / (b * (a * (b + a)));
          	end
          	tmp_2 = tmp;
          end
          
          code[a_, b_] := If[LessEqual[b, 1e+43], N[(N[(Pi * 0.5), $MachinePrecision] / N[(a * N[(b * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(Pi * 0.5), $MachinePrecision] / N[(b * N[(a * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;b \leq 10^{+43}:\\
          \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)}\\
          
          \mathbf{else}:\\
          \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if b < 1.00000000000000001e43

            1. Initial program 81.7%

              \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              3. lift-*.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              4. lift-/.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. un-div-invN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              6. associate-*r/N/A

                \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
              8. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
              9. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
              10. difference-of-squaresN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. *-rgt-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
              12. *-lft-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
              13. times-fracN/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
              14. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            4. Applied rewrites99.5%

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
            5. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              2. lift-/.f64N/A

                \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              3. div-invN/A

                \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              4. lift-*.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              5. *-commutativeN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              6. associate-/r*N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              7. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              8. un-div-invN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              9. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              10. associate-/l*N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              11. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              12. lower-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              13. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              14. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              15. frac-timesN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              16. metadata-evalN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              17. *-commutativeN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              18. lift-*.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              19. lower-/.f6499.6

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
            6. Applied rewrites99.6%

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
            7. Applied rewrites99.6%

              \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
            8. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
              2. clear-numN/A

                \[\leadsto \color{blue}{\frac{1}{\frac{b \cdot a}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}}} \]
              3. associate-/r/N/A

                \[\leadsto \color{blue}{\frac{1}{b \cdot a} \cdot \frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}} \]
              4. lift-/.f64N/A

                \[\leadsto \frac{1}{b \cdot a} \cdot \color{blue}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}} \]
              5. times-fracN/A

                \[\leadsto \color{blue}{\frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot a\right) \cdot \left(\left(b + a\right) \cdot 2\right)}} \]
              6. lift-*.f64N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot a\right) \cdot \color{blue}{\left(\left(b + a\right) \cdot 2\right)}} \]
              7. associate-*r*N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(\left(b \cdot a\right) \cdot \left(b + a\right)\right) \cdot 2}} \]
              8. lift-*.f64N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(\color{blue}{\left(b \cdot a\right)} \cdot \left(b + a\right)\right) \cdot 2} \]
              9. associate-*r*N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(b \cdot \left(a \cdot \left(b + a\right)\right)\right)} \cdot 2} \]
              10. lift-*.f64N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot \color{blue}{\left(a \cdot \left(b + a\right)\right)}\right) \cdot 2} \]
              11. lift-*.f64N/A

                \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(b \cdot \left(a \cdot \left(b + a\right)\right)\right)} \cdot 2} \]
              12. frac-timesN/A

                \[\leadsto \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \frac{\mathsf{PI}\left(\right)}{2}} \]
              13. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \cdot \frac{\mathsf{PI}\left(\right)}{2} \]
              14. div-invN/A

                \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)} \]
              15. metadata-evalN/A

                \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{1}{2}}\right) \]
              16. lift-*.f64N/A

                \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)} \]
              17. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right) \cdot \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
              18. lift-/.f64N/A

                \[\leadsto \left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
              19. un-div-invN/A

                \[\leadsto \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
            9. Applied rewrites96.6%

              \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{a \cdot \left(\left(b + a\right) \cdot b\right)}} \]

            if 1.00000000000000001e43 < b

            1. Initial program 82.4%

              \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              3. lift-*.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
              4. lift-/.f64N/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. un-div-invN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              6. associate-*r/N/A

                \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
              8. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
              9. lift-*.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
              10. difference-of-squaresN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. *-rgt-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
              12. *-lft-identityN/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
              13. times-fracN/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
              14. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            4. Applied rewrites99.8%

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
            5. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              2. lift-/.f64N/A

                \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              3. div-invN/A

                \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              4. lift-*.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              5. *-commutativeN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              6. associate-/r*N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              7. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              8. un-div-invN/A

                \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              9. lift-/.f64N/A

                \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              10. associate-/l*N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              11. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              12. lower-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              13. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              14. lift-/.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              15. frac-timesN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              16. metadata-evalN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              17. *-commutativeN/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              18. lift-*.f64N/A

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
              19. lower-/.f6499.8

                \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
            6. Applied rewrites99.8%

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
            7. Applied rewrites99.2%

              \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification97.1%

            \[\leadsto \begin{array}{l} \mathbf{if}\;b \leq 10^{+43}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{b \cdot \left(a \cdot \left(b + a\right)\right)}\\ \end{array} \]
          5. Add Preprocessing

          Alternative 6: 99.6% accurate, 2.0× speedup?

          \[\begin{array}{l} \\ \frac{\pi}{b \cdot a} \cdot \frac{0.5}{b + a} \end{array} \]
          (FPCore (a b) :precision binary64 (* (/ PI (* b a)) (/ 0.5 (+ b a))))
          double code(double a, double b) {
          	return (((double) M_PI) / (b * a)) * (0.5 / (b + a));
          }
          
          public static double code(double a, double b) {
          	return (Math.PI / (b * a)) * (0.5 / (b + a));
          }
          
          def code(a, b):
          	return (math.pi / (b * a)) * (0.5 / (b + a))
          
          function code(a, b)
          	return Float64(Float64(pi / Float64(b * a)) * Float64(0.5 / Float64(b + a)))
          end
          
          function tmp = code(a, b)
          	tmp = (pi / (b * a)) * (0.5 / (b + a));
          end
          
          code[a_, b_] := N[(N[(Pi / N[(b * a), $MachinePrecision]), $MachinePrecision] * N[(0.5 / N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \frac{\pi}{b \cdot a} \cdot \frac{0.5}{b + a}
          \end{array}
          
          Derivation
          1. Initial program 81.8%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
            2. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            4. lift-/.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. un-div-invN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            6. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
            8. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
            9. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
            10. difference-of-squaresN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. *-rgt-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
            12. *-lft-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
            13. times-fracN/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            14. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
          4. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
          5. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            2. lift-/.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            3. div-invN/A

              \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            4. lift-*.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            5. *-commutativeN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            6. associate-/r*N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            7. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            8. un-div-invN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            9. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            10. associate-/l*N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            11. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            12. lower-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            13. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            14. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            15. frac-timesN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            16. metadata-evalN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            17. *-commutativeN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            18. lift-*.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            19. lower-/.f6499.6

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
          6. Applied rewrites99.6%

            \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
          7. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
          8. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
            2. clear-numN/A

              \[\leadsto \color{blue}{\frac{1}{\frac{b \cdot a}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}}} \]
            3. inv-powN/A

              \[\leadsto \color{blue}{{\left(\frac{b \cdot a}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}\right)}^{-1}} \]
            4. lift-/.f64N/A

              \[\leadsto {\left(\frac{b \cdot a}{\color{blue}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}}\right)}^{-1} \]
            5. associate-/r/N/A

              \[\leadsto {\color{blue}{\left(\frac{b \cdot a}{\mathsf{PI}\left(\right)} \cdot \left(\left(b + a\right) \cdot 2\right)\right)}}^{-1} \]
            6. lift-/.f64N/A

              \[\leadsto {\left(\color{blue}{\frac{b \cdot a}{\mathsf{PI}\left(\right)}} \cdot \left(\left(b + a\right) \cdot 2\right)\right)}^{-1} \]
            7. unpow-prod-downN/A

              \[\leadsto \color{blue}{{\left(\frac{b \cdot a}{\mathsf{PI}\left(\right)}\right)}^{-1} \cdot {\left(\left(b + a\right) \cdot 2\right)}^{-1}} \]
            8. inv-powN/A

              \[\leadsto \color{blue}{\frac{1}{\frac{b \cdot a}{\mathsf{PI}\left(\right)}}} \cdot {\left(\left(b + a\right) \cdot 2\right)}^{-1} \]
            9. lift-/.f64N/A

              \[\leadsto \frac{1}{\color{blue}{\frac{b \cdot a}{\mathsf{PI}\left(\right)}}} \cdot {\left(\left(b + a\right) \cdot 2\right)}^{-1} \]
            10. clear-numN/A

              \[\leadsto \color{blue}{\frac{\mathsf{PI}\left(\right)}{b \cdot a}} \cdot {\left(\left(b + a\right) \cdot 2\right)}^{-1} \]
            11. inv-powN/A

              \[\leadsto \frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \color{blue}{\frac{1}{\left(b + a\right) \cdot 2}} \]
            12. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \frac{1}{\left(b + a\right) \cdot 2}} \]
            13. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\mathsf{PI}\left(\right)}{b \cdot a}} \cdot \frac{1}{\left(b + a\right) \cdot 2} \]
            14. lift-*.f64N/A

              \[\leadsto \frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \frac{1}{\color{blue}{\left(b + a\right) \cdot 2}} \]
            15. *-commutativeN/A

              \[\leadsto \frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \frac{1}{\color{blue}{2 \cdot \left(b + a\right)}} \]
            16. associate-/r*N/A

              \[\leadsto \frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \color{blue}{\frac{\frac{1}{2}}{b + a}} \]
            17. metadata-evalN/A

              \[\leadsto \frac{\mathsf{PI}\left(\right)}{b \cdot a} \cdot \frac{\color{blue}{\frac{1}{2}}}{b + a} \]
            18. lower-/.f6499.6

              \[\leadsto \frac{\pi}{b \cdot a} \cdot \color{blue}{\frac{0.5}{b + a}} \]
          9. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\pi}{b \cdot a} \cdot \frac{0.5}{b + a}} \]
          10. Add Preprocessing

          Alternative 7: 71.8% accurate, 2.2× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \leq 2.5 \cdot 10^{-51}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot b\right)}\\ \end{array} \end{array} \]
          (FPCore (a b)
           :precision binary64
           (if (<= b 2.5e-51) (/ (* PI 0.5) (* a (* b a))) (/ (* PI 0.5) (* a (* b b)))))
          double code(double a, double b) {
          	double tmp;
          	if (b <= 2.5e-51) {
          		tmp = (((double) M_PI) * 0.5) / (a * (b * a));
          	} else {
          		tmp = (((double) M_PI) * 0.5) / (a * (b * b));
          	}
          	return tmp;
          }
          
          public static double code(double a, double b) {
          	double tmp;
          	if (b <= 2.5e-51) {
          		tmp = (Math.PI * 0.5) / (a * (b * a));
          	} else {
          		tmp = (Math.PI * 0.5) / (a * (b * b));
          	}
          	return tmp;
          }
          
          def code(a, b):
          	tmp = 0
          	if b <= 2.5e-51:
          		tmp = (math.pi * 0.5) / (a * (b * a))
          	else:
          		tmp = (math.pi * 0.5) / (a * (b * b))
          	return tmp
          
          function code(a, b)
          	tmp = 0.0
          	if (b <= 2.5e-51)
          		tmp = Float64(Float64(pi * 0.5) / Float64(a * Float64(b * a)));
          	else
          		tmp = Float64(Float64(pi * 0.5) / Float64(a * Float64(b * b)));
          	end
          	return tmp
          end
          
          function tmp_2 = code(a, b)
          	tmp = 0.0;
          	if (b <= 2.5e-51)
          		tmp = (pi * 0.5) / (a * (b * a));
          	else
          		tmp = (pi * 0.5) / (a * (b * b));
          	end
          	tmp_2 = tmp;
          end
          
          code[a_, b_] := If[LessEqual[b, 2.5e-51], N[(N[(Pi * 0.5), $MachinePrecision] / N[(a * N[(b * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(Pi * 0.5), $MachinePrecision] / N[(a * N[(b * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;b \leq 2.5 \cdot 10^{-51}:\\
          \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)}\\
          
          \mathbf{else}:\\
          \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot b\right)}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if b < 2.50000000000000002e-51

            1. Initial program 79.5%

              \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
            2. Add Preprocessing
            3. Taylor expanded in b around 0

              \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            4. Step-by-step derivation
              1. associate-*r/N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
              2. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
              3. lower-*.f64N/A

                \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
              4. lower-PI.f64N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
              5. unpow2N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
              6. associate-*l*N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
              7. lower-*.f64N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
              8. lower-*.f6472.2

                \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
            5. Applied rewrites72.2%

              \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]

            if 2.50000000000000002e-51 < b

            1. Initial program 87.2%

              \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
            2. Add Preprocessing
            3. Taylor expanded in b around inf

              \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{a \cdot {b}^{2}}} \]
            4. Step-by-step derivation
              1. associate-*r/N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{a \cdot {b}^{2}}} \]
              2. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{a \cdot {b}^{2}}} \]
              3. lower-*.f64N/A

                \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{a \cdot {b}^{2}} \]
              4. lower-PI.f64N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{a \cdot {b}^{2}} \]
              5. lower-*.f64N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot {b}^{2}}} \]
              6. unpow2N/A

                \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{a \cdot \color{blue}{\left(b \cdot b\right)}} \]
              7. lower-*.f6483.9

                \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(b \cdot b\right)}} \]
            5. Applied rewrites83.9%

              \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(b \cdot b\right)}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification75.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;b \leq 2.5 \cdot 10^{-51}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi \cdot 0.5}{a \cdot \left(b \cdot b\right)}\\ \end{array} \]
          5. Add Preprocessing

          Alternative 8: 93.2% accurate, 2.4× speedup?

          \[\begin{array}{l} \\ \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)} \end{array} \]
          (FPCore (a b) :precision binary64 (/ (* PI 0.5) (* a (* b (+ b a)))))
          double code(double a, double b) {
          	return (((double) M_PI) * 0.5) / (a * (b * (b + a)));
          }
          
          public static double code(double a, double b) {
          	return (Math.PI * 0.5) / (a * (b * (b + a)));
          }
          
          def code(a, b):
          	return (math.pi * 0.5) / (a * (b * (b + a)))
          
          function code(a, b)
          	return Float64(Float64(pi * 0.5) / Float64(a * Float64(b * Float64(b + a))))
          end
          
          function tmp = code(a, b)
          	tmp = (pi * 0.5) / (a * (b * (b + a)));
          end
          
          code[a_, b_] := N[(N[(Pi * 0.5), $MachinePrecision] / N[(a * N[(b * N[(b + a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)}
          \end{array}
          
          Derivation
          1. Initial program 81.8%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)} \]
            2. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            3. lift-*.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right)} \]
            4. lift-/.f64N/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \left(\frac{\mathsf{PI}\left(\right)}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. un-div-invN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            6. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b - a \cdot a}} \]
            8. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{b \cdot b} - a \cdot a} \]
            9. lift-*.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
            10. difference-of-squaresN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. *-rgt-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(b - \color{blue}{a \cdot 1}\right)} \]
            12. *-lft-identityN/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\mathsf{PI}\left(\right)}{2}}{\left(b + a\right) \cdot \left(\color{blue}{1 \cdot b} - a \cdot 1\right)} \]
            13. times-fracN/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
            14. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{a} - \frac{1}{b}}{b + a} \cdot \frac{\frac{\mathsf{PI}\left(\right)}{2}}{1 \cdot b - a \cdot 1}} \]
          4. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a} \cdot \frac{\pi \cdot 0.5}{b - a}} \]
          5. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{b - a}{b \cdot a}}{b + a}} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            2. lift-/.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{b - a}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            3. div-invN/A

              \[\leadsto \frac{\color{blue}{\left(b - a\right) \cdot \frac{1}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            4. lift-*.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{b \cdot a}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            5. *-commutativeN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{1}{\color{blue}{a \cdot b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            6. associate-/r*N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a}}{b}}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            7. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}}}{b}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            8. un-div-invN/A

              \[\leadsto \frac{\left(b - a\right) \cdot \color{blue}{\left(\frac{1}{a} \cdot \frac{1}{b}\right)}}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            9. lift-/.f64N/A

              \[\leadsto \frac{\left(b - a\right) \cdot \left(\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}\right)}{b + a} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            10. associate-/l*N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            11. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}\right)} \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            12. lower-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \color{blue}{\frac{\frac{1}{a} \cdot \frac{1}{b}}{b + a}}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            13. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{a} \cdot \color{blue}{\frac{1}{b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            14. lift-/.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{a}} \cdot \frac{1}{b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            15. frac-timesN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1 \cdot 1}{a \cdot b}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            16. metadata-evalN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{\color{blue}{1}}{a \cdot b}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            17. *-commutativeN/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            18. lift-*.f64N/A

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\frac{1}{\color{blue}{b \cdot a}}}{b + a}\right) \cdot \frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b - a} \]
            19. lower-/.f6499.6

              \[\leadsto \left(\left(b - a\right) \cdot \frac{\color{blue}{\frac{1}{b \cdot a}}}{b + a}\right) \cdot \frac{\pi \cdot 0.5}{b - a} \]
          6. Applied rewrites99.6%

            \[\leadsto \color{blue}{\left(\left(b - a\right) \cdot \frac{\frac{1}{b \cdot a}}{b + a}\right)} \cdot \frac{\pi \cdot 0.5}{b - a} \]
          7. Applied rewrites99.6%

            \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
          8. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}{b \cdot a}} \]
            2. clear-numN/A

              \[\leadsto \color{blue}{\frac{1}{\frac{b \cdot a}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}}}} \]
            3. associate-/r/N/A

              \[\leadsto \color{blue}{\frac{1}{b \cdot a} \cdot \frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}} \]
            4. lift-/.f64N/A

              \[\leadsto \frac{1}{b \cdot a} \cdot \color{blue}{\frac{\mathsf{PI}\left(\right)}{\left(b + a\right) \cdot 2}} \]
            5. times-fracN/A

              \[\leadsto \color{blue}{\frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot a\right) \cdot \left(\left(b + a\right) \cdot 2\right)}} \]
            6. lift-*.f64N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot a\right) \cdot \color{blue}{\left(\left(b + a\right) \cdot 2\right)}} \]
            7. associate-*r*N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(\left(b \cdot a\right) \cdot \left(b + a\right)\right) \cdot 2}} \]
            8. lift-*.f64N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(\color{blue}{\left(b \cdot a\right)} \cdot \left(b + a\right)\right) \cdot 2} \]
            9. associate-*r*N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(b \cdot \left(a \cdot \left(b + a\right)\right)\right)} \cdot 2} \]
            10. lift-*.f64N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\left(b \cdot \color{blue}{\left(a \cdot \left(b + a\right)\right)}\right) \cdot 2} \]
            11. lift-*.f64N/A

              \[\leadsto \frac{1 \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(b \cdot \left(a \cdot \left(b + a\right)\right)\right)} \cdot 2} \]
            12. frac-timesN/A

              \[\leadsto \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \frac{\mathsf{PI}\left(\right)}{2}} \]
            13. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \cdot \frac{\mathsf{PI}\left(\right)}{2} \]
            14. div-invN/A

              \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)} \]
            15. metadata-evalN/A

              \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{1}{2}}\right) \]
            16. lift-*.f64N/A

              \[\leadsto \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)} \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right)} \]
            17. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right) \cdot \frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
            18. lift-/.f64N/A

              \[\leadsto \left(\mathsf{PI}\left(\right) \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
            19. un-div-invN/A

              \[\leadsto \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot \frac{1}{2}}{b \cdot \left(a \cdot \left(b + a\right)\right)}} \]
          9. Applied rewrites95.3%

            \[\leadsto \color{blue}{\frac{\pi \cdot 0.5}{a \cdot \left(\left(b + a\right) \cdot b\right)}} \]
          10. Final simplification95.3%

            \[\leadsto \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(b + a\right)\right)} \]
          11. Add Preprocessing

          Alternative 9: 62.3% accurate, 2.6× speedup?

          \[\begin{array}{l} \\ \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)} \end{array} \]
          (FPCore (a b) :precision binary64 (/ (* PI 0.5) (* a (* b a))))
          double code(double a, double b) {
          	return (((double) M_PI) * 0.5) / (a * (b * a));
          }
          
          public static double code(double a, double b) {
          	return (Math.PI * 0.5) / (a * (b * a));
          }
          
          def code(a, b):
          	return (math.pi * 0.5) / (a * (b * a))
          
          function code(a, b)
          	return Float64(Float64(pi * 0.5) / Float64(a * Float64(b * a)))
          end
          
          function tmp = code(a, b)
          	tmp = (pi * 0.5) / (a * (b * a));
          end
          
          code[a_, b_] := N[(N[(Pi * 0.5), $MachinePrecision] / N[(a * N[(b * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)}
          \end{array}
          
          Derivation
          1. Initial program 81.8%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Taylor expanded in b around 0

            \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
          4. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            2. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            3. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            4. lower-PI.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            5. unpow2N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
            6. associate-*l*N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            7. lower-*.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            8. lower-*.f6463.6

              \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
          5. Applied rewrites63.6%

            \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]
          6. Final simplification63.6%

            \[\leadsto \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot a\right)} \]
          7. Add Preprocessing

          Alternative 10: 56.4% accurate, 2.6× speedup?

          \[\begin{array}{l} \\ \pi \cdot \frac{0.5}{b \cdot \left(a \cdot a\right)} \end{array} \]
          (FPCore (a b) :precision binary64 (* PI (/ 0.5 (* b (* a a)))))
          double code(double a, double b) {
          	return ((double) M_PI) * (0.5 / (b * (a * a)));
          }
          
          public static double code(double a, double b) {
          	return Math.PI * (0.5 / (b * (a * a)));
          }
          
          def code(a, b):
          	return math.pi * (0.5 / (b * (a * a)))
          
          function code(a, b)
          	return Float64(pi * Float64(0.5 / Float64(b * Float64(a * a))))
          end
          
          function tmp = code(a, b)
          	tmp = pi * (0.5 / (b * (a * a)));
          end
          
          code[a_, b_] := N[(Pi * N[(0.5 / N[(b * N[(a * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \pi \cdot \frac{0.5}{b \cdot \left(a \cdot a\right)}
          \end{array}
          
          Derivation
          1. Initial program 81.8%

            \[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right) \]
          2. Add Preprocessing
          3. Taylor expanded in b around 0

            \[\leadsto \color{blue}{\frac{1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
          4. Step-by-step derivation
            1. associate-*r/N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            2. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{{a}^{2} \cdot b}} \]
            3. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            4. lower-PI.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}}{{a}^{2} \cdot b} \]
            5. unpow2N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left(a \cdot a\right)} \cdot b} \]
            6. associate-*l*N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            7. lower-*.f64N/A

              \[\leadsto \frac{\frac{1}{2} \cdot \mathsf{PI}\left(\right)}{\color{blue}{a \cdot \left(a \cdot b\right)}} \]
            8. lower-*.f6463.6

              \[\leadsto \frac{0.5 \cdot \pi}{a \cdot \color{blue}{\left(a \cdot b\right)}} \]
          5. Applied rewrites63.6%

            \[\leadsto \color{blue}{\frac{0.5 \cdot \pi}{a \cdot \left(a \cdot b\right)}} \]
          6. Step-by-step derivation
            1. Applied rewrites57.8%

              \[\leadsto \pi \cdot \color{blue}{\frac{0.5}{b \cdot \left(a \cdot a\right)}} \]
            2. Add Preprocessing

            Reproduce

            ?
            herbie shell --seed 2024232 
            (FPCore (a b)
              :name "NMSE Section 6.1 mentioned, B"
              :precision binary64
              (* (* (/ PI 2.0) (/ 1.0 (- (* b b) (* a a)))) (- (/ 1.0 a) (/ 1.0 b))))