NMSE Section 6.1 mentioned, B

Percentage Accurate: 78.8% → 99.6%
Time: 3.5s
Alternatives: 9
Speedup: 1.6×

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}

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 9 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.8% 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.6% accurate, 1.6× speedup?

\[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;b \leq 1.5 \cdot 10^{+44}:\\ \;\;\;\;\frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\frac{\pi}{b - a}}{a}}{b + b}\\ \end{array} \end{array} \]
NOTE: a and b should be sorted in increasing order before calling this function.
(FPCore (a b)
 :precision binary64
 (if (<= b 1.5e+44)
   (* (/ (/ PI a) (* (+ a b) b)) 0.5)
   (/ (/ (/ PI (- b a)) a) (+ b b))))
assert(a < b);
double code(double a, double b) {
	double tmp;
	if (b <= 1.5e+44) {
		tmp = ((((double) M_PI) / a) / ((a + b) * b)) * 0.5;
	} else {
		tmp = ((((double) M_PI) / (b - a)) / a) / (b + b);
	}
	return tmp;
}
assert a < b;
public static double code(double a, double b) {
	double tmp;
	if (b <= 1.5e+44) {
		tmp = ((Math.PI / a) / ((a + b) * b)) * 0.5;
	} else {
		tmp = ((Math.PI / (b - a)) / a) / (b + b);
	}
	return tmp;
}
[a, b] = sort([a, b])
def code(a, b):
	tmp = 0
	if b <= 1.5e+44:
		tmp = ((math.pi / a) / ((a + b) * b)) * 0.5
	else:
		tmp = ((math.pi / (b - a)) / a) / (b + b)
	return tmp
a, b = sort([a, b])
function code(a, b)
	tmp = 0.0
	if (b <= 1.5e+44)
		tmp = Float64(Float64(Float64(pi / a) / Float64(Float64(a + b) * b)) * 0.5);
	else
		tmp = Float64(Float64(Float64(pi / Float64(b - a)) / a) / Float64(b + b));
	end
	return tmp
end
a, b = num2cell(sort([a, b])){:}
function tmp_2 = code(a, b)
	tmp = 0.0;
	if (b <= 1.5e+44)
		tmp = ((pi / a) / ((a + b) * b)) * 0.5;
	else
		tmp = ((pi / (b - a)) / a) / (b + b);
	end
	tmp_2 = tmp;
end
NOTE: a and b should be sorted in increasing order before calling this function.
code[a_, b_] := If[LessEqual[b, 1.5e+44], N[(N[(N[(Pi / a), $MachinePrecision] / N[(N[(a + b), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], N[(N[(N[(Pi / N[(b - a), $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision] / N[(b + b), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
[a, b] = \mathsf{sort}([a, b])\\
\\
\begin{array}{l}
\mathbf{if}\;b \leq 1.5 \cdot 10^{+44}:\\
\;\;\;\;\frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\frac{\pi}{b - a}}{a}}{b + b}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if b < 1.49999999999999993e44

    1. Initial program 78.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. Step-by-step derivation
      1. lift-*.f64N/A

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

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

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

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

        \[\leadsto \color{blue}{\frac{\left(\pi \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)}{2}} \]
      6. mult-flipN/A

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

        \[\leadsto \color{blue}{\left(\left(\pi \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)\right) \cdot \frac{1}{2}} \]
    3. Applied rewrites87.9%

      \[\leadsto \color{blue}{\frac{\pi \cdot \frac{b - a}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot 0.5} \]
    4. Taylor expanded in a around 0

      \[\leadsto \frac{\pi \cdot \frac{\color{blue}{b}}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot \frac{1}{2} \]
    5. Step-by-step derivation
      1. Applied rewrites64.8%

        \[\leadsto \frac{\pi \cdot \frac{\color{blue}{b}}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot 0.5 \]
      2. Taylor expanded in a around 0

        \[\leadsto \frac{\pi \cdot \frac{b}{a \cdot b}}{\left(a + b\right) \cdot \color{blue}{b}} \cdot \frac{1}{2} \]
      3. Step-by-step derivation
        1. Applied rewrites93.7%

          \[\leadsto \frac{\pi \cdot \frac{b}{a \cdot b}}{\left(a + b\right) \cdot \color{blue}{b}} \cdot 0.5 \]
        2. Taylor expanded in a around 0

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

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

            \[\leadsto \frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5 \]
        4. Applied rewrites93.8%

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

        if 1.49999999999999993e44 < b

        1. Initial program 78.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. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
          5. mult-flip-revN/A

            \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
          7. lift--.f64N/A

            \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
          11. sub-negate-revN/A

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

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

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

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

            \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
          16. sub-negate-revN/A

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

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

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

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

          \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
        6. Taylor expanded in a around 0

          \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
        7. Step-by-step derivation
          1. lower-PI.f6466.3

            \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
        8. Applied rewrites66.3%

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

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

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

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

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

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

            \[\leadsto \color{blue}{\frac{\frac{\frac{\pi}{b - a}}{a}}{b + b}} \]
          7. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\frac{\frac{\pi}{b - a}}{a}}{b + b}} \]
          8. lower-/.f64N/A

            \[\leadsto \frac{\color{blue}{\frac{\frac{\pi}{b - a}}{a}}}{b + b} \]
          9. lower-/.f6466.7

            \[\leadsto \frac{\frac{\color{blue}{\frac{\pi}{b - a}}}{a}}{b + b} \]
        10. Applied rewrites66.7%

          \[\leadsto \color{blue}{\frac{\frac{\frac{\pi}{b - a}}{a}}{b + b}} \]
      4. Recombined 2 regimes into one program.
      5. Add Preprocessing

      Alternative 2: 99.6% accurate, 1.6× speedup?

      \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;b \leq 1.08 \cdot 10^{+76}:\\ \;\;\;\;\frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\pi}{\left(b + b\right) \cdot a}}{b - a}\\ \end{array} \end{array} \]
      NOTE: a and b should be sorted in increasing order before calling this function.
      (FPCore (a b)
       :precision binary64
       (if (<= b 1.08e+76)
         (* (/ (/ PI a) (* (+ a b) b)) 0.5)
         (/ (/ PI (* (+ b b) a)) (- b a))))
      assert(a < b);
      double code(double a, double b) {
      	double tmp;
      	if (b <= 1.08e+76) {
      		tmp = ((((double) M_PI) / a) / ((a + b) * b)) * 0.5;
      	} else {
      		tmp = (((double) M_PI) / ((b + b) * a)) / (b - a);
      	}
      	return tmp;
      }
      
      assert a < b;
      public static double code(double a, double b) {
      	double tmp;
      	if (b <= 1.08e+76) {
      		tmp = ((Math.PI / a) / ((a + b) * b)) * 0.5;
      	} else {
      		tmp = (Math.PI / ((b + b) * a)) / (b - a);
      	}
      	return tmp;
      }
      
      [a, b] = sort([a, b])
      def code(a, b):
      	tmp = 0
      	if b <= 1.08e+76:
      		tmp = ((math.pi / a) / ((a + b) * b)) * 0.5
      	else:
      		tmp = (math.pi / ((b + b) * a)) / (b - a)
      	return tmp
      
      a, b = sort([a, b])
      function code(a, b)
      	tmp = 0.0
      	if (b <= 1.08e+76)
      		tmp = Float64(Float64(Float64(pi / a) / Float64(Float64(a + b) * b)) * 0.5);
      	else
      		tmp = Float64(Float64(pi / Float64(Float64(b + b) * a)) / Float64(b - a));
      	end
      	return tmp
      end
      
      a, b = num2cell(sort([a, b])){:}
      function tmp_2 = code(a, b)
      	tmp = 0.0;
      	if (b <= 1.08e+76)
      		tmp = ((pi / a) / ((a + b) * b)) * 0.5;
      	else
      		tmp = (pi / ((b + b) * a)) / (b - a);
      	end
      	tmp_2 = tmp;
      end
      
      NOTE: a and b should be sorted in increasing order before calling this function.
      code[a_, b_] := If[LessEqual[b, 1.08e+76], N[(N[(N[(Pi / a), $MachinePrecision] / N[(N[(a + b), $MachinePrecision] * b), $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], N[(N[(Pi / N[(N[(b + b), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision] / N[(b - a), $MachinePrecision]), $MachinePrecision]]
      
      \begin{array}{l}
      [a, b] = \mathsf{sort}([a, b])\\
      \\
      \begin{array}{l}
      \mathbf{if}\;b \leq 1.08 \cdot 10^{+76}:\\
      \;\;\;\;\frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{\frac{\pi}{\left(b + b\right) \cdot a}}{b - a}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if b < 1.07999999999999999e76

        1. Initial program 78.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. Step-by-step derivation
          1. lift-*.f64N/A

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

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

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

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

            \[\leadsto \color{blue}{\frac{\left(\pi \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)}{2}} \]
          6. mult-flipN/A

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

            \[\leadsto \color{blue}{\left(\left(\pi \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)\right) \cdot \frac{1}{2}} \]
        3. Applied rewrites87.9%

          \[\leadsto \color{blue}{\frac{\pi \cdot \frac{b - a}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot 0.5} \]
        4. Taylor expanded in a around 0

          \[\leadsto \frac{\pi \cdot \frac{\color{blue}{b}}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot \frac{1}{2} \]
        5. Step-by-step derivation
          1. Applied rewrites64.8%

            \[\leadsto \frac{\pi \cdot \frac{\color{blue}{b}}{a \cdot b}}{\left(a + b\right) \cdot \left(b - a\right)} \cdot 0.5 \]
          2. Taylor expanded in a around 0

            \[\leadsto \frac{\pi \cdot \frac{b}{a \cdot b}}{\left(a + b\right) \cdot \color{blue}{b}} \cdot \frac{1}{2} \]
          3. Step-by-step derivation
            1. Applied rewrites93.7%

              \[\leadsto \frac{\pi \cdot \frac{b}{a \cdot b}}{\left(a + b\right) \cdot \color{blue}{b}} \cdot 0.5 \]
            2. Taylor expanded in a around 0

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

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

                \[\leadsto \frac{\frac{\pi}{a}}{\left(a + b\right) \cdot b} \cdot 0.5 \]
            4. Applied rewrites93.8%

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

            if 1.07999999999999999e76 < b

            1. Initial program 78.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. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. mult-flip-revN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. sub-negate-revN/A

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

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

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

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

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
              16. sub-negate-revN/A

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

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

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

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

              \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
            6. Taylor expanded in a around 0

              \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            7. Step-by-step derivation
              1. lower-PI.f6466.3

                \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            8. Applied rewrites66.3%

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

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

                \[\leadsto \frac{\pi}{\color{blue}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
              3. *-commutativeN/A

                \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b + b\right) \cdot a\right) \cdot \left(b - a\right)}} \]
              4. associate-/r*N/A

                \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + b\right) \cdot a}}{b - a}} \]
              5. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\frac{\pi}{\left(b + b\right) \cdot a}}{b - a}} \]
              6. lower-/.f6466.6

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

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

          Alternative 3: 99.6% accurate, 1.1× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \frac{\frac{\frac{b - a}{a \cdot b} \cdot \left(0.5 \cdot \pi\right)}{a + b}}{b - a} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (/ (/ (* (/ (- b a) (* a b)) (* 0.5 PI)) (+ a b)) (- b a)))
          assert(a < b);
          double code(double a, double b) {
          	return ((((b - a) / (a * b)) * (0.5 * ((double) M_PI))) / (a + b)) / (b - a);
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	return ((((b - a) / (a * b)) * (0.5 * Math.PI)) / (a + b)) / (b - a);
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	return ((((b - a) / (a * b)) * (0.5 * math.pi)) / (a + b)) / (b - a)
          
          a, b = sort([a, b])
          function code(a, b)
          	return Float64(Float64(Float64(Float64(Float64(b - a) / Float64(a * b)) * Float64(0.5 * pi)) / Float64(a + b)) / Float64(b - a))
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp = code(a, b)
          	tmp = ((((b - a) / (a * b)) * (0.5 * pi)) / (a + b)) / (b - a);
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := N[(N[(N[(N[(N[(b - a), $MachinePrecision] / N[(a * b), $MachinePrecision]), $MachinePrecision] * N[(0.5 * Pi), $MachinePrecision]), $MachinePrecision] / N[(a + b), $MachinePrecision]), $MachinePrecision] / N[(b - a), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \frac{\frac{\frac{b - a}{a \cdot b} \cdot \left(0.5 \cdot \pi\right)}{a + b}}{b - a}
          \end{array}
          
          Derivation
          1. Initial program 78.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. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. mult-flip-revN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. sub-negate-revN/A

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

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

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
            16. sub-negate-revN/A

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

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

          Alternative 4: 99.4% accurate, 1.1× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \frac{\frac{b - a}{a \cdot b}}{b - a} \cdot \left(0.5 \cdot \frac{\pi}{a + b}\right) \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (* (/ (/ (- b a) (* a b)) (- b a)) (* 0.5 (/ PI (+ a b)))))
          assert(a < b);
          double code(double a, double b) {
          	return (((b - a) / (a * b)) / (b - a)) * (0.5 * (((double) M_PI) / (a + b)));
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	return (((b - a) / (a * b)) / (b - a)) * (0.5 * (Math.PI / (a + b)));
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	return (((b - a) / (a * b)) / (b - a)) * (0.5 * (math.pi / (a + b)))
          
          a, b = sort([a, b])
          function code(a, b)
          	return Float64(Float64(Float64(Float64(b - a) / Float64(a * b)) / Float64(b - a)) * Float64(0.5 * Float64(pi / Float64(a + b))))
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp = code(a, b)
          	tmp = (((b - a) / (a * b)) / (b - a)) * (0.5 * (pi / (a + b)));
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := N[(N[(N[(N[(b - a), $MachinePrecision] / N[(a * b), $MachinePrecision]), $MachinePrecision] / N[(b - a), $MachinePrecision]), $MachinePrecision] * N[(0.5 * N[(Pi / N[(a + b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \frac{\frac{b - a}{a \cdot b}}{b - a} \cdot \left(0.5 \cdot \frac{\pi}{a + b}\right)
          \end{array}
          
          Derivation
          1. Initial program 78.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. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. mult-flip-revN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{2}}{b \cdot b - \color{blue}{a \cdot a}} \]
            9. lift-*.f64N/A

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\color{blue}{\left(b - a\right) \cdot \left(b + a\right)}} \]
            12. sub-negate-revN/A

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

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

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right) \cdot \left(b + a\right)} \]
            17. sub-negate-revN/A

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

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

          Alternative 5: 99.0% accurate, 1.2× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (/ (* (/ PI (+ a b)) (- b a)) (* (- b a) (* (+ b b) a))))
          assert(a < b);
          double code(double a, double b) {
          	return ((((double) M_PI) / (a + b)) * (b - a)) / ((b - a) * ((b + b) * a));
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	return ((Math.PI / (a + b)) * (b - a)) / ((b - a) * ((b + b) * a));
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	return ((math.pi / (a + b)) * (b - a)) / ((b - a) * ((b + b) * a))
          
          a, b = sort([a, b])
          function code(a, b)
          	return Float64(Float64(Float64(pi / Float64(a + b)) * Float64(b - a)) / Float64(Float64(b - a) * Float64(Float64(b + b) * a)))
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp = code(a, b)
          	tmp = ((pi / (a + b)) * (b - a)) / ((b - a) * ((b + b) * a));
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := N[(N[(N[(Pi / N[(a + b), $MachinePrecision]), $MachinePrecision] * N[(b - a), $MachinePrecision]), $MachinePrecision] / N[(N[(b - a), $MachinePrecision] * N[(N[(b + b), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}
          \end{array}
          
          Derivation
          1. Initial program 78.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. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. mult-flip-revN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. sub-negate-revN/A

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

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

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
            16. sub-negate-revN/A

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

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

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

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

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

          Alternative 6: 89.2% accurate, 1.6× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -3.8 \cdot 10^{-165}:\\ \;\;\;\;\frac{\pi \cdot \frac{-0.5}{a \cdot b}}{b - a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}\\ \end{array} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (if (<= a -3.8e-165)
             (/ (* PI (/ -0.5 (* a b))) (- b a))
             (/ PI (* (+ b b) (* (- b a) a)))))
          assert(a < b);
          double code(double a, double b) {
          	double tmp;
          	if (a <= -3.8e-165) {
          		tmp = (((double) M_PI) * (-0.5 / (a * b))) / (b - a);
          	} else {
          		tmp = ((double) M_PI) / ((b + b) * ((b - a) * a));
          	}
          	return tmp;
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	double tmp;
          	if (a <= -3.8e-165) {
          		tmp = (Math.PI * (-0.5 / (a * b))) / (b - a);
          	} else {
          		tmp = Math.PI / ((b + b) * ((b - a) * a));
          	}
          	return tmp;
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	tmp = 0
          	if a <= -3.8e-165:
          		tmp = (math.pi * (-0.5 / (a * b))) / (b - a)
          	else:
          		tmp = math.pi / ((b + b) * ((b - a) * a))
          	return tmp
          
          a, b = sort([a, b])
          function code(a, b)
          	tmp = 0.0
          	if (a <= -3.8e-165)
          		tmp = Float64(Float64(pi * Float64(-0.5 / Float64(a * b))) / Float64(b - a));
          	else
          		tmp = Float64(pi / Float64(Float64(b + b) * Float64(Float64(b - a) * a)));
          	end
          	return tmp
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp_2 = code(a, b)
          	tmp = 0.0;
          	if (a <= -3.8e-165)
          		tmp = (pi * (-0.5 / (a * b))) / (b - a);
          	else
          		tmp = pi / ((b + b) * ((b - a) * a));
          	end
          	tmp_2 = tmp;
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := If[LessEqual[a, -3.8e-165], N[(N[(Pi * N[(-0.5 / N[(a * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(b - a), $MachinePrecision]), $MachinePrecision], N[(Pi / N[(N[(b + b), $MachinePrecision] * N[(N[(b - a), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \begin{array}{l}
          \mathbf{if}\;a \leq -3.8 \cdot 10^{-165}:\\
          \;\;\;\;\frac{\pi \cdot \frac{-0.5}{a \cdot b}}{b - a}\\
          
          \mathbf{else}:\\
          \;\;\;\;\frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if a < -3.80000000000000018e-165

            1. Initial program 78.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. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. mult-flip-revN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. sub-negate-revN/A

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

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

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

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

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
              16. sub-negate-revN/A

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

              \[\leadsto \color{blue}{\frac{\frac{\frac{b - a}{a \cdot b} \cdot \left(0.5 \cdot \pi\right)}{a + b}}{b - a}} \]
            4. Taylor expanded in a around inf

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

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

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

                \[\leadsto \frac{\frac{-1}{2} \cdot \frac{\pi}{\color{blue}{a} \cdot b}}{b - a} \]
              4. lower-*.f6467.1

                \[\leadsto \frac{-0.5 \cdot \frac{\pi}{a \cdot \color{blue}{b}}}{b - a} \]
            6. Applied rewrites67.1%

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

                \[\leadsto \frac{\frac{-1}{2} \cdot \color{blue}{\frac{\pi}{a \cdot b}}}{b - a} \]
              2. lift-/.f64N/A

                \[\leadsto \frac{\frac{-1}{2} \cdot \frac{\pi}{\color{blue}{a \cdot b}}}{b - a} \]
              3. associate-*r/N/A

                \[\leadsto \frac{\frac{\frac{-1}{2} \cdot \pi}{\color{blue}{a \cdot b}}}{b - a} \]
              4. lift-*.f64N/A

                \[\leadsto \frac{\frac{\frac{-1}{2} \cdot \pi}{a \cdot \color{blue}{b}}}{b - a} \]
              5. *-commutativeN/A

                \[\leadsto \frac{\frac{\frac{-1}{2} \cdot \pi}{b \cdot \color{blue}{a}}}{b - a} \]
              6. associate-/r*N/A

                \[\leadsto \frac{\frac{\frac{\frac{-1}{2} \cdot \pi}{b}}{\color{blue}{a}}}{b - a} \]
              7. lower-/.f64N/A

                \[\leadsto \frac{\frac{\frac{\frac{-1}{2} \cdot \pi}{b}}{\color{blue}{a}}}{b - a} \]
              8. lower-/.f64N/A

                \[\leadsto \frac{\frac{\frac{\frac{-1}{2} \cdot \pi}{b}}{a}}{b - a} \]
              9. lower-*.f6467.1

                \[\leadsto \frac{\frac{\frac{-0.5 \cdot \pi}{b}}{a}}{b - a} \]
            8. Applied rewrites67.1%

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

                \[\leadsto \frac{\frac{\frac{\frac{-1}{2} \cdot \pi}{b}}{\color{blue}{a}}}{b - a} \]
              2. lift-/.f64N/A

                \[\leadsto \frac{\frac{\frac{\frac{-1}{2} \cdot \pi}{b}}{a}}{b - a} \]
              3. associate-/l/N/A

                \[\leadsto \frac{\frac{\frac{-1}{2} \cdot \pi}{\color{blue}{b \cdot a}}}{b - a} \]
              4. lift-*.f64N/A

                \[\leadsto \frac{\frac{\frac{-1}{2} \cdot \pi}{\color{blue}{b} \cdot a}}{b - a} \]
              5. *-commutativeN/A

                \[\leadsto \frac{\frac{\pi \cdot \frac{-1}{2}}{\color{blue}{b} \cdot a}}{b - a} \]
              6. *-commutativeN/A

                \[\leadsto \frac{\frac{\pi \cdot \frac{-1}{2}}{a \cdot \color{blue}{b}}}{b - a} \]
              7. lift-*.f64N/A

                \[\leadsto \frac{\frac{\pi \cdot \frac{-1}{2}}{a \cdot \color{blue}{b}}}{b - a} \]
              8. associate-/l*N/A

                \[\leadsto \frac{\pi \cdot \color{blue}{\frac{\frac{-1}{2}}{a \cdot b}}}{b - a} \]
              9. lower-*.f64N/A

                \[\leadsto \frac{\pi \cdot \color{blue}{\frac{\frac{-1}{2}}{a \cdot b}}}{b - a} \]
              10. lower-/.f6467.1

                \[\leadsto \frac{\pi \cdot \frac{-0.5}{\color{blue}{a \cdot b}}}{b - a} \]
            10. Applied rewrites67.1%

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

            if -3.80000000000000018e-165 < a

            1. Initial program 78.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. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. mult-flip-revN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. sub-negate-revN/A

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

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

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

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

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
              16. sub-negate-revN/A

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

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

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

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

              \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
            6. Taylor expanded in a around 0

              \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            7. Step-by-step derivation
              1. lower-PI.f6466.3

                \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            8. Applied rewrites66.3%

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

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

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

                \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b + b\right) \cdot a\right)} \cdot \left(b - a\right)} \]
              4. associate-*l*N/A

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

                \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
              6. lower-*.f64N/A

                \[\leadsto \frac{\pi}{\color{blue}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}} \]
              7. lower-*.f6466.4

                \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
            10. Applied rewrites66.4%

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

          Alternative 7: 89.2% accurate, 1.6× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -3.8 \cdot 10^{-165}:\\ \;\;\;\;\frac{-0.5 \cdot \frac{\pi}{a \cdot b}}{b - a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}\\ \end{array} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (if (<= a -3.8e-165)
             (/ (* -0.5 (/ PI (* a b))) (- b a))
             (/ PI (* (+ b b) (* (- b a) a)))))
          assert(a < b);
          double code(double a, double b) {
          	double tmp;
          	if (a <= -3.8e-165) {
          		tmp = (-0.5 * (((double) M_PI) / (a * b))) / (b - a);
          	} else {
          		tmp = ((double) M_PI) / ((b + b) * ((b - a) * a));
          	}
          	return tmp;
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	double tmp;
          	if (a <= -3.8e-165) {
          		tmp = (-0.5 * (Math.PI / (a * b))) / (b - a);
          	} else {
          		tmp = Math.PI / ((b + b) * ((b - a) * a));
          	}
          	return tmp;
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	tmp = 0
          	if a <= -3.8e-165:
          		tmp = (-0.5 * (math.pi / (a * b))) / (b - a)
          	else:
          		tmp = math.pi / ((b + b) * ((b - a) * a))
          	return tmp
          
          a, b = sort([a, b])
          function code(a, b)
          	tmp = 0.0
          	if (a <= -3.8e-165)
          		tmp = Float64(Float64(-0.5 * Float64(pi / Float64(a * b))) / Float64(b - a));
          	else
          		tmp = Float64(pi / Float64(Float64(b + b) * Float64(Float64(b - a) * a)));
          	end
          	return tmp
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp_2 = code(a, b)
          	tmp = 0.0;
          	if (a <= -3.8e-165)
          		tmp = (-0.5 * (pi / (a * b))) / (b - a);
          	else
          		tmp = pi / ((b + b) * ((b - a) * a));
          	end
          	tmp_2 = tmp;
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := If[LessEqual[a, -3.8e-165], N[(N[(-0.5 * N[(Pi / N[(a * b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(b - a), $MachinePrecision]), $MachinePrecision], N[(Pi / N[(N[(b + b), $MachinePrecision] * N[(N[(b - a), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \begin{array}{l}
          \mathbf{if}\;a \leq -3.8 \cdot 10^{-165}:\\
          \;\;\;\;\frac{-0.5 \cdot \frac{\pi}{a \cdot b}}{b - a}\\
          
          \mathbf{else}:\\
          \;\;\;\;\frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if a < -3.80000000000000018e-165

            1. Initial program 78.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. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. mult-flip-revN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. sub-negate-revN/A

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

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

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

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

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
              16. sub-negate-revN/A

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

              \[\leadsto \color{blue}{\frac{\frac{\frac{b - a}{a \cdot b} \cdot \left(0.5 \cdot \pi\right)}{a + b}}{b - a}} \]
            4. Taylor expanded in a around inf

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

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

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

                \[\leadsto \frac{\frac{-1}{2} \cdot \frac{\pi}{\color{blue}{a} \cdot b}}{b - a} \]
              4. lower-*.f6467.1

                \[\leadsto \frac{-0.5 \cdot \frac{\pi}{a \cdot \color{blue}{b}}}{b - a} \]
            6. Applied rewrites67.1%

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

            if -3.80000000000000018e-165 < a

            1. Initial program 78.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. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
              5. mult-flip-revN/A

                \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
              7. lift--.f64N/A

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
              11. sub-negate-revN/A

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

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

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

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

                \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
              16. sub-negate-revN/A

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

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

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

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

              \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
            6. Taylor expanded in a around 0

              \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            7. Step-by-step derivation
              1. lower-PI.f6466.3

                \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
            8. Applied rewrites66.3%

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

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

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

                \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b + b\right) \cdot a\right)} \cdot \left(b - a\right)} \]
              4. associate-*l*N/A

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

                \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
              6. lower-*.f64N/A

                \[\leadsto \frac{\pi}{\color{blue}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}} \]
              7. lower-*.f6466.4

                \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
            10. Applied rewrites66.4%

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

          Alternative 8: 66.4% accurate, 2.0× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b) :precision binary64 (/ PI (* (+ b b) (* (- b a) a))))
          assert(a < b);
          double code(double a, double b) {
          	return ((double) M_PI) / ((b + b) * ((b - a) * a));
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	return Math.PI / ((b + b) * ((b - a) * a));
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	return math.pi / ((b + b) * ((b - a) * a))
          
          a, b = sort([a, b])
          function code(a, b)
          	return Float64(pi / Float64(Float64(b + b) * Float64(Float64(b - a) * a)))
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp = code(a, b)
          	tmp = pi / ((b + b) * ((b - a) * a));
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := N[(Pi / N[(N[(b + b), $MachinePrecision] * N[(N[(b - a), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \frac{\pi}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}
          \end{array}
          
          Derivation
          1. Initial program 78.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. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. mult-flip-revN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. sub-negate-revN/A

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

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

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
            16. sub-negate-revN/A

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

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

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

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

            \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
          6. Taylor expanded in a around 0

            \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
          7. Step-by-step derivation
            1. lower-PI.f6466.3

              \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
          8. Applied rewrites66.3%

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

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

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

              \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b + b\right) \cdot a\right)} \cdot \left(b - a\right)} \]
            4. associate-*l*N/A

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

              \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
            6. lower-*.f64N/A

              \[\leadsto \frac{\pi}{\color{blue}{\left(b + b\right) \cdot \left(\left(b - a\right) \cdot a\right)}} \]
            7. lower-*.f6466.4

              \[\leadsto \frac{\pi}{\left(b + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot a\right)}} \]
          10. Applied rewrites66.4%

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

          Alternative 9: 60.7% accurate, 2.0× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \frac{\pi}{\left(\left(b + b\right) \cdot \left(b - a\right)\right) \cdot a} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b) :precision binary64 (/ PI (* (* (+ b b) (- b a)) a)))
          assert(a < b);
          double code(double a, double b) {
          	return ((double) M_PI) / (((b + b) * (b - a)) * a);
          }
          
          assert a < b;
          public static double code(double a, double b) {
          	return Math.PI / (((b + b) * (b - a)) * a);
          }
          
          [a, b] = sort([a, b])
          def code(a, b):
          	return math.pi / (((b + b) * (b - a)) * a)
          
          a, b = sort([a, b])
          function code(a, b)
          	return Float64(pi / Float64(Float64(Float64(b + b) * Float64(b - a)) * a))
          end
          
          a, b = num2cell(sort([a, b])){:}
          function tmp = code(a, b)
          	tmp = pi / (((b + b) * (b - a)) * a);
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := N[(Pi / N[(N[(N[(b + b), $MachinePrecision] * N[(b - a), $MachinePrecision]), $MachinePrecision] * a), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \frac{\pi}{\left(\left(b + b\right) \cdot \left(b - a\right)\right) \cdot a}
          \end{array}
          
          Derivation
          1. Initial program 78.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. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2} \cdot \color{blue}{\frac{1}{b \cdot b - a \cdot a}}\right) \]
            5. mult-flip-revN/A

              \[\leadsto \left(\frac{1}{a} - \frac{1}{b}\right) \cdot \color{blue}{\frac{\frac{\pi}{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{\pi}{2}}{b \cdot b - a \cdot a}} \]
            7. lift--.f64N/A

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{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{\pi}{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{\pi}{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{\pi}{2}}{\color{blue}{\left(b + a\right) \cdot \left(b - a\right)}} \]
            11. sub-negate-revN/A

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

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

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

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

              \[\leadsto \frac{\left(\frac{1}{a} - \frac{1}{b}\right) \cdot \frac{\pi}{2}}{\left(b + a\right) \cdot \left(\mathsf{neg}\left(\left(a \cdot 1 - \color{blue}{1 \cdot b}\right)\right)\right)} \]
            16. sub-negate-revN/A

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

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

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

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

            \[\leadsto \color{blue}{\frac{\frac{\pi}{a + b} \cdot \left(b - a\right)}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)}} \]
          6. Taylor expanded in a around 0

            \[\leadsto \frac{\color{blue}{\mathsf{PI}\left(\right)}}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
          7. Step-by-step derivation
            1. lower-PI.f6466.3

              \[\leadsto \frac{\pi}{\left(b - a\right) \cdot \left(\left(b + b\right) \cdot a\right)} \]
          8. Applied rewrites66.3%

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

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

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

              \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b - a\right) \cdot \left(b + b\right)\right) \cdot a}} \]
            4. lower-*.f64N/A

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

              \[\leadsto \frac{\pi}{\color{blue}{\left(\left(b + b\right) \cdot \left(b - a\right)\right)} \cdot a} \]
            6. lower-*.f6460.7

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

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

          Reproduce

          ?
          herbie shell --seed 2025156 
          (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))))