\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le 8.563796406084569868589291353255847362523 \cdot 10^{122}:\\ \;\;\;\;\mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, \left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right) \cdot \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}\right) + \mathsf{fma}\left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{\left(\left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}\\ \end{array}\]

\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}

↓

\begin{array}{l}
\mathbf{if}\;x \le 8.563796406084569868589291353255847362523 \cdot 10^{122}:\\
\;\;\;\;\mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, \left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right) \cdot \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}\right) + \mathsf{fma}\left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt[3]{\left(\left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}\\

\end{array}

double f(double x) {
        double r6664690 = 1.0;
        double r6664691 = x;
        double r6664692 = sqrt(r6664691);
        double r6664693 = r6664690 / r6664692;
        double r6664694 = r6664691 + r6664690;
        double r6664695 = sqrt(r6664694);
        double r6664696 = r6664690 / r6664695;
        double r6664697 = r6664693 - r6664696;
        return r6664697;
}

↓

double f(double x) {
        double r6664698 = x;
        double r6664699 = 8.56379640608457e+122;
        bool r6664700 = r6664698 <= r6664699;
        double r6664701 = 1.0;
        double r6664702 = 1.0;
        double r6664703 = sqrt(r6664698);
        double r6664704 = r6664702 / r6664703;
        double r6664705 = r6664698 * r6664698;
        double r6664706 = r6664702 * r6664702;
        double r6664707 = r6664702 * r6664698;
        double r6664708 = r6664706 - r6664707;
        double r6664709 = r6664705 + r6664708;
        double r6664710 = sqrt(r6664709);
        double r6664711 = -r6664710;
        double r6664712 = 3.0;
        double r6664713 = pow(r6664698, r6664712);
        double r6664714 = pow(r6664702, r6664712);
        double r6664715 = r6664713 + r6664714;
        double r6664716 = sqrt(r6664715);
        double r6664717 = r6664702 / r6664716;
        double r6664718 = r6664711 * r6664717;
        double r6664719 = fma(r6664701, r6664704, r6664718);
        double r6664720 = r6664717 * r6664710;
        double r6664721 = fma(r6664711, r6664717, r6664720);
        double r6664722 = r6664719 + r6664721;
        double r6664723 = r6664698 + r6664702;
        double r6664724 = sqrt(r6664723);
        double r6664725 = r6664702 / r6664724;
        double r6664726 = r6664704 - r6664725;
        double r6664727 = r6664726 * r6664726;
        double r6664728 = r6664727 * r6664726;
        double r6664729 = cbrt(r6664728);
        double r6664730 = r6664700 ? r6664722 : r6664729;
        return r6664730;
}

Original	20.0
Target	0.8
Herbie	19.9

Derivation

Split input into 2 regimes
if x < 8.56379640608457e+122
1. Initial program 16.6
  \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
2. Using strategy rm
3. Applied flip3-+16.6
  \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\sqrt{\color{blue}{\frac{{x}^{3} + {1}^{3}}{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}}}\]
4. Applied sqrt-div16.6
  \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\color{blue}{\frac{\sqrt{{x}^{3} + {1}^{3}}}{\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}}}\]
5. Applied associate-/r/16.6
  \[\leadsto \frac{1}{\sqrt{x}} - \color{blue}{\frac{1}{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}}\]
6. Applied *-un-lft-identity16.6
  \[\leadsto \color{blue}{1 \cdot \frac{1}{\sqrt{x}}} - \frac{1}{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}\]
7. Applied prod-diff16.5
  \[\leadsto \color{blue}{\mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, -\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)} \cdot \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}\right) + \mathsf{fma}\left(-\sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}, \sqrt{x \cdot x + \left(1 \cdot 1 - x \cdot 1\right)} \cdot \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}\right)}\]
if 8.56379640608457e+122 < x
1. Initial program 28.2
  \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
2. Using strategy rm
3. Applied add-cbrt-cube28.2
  \[\leadsto \color{blue}{\sqrt[3]{\left(\left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}}\]
Recombined 2 regimes into one program.
Final simplification19.9
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le 8.563796406084569868589291353255847362523 \cdot 10^{122}:\\ \;\;\;\;\mathsf{fma}\left(1, \frac{1}{\sqrt{x}}, \left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right) \cdot \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}\right) + \mathsf{fma}\left(-\sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}}, \frac{1}{\sqrt{{x}^{3} + {1}^{3}}} \cdot \sqrt{x \cdot x + \left(1 \cdot 1 - 1 \cdot x\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{\left(\left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)\right) \cdot \left(\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\right)}\\ \end{array}\]

Error

Target

Derivation

`if x < 8.56379640608457e+122`

`if 8.56379640608457e+122 < x`

Reproduce