Eccentricity of an ellipse

Percentage Accurate: 77.2% → 100.0%
Time: 4.1s
Alternatives: 3
Speedup: 42.0×

Specification

?
\[\left(0 \leq b \land b \leq a\right) \land a \leq 1\]
\[\begin{array}{l} \\ \sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|} \end{array} \]
(FPCore (a b)
 :precision binary64
 (sqrt (fabs (/ (- (* a a) (* b b)) (* a a)))))
double code(double a, double b) {
	return sqrt(fabs((((a * a) - (b * b)) / (a * a))));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = sqrt(abs((((a * a) - (b * b)) / (a * a))))
end function
public static double code(double a, double b) {
	return Math.sqrt(Math.abs((((a * a) - (b * b)) / (a * a))));
}
def code(a, b):
	return math.sqrt(math.fabs((((a * a) - (b * b)) / (a * a))))
function code(a, b)
	return sqrt(abs(Float64(Float64(Float64(a * a) - Float64(b * b)) / Float64(a * a))))
end
function tmp = code(a, b)
	tmp = sqrt(abs((((a * a) - (b * b)) / (a * a))));
end
code[a_, b_] := N[Sqrt[N[Abs[N[(N[(N[(a * a), $MachinePrecision] - N[(b * b), $MachinePrecision]), $MachinePrecision] / N[(a * a), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\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 3 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: 77.2% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|} \end{array} \]
(FPCore (a b)
 :precision binary64
 (sqrt (fabs (/ (- (* a a) (* b b)) (* a a)))))
double code(double a, double b) {
	return sqrt(fabs((((a * a) - (b * b)) / (a * a))));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = sqrt(abs((((a * a) - (b * b)) / (a * a))))
end function
public static double code(double a, double b) {
	return Math.sqrt(Math.abs((((a * a) - (b * b)) / (a * a))));
}
def code(a, b):
	return math.sqrt(math.fabs((((a * a) - (b * b)) / (a * a))))
function code(a, b)
	return sqrt(abs(Float64(Float64(Float64(a * a) - Float64(b * b)) / Float64(a * a))))
end
function tmp = code(a, b)
	tmp = sqrt(abs((((a * a) - (b * b)) / (a * a))));
end
code[a_, b_] := N[Sqrt[N[Abs[N[(N[(N[(a * a), $MachinePrecision] - N[(b * b), $MachinePrecision]), $MachinePrecision] / N[(a * a), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|}
\end{array}

Alternative 1: 100.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{\left|\mathsf{fma}\left(\frac{\frac{b}{a}}{a}, b, -1\right)\right|} \end{array} \]
(FPCore (a b) :precision binary64 (sqrt (fabs (fma (/ (/ b a) a) b -1.0))))
double code(double a, double b) {
	return sqrt(fabs(fma(((b / a) / a), b, -1.0)));
}
function code(a, b)
	return sqrt(abs(fma(Float64(Float64(b / a) / a), b, -1.0)))
end
code[a_, b_] := N[Sqrt[N[Abs[N[(N[(N[(b / a), $MachinePrecision] / a), $MachinePrecision] * b + -1.0), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\sqrt{\left|\mathsf{fma}\left(\frac{\frac{b}{a}}{a}, b, -1\right)\right|}
\end{array}
Derivation
  1. Initial program 83.4%

    \[\sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|} \]
  2. Add Preprocessing
  3. Taylor expanded in a around 0

    \[\leadsto \sqrt{\color{blue}{\left|\frac{{a}^{2} - {b}^{2}}{{a}^{2}}\right|}} \]
  4. Step-by-step derivation
    1. fabs-negN/A

      \[\leadsto \sqrt{\color{blue}{\left|\mathsf{neg}\left(\frac{{a}^{2} - {b}^{2}}{{a}^{2}}\right)\right|}} \]
    2. lower-fabs.f64N/A

      \[\leadsto \sqrt{\color{blue}{\left|\mathsf{neg}\left(\frac{{a}^{2} - {b}^{2}}{{a}^{2}}\right)\right|}} \]
    3. div-subN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\color{blue}{\left(\frac{{a}^{2}}{{a}^{2}} - \frac{{b}^{2}}{{a}^{2}}\right)}\right)\right|} \]
    4. *-inversesN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\left(\color{blue}{1} - \frac{{b}^{2}}{{a}^{2}}\right)\right)\right|} \]
    5. *-lft-identityN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\left(1 - \color{blue}{1 \cdot \frac{{b}^{2}}{{a}^{2}}}\right)\right)\right|} \]
    6. metadata-evalN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\left(1 - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot \frac{{b}^{2}}{{a}^{2}}\right)\right)\right|} \]
    7. fp-cancel-sign-sub-invN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\color{blue}{\left(1 + -1 \cdot \frac{{b}^{2}}{{a}^{2}}\right)}\right)\right|} \]
    8. +-commutativeN/A

      \[\leadsto \sqrt{\left|\mathsf{neg}\left(\color{blue}{\left(-1 \cdot \frac{{b}^{2}}{{a}^{2}} + 1\right)}\right)\right|} \]
    9. distribute-neg-inN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left(\mathsf{neg}\left(-1 \cdot \frac{{b}^{2}}{{a}^{2}}\right)\right) + \left(\mathsf{neg}\left(1\right)\right)}\right|} \]
    10. distribute-lft-neg-inN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left(\mathsf{neg}\left(-1\right)\right) \cdot \frac{{b}^{2}}{{a}^{2}}} + \left(\mathsf{neg}\left(1\right)\right)\right|} \]
    11. metadata-evalN/A

      \[\leadsto \sqrt{\left|\color{blue}{1} \cdot \frac{{b}^{2}}{{a}^{2}} + \left(\mathsf{neg}\left(1\right)\right)\right|} \]
    12. metadata-evalN/A

      \[\leadsto \sqrt{\left|1 \cdot \frac{{b}^{2}}{{a}^{2}} + \color{blue}{-1}\right|} \]
    13. *-lft-identityN/A

      \[\leadsto \sqrt{\left|\color{blue}{\frac{{b}^{2}}{{a}^{2}}} + -1\right|} \]
    14. unpow2N/A

      \[\leadsto \sqrt{\left|\frac{\color{blue}{b \cdot b}}{{a}^{2}} + -1\right|} \]
    15. associate-/l*N/A

      \[\leadsto \sqrt{\left|\color{blue}{b \cdot \frac{b}{{a}^{2}}} + -1\right|} \]
    16. *-commutativeN/A

      \[\leadsto \sqrt{\left|\color{blue}{\frac{b}{{a}^{2}} \cdot b} + -1\right|} \]
    17. lower-fma.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\mathsf{fma}\left(\frac{b}{{a}^{2}}, b, -1\right)}\right|} \]
  5. Applied rewrites100.0%

    \[\leadsto \sqrt{\color{blue}{\left|\mathsf{fma}\left(\frac{\frac{b}{a}}{a}, b, -1\right)\right|}} \]
  6. Add Preprocessing

Alternative 2: 99.0% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(-0.5 \cdot b, \frac{\frac{b}{a}}{a}, 1\right) \end{array} \]
(FPCore (a b) :precision binary64 (fma (* -0.5 b) (/ (/ b a) a) 1.0))
double code(double a, double b) {
	return fma((-0.5 * b), ((b / a) / a), 1.0);
}
function code(a, b)
	return fma(Float64(-0.5 * b), Float64(Float64(b / a) / a), 1.0)
end
code[a_, b_] := N[(N[(-0.5 * b), $MachinePrecision] * N[(N[(b / a), $MachinePrecision] / a), $MachinePrecision] + 1.0), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(-0.5 \cdot b, \frac{\frac{b}{a}}{a}, 1\right)
\end{array}
Derivation
  1. Initial program 83.4%

    \[\sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. rem-square-sqrtN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a}} \cdot \sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a}}}\right|} \]
    2. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a} \cdot \frac{a \cdot a - b \cdot b}{a \cdot a}}}\right|} \]
    3. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|}\right|} \]
    4. lift-/.f64N/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{\frac{a \cdot a - b \cdot b}{a \cdot a}}\right|\right|} \]
    5. fabs-divN/A

      \[\leadsto \sqrt{\left|\color{blue}{\frac{\left|a \cdot a - b \cdot b\right|}{\left|a \cdot a\right|}}\right|} \]
    6. lift--.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{a \cdot a - b \cdot b}\right|}{\left|a \cdot a\right|}\right|} \]
    7. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{a \cdot a} - b \cdot b\right|}{\left|a \cdot a\right|}\right|} \]
    8. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|a \cdot a - \color{blue}{b \cdot b}\right|}{\left|a \cdot a\right|}\right|} \]
    9. difference-of-squaresN/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{\left(a + b\right) \cdot \left(a - b\right)}\right|}{\left|a \cdot a\right|}\right|} \]
    10. fabs-mulN/A

      \[\leadsto \sqrt{\left|\frac{\color{blue}{\left|a + b\right| \cdot \left|a - b\right|}}{\left|a \cdot a\right|}\right|} \]
    11. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{\sqrt{\left(a \cdot a\right) \cdot \left(a \cdot a\right)}}}\right|} \]
    12. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{\sqrt{a \cdot a} \cdot \sqrt{a \cdot a}}}\right|} \]
    13. rem-square-sqrtN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{a \cdot a}}\right|} \]
    14. associate-/l*N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right| \cdot \frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    15. lower-*.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right| \cdot \frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    16. lower-fabs.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right|} \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    17. +-commutativeN/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{b + a}\right| \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    18. lower-+.f64N/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{b + a}\right| \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    19. lower-/.f64N/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \color{blue}{\frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    20. fabs-subN/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\color{blue}{\left|b - a\right|}}{a \cdot a}\right|} \]
    21. lower-fabs.f64N/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\color{blue}{\left|b - a\right|}}{a \cdot a}\right|} \]
    22. lower--.f6482.8

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\left|\color{blue}{b - a}\right|}{a \cdot a}\right|} \]
  4. Applied rewrites82.8%

    \[\leadsto \sqrt{\left|\color{blue}{\left|b + a\right| \cdot \frac{\left|b - a\right|}{a \cdot a}}\right|} \]
  5. Step-by-step derivation
    1. lift-fabs.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|b + a\right|} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    2. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\left(b + a\right) \cdot \left(b + a\right)}} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    3. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left(\sqrt{b + a} \cdot \sqrt{b + a}\right)} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    4. rem-square-sqrt82.8

      \[\leadsto \sqrt{\left|\color{blue}{\left(b + a\right)} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
  6. Applied rewrites82.8%

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

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

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

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

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

      \[\leadsto \sqrt{\left|\color{blue}{\frac{\left(b + a\right) \cdot \left|b - a\right|}{a \cdot a}}\right|} \]
    6. fabs-divN/A

      \[\leadsto \sqrt{\color{blue}{\frac{\left|\left(b + a\right) \cdot \left|b - a\right|\right|}{\left|a \cdot a\right|}}} \]
    7. fabs-mulN/A

      \[\leadsto \sqrt{\frac{\color{blue}{\left|b + a\right| \cdot \left|\left|b - a\right|\right|}}{\left|a \cdot a\right|}} \]
    8. lift-fabs.f64N/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \left|\color{blue}{\left|b - a\right|}\right|}{\left|a \cdot a\right|}} \]
    9. fabs-fabsN/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \color{blue}{\left|b - a\right|}}{\left|a \cdot a\right|}} \]
    10. lift--.f64N/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \left|\color{blue}{b - a}\right|}{\left|a \cdot a\right|}} \]
    11. fabs-subN/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \color{blue}{\left|a - b\right|}}{\left|a \cdot a\right|}} \]
    12. fabs-mulN/A

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

      \[\leadsto \sqrt{\frac{\left|\color{blue}{\left(b + a\right)} \cdot \left(a - b\right)\right|}{\left|a \cdot a\right|}} \]
    14. +-commutativeN/A

      \[\leadsto \sqrt{\frac{\left|\color{blue}{\left(a + b\right)} \cdot \left(a - b\right)\right|}{\left|a \cdot a\right|}} \]
    15. difference-of-squaresN/A

      \[\leadsto \sqrt{\frac{\left|\color{blue}{a \cdot a - b \cdot b}\right|}{\left|a \cdot a\right|}} \]
    16. fabs-divN/A

      \[\leadsto \sqrt{\color{blue}{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|}} \]
    17. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{a \cdot a - b \cdot b}{\color{blue}{a \cdot a}}\right|} \]
  8. Applied rewrites83.1%

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

    \[\leadsto \color{blue}{1 + b \cdot \left(\frac{-1}{2} \cdot \frac{b \cdot \left(1 + \frac{1}{4} \cdot \frac{{\left(a + -1 \cdot a\right)}^{2}}{{a}^{2}}\right)}{{a}^{2}} + \frac{1}{2} \cdot \frac{a + -1 \cdot a}{{a}^{2}}\right)} \]
  10. Applied rewrites100.0%

    \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5 \cdot b, \frac{\frac{b}{a}}{a}, 1\right)} \]
  11. Add Preprocessing

Alternative 3: 97.9% accurate, 42.0× speedup?

\[\begin{array}{l} \\ 1 \end{array} \]
(FPCore (a b) :precision binary64 1.0)
double code(double a, double b) {
	return 1.0;
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = 1.0d0
end function
public static double code(double a, double b) {
	return 1.0;
}
def code(a, b):
	return 1.0
function code(a, b)
	return 1.0
end
function tmp = code(a, b)
	tmp = 1.0;
end
code[a_, b_] := 1.0
\begin{array}{l}

\\
1
\end{array}
Derivation
  1. Initial program 83.4%

    \[\sqrt{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. rem-square-sqrtN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a}} \cdot \sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a}}}\right|} \]
    2. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\frac{a \cdot a - b \cdot b}{a \cdot a} \cdot \frac{a \cdot a - b \cdot b}{a \cdot a}}}\right|} \]
    3. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|}\right|} \]
    4. lift-/.f64N/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{\frac{a \cdot a - b \cdot b}{a \cdot a}}\right|\right|} \]
    5. fabs-divN/A

      \[\leadsto \sqrt{\left|\color{blue}{\frac{\left|a \cdot a - b \cdot b\right|}{\left|a \cdot a\right|}}\right|} \]
    6. lift--.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{a \cdot a - b \cdot b}\right|}{\left|a \cdot a\right|}\right|} \]
    7. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{a \cdot a} - b \cdot b\right|}{\left|a \cdot a\right|}\right|} \]
    8. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{\left|a \cdot a - \color{blue}{b \cdot b}\right|}{\left|a \cdot a\right|}\right|} \]
    9. difference-of-squaresN/A

      \[\leadsto \sqrt{\left|\frac{\left|\color{blue}{\left(a + b\right) \cdot \left(a - b\right)}\right|}{\left|a \cdot a\right|}\right|} \]
    10. fabs-mulN/A

      \[\leadsto \sqrt{\left|\frac{\color{blue}{\left|a + b\right| \cdot \left|a - b\right|}}{\left|a \cdot a\right|}\right|} \]
    11. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{\sqrt{\left(a \cdot a\right) \cdot \left(a \cdot a\right)}}}\right|} \]
    12. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{\sqrt{a \cdot a} \cdot \sqrt{a \cdot a}}}\right|} \]
    13. rem-square-sqrtN/A

      \[\leadsto \sqrt{\left|\frac{\left|a + b\right| \cdot \left|a - b\right|}{\color{blue}{a \cdot a}}\right|} \]
    14. associate-/l*N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right| \cdot \frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    15. lower-*.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right| \cdot \frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    16. lower-fabs.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|a + b\right|} \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    17. +-commutativeN/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{b + a}\right| \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    18. lower-+.f64N/A

      \[\leadsto \sqrt{\left|\left|\color{blue}{b + a}\right| \cdot \frac{\left|a - b\right|}{a \cdot a}\right|} \]
    19. lower-/.f64N/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \color{blue}{\frac{\left|a - b\right|}{a \cdot a}}\right|} \]
    20. fabs-subN/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\color{blue}{\left|b - a\right|}}{a \cdot a}\right|} \]
    21. lower-fabs.f64N/A

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\color{blue}{\left|b - a\right|}}{a \cdot a}\right|} \]
    22. lower--.f6482.8

      \[\leadsto \sqrt{\left|\left|b + a\right| \cdot \frac{\left|\color{blue}{b - a}\right|}{a \cdot a}\right|} \]
  4. Applied rewrites82.8%

    \[\leadsto \sqrt{\left|\color{blue}{\left|b + a\right| \cdot \frac{\left|b - a\right|}{a \cdot a}}\right|} \]
  5. Step-by-step derivation
    1. lift-fabs.f64N/A

      \[\leadsto \sqrt{\left|\color{blue}{\left|b + a\right|} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    2. rem-sqrt-square-revN/A

      \[\leadsto \sqrt{\left|\color{blue}{\sqrt{\left(b + a\right) \cdot \left(b + a\right)}} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    3. sqrt-prodN/A

      \[\leadsto \sqrt{\left|\color{blue}{\left(\sqrt{b + a} \cdot \sqrt{b + a}\right)} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
    4. rem-square-sqrt82.8

      \[\leadsto \sqrt{\left|\color{blue}{\left(b + a\right)} \cdot \frac{\left|b - a\right|}{a \cdot a}\right|} \]
  6. Applied rewrites82.8%

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

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

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

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

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

      \[\leadsto \sqrt{\left|\color{blue}{\frac{\left(b + a\right) \cdot \left|b - a\right|}{a \cdot a}}\right|} \]
    6. fabs-divN/A

      \[\leadsto \sqrt{\color{blue}{\frac{\left|\left(b + a\right) \cdot \left|b - a\right|\right|}{\left|a \cdot a\right|}}} \]
    7. fabs-mulN/A

      \[\leadsto \sqrt{\frac{\color{blue}{\left|b + a\right| \cdot \left|\left|b - a\right|\right|}}{\left|a \cdot a\right|}} \]
    8. lift-fabs.f64N/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \left|\color{blue}{\left|b - a\right|}\right|}{\left|a \cdot a\right|}} \]
    9. fabs-fabsN/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \color{blue}{\left|b - a\right|}}{\left|a \cdot a\right|}} \]
    10. lift--.f64N/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \left|\color{blue}{b - a}\right|}{\left|a \cdot a\right|}} \]
    11. fabs-subN/A

      \[\leadsto \sqrt{\frac{\left|b + a\right| \cdot \color{blue}{\left|a - b\right|}}{\left|a \cdot a\right|}} \]
    12. fabs-mulN/A

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

      \[\leadsto \sqrt{\frac{\left|\color{blue}{\left(b + a\right)} \cdot \left(a - b\right)\right|}{\left|a \cdot a\right|}} \]
    14. +-commutativeN/A

      \[\leadsto \sqrt{\frac{\left|\color{blue}{\left(a + b\right)} \cdot \left(a - b\right)\right|}{\left|a \cdot a\right|}} \]
    15. difference-of-squaresN/A

      \[\leadsto \sqrt{\frac{\left|\color{blue}{a \cdot a - b \cdot b}\right|}{\left|a \cdot a\right|}} \]
    16. fabs-divN/A

      \[\leadsto \sqrt{\color{blue}{\left|\frac{a \cdot a - b \cdot b}{a \cdot a}\right|}} \]
    17. lift-*.f64N/A

      \[\leadsto \sqrt{\left|\frac{a \cdot a - b \cdot b}{\color{blue}{a \cdot a}}\right|} \]
  8. Applied rewrites83.1%

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

    \[\leadsto \color{blue}{1} \]
  10. Step-by-step derivation
    1. Applied rewrites99.3%

      \[\leadsto \color{blue}{1} \]
    2. Add Preprocessing

    Reproduce

    ?
    herbie shell --seed 2024332 
    (FPCore (a b)
      :name "Eccentricity of an ellipse"
      :precision binary64
      :pre (and (and (<= 0.0 b) (<= b a)) (<= a 1.0))
      (sqrt (fabs (/ (- (* a a) (* b b)) (* a a)))))