ENA, Section 1.4, Exercise 4d

1. Split input into 2 regimes

2. if (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps))) < -9.9999999999999997e-155

   1. Initial program 98.2%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. flip--98.1%

         \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      2. div-inv97.9%

         \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      3. add-sqr-sqrt97.5%

         \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

      4. sub-neg97.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

      5. add-sqr-sqrt97.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

      6. hypot-def97.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Applied egg-rr97.5%

      \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
   4. Step-by-step derivation

      1. associate-*r/97.6%

         \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

      2. *-rgt-identity97.6%

         \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      3. associate--r-99.2%

         \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      4. +-inverses99.2%

         \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      5. +-lft-identity99.2%

         \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. Simplified99.2%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   if -9.9999999999999997e-155 < (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps)))

   1. Initial program 9.4%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. flip--9.3%

         \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      2. div-inv9.3%

         \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      3. add-sqr-sqrt9.4%

         \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

      4. sub-neg9.4%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

      5. add-sqr-sqrt2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

      6. hypot-def2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Applied egg-rr2.5%

      \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
   4. Step-by-step derivation

      1. associate-*r/2.5%

         \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

      2. *-rgt-identity2.5%

         \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      3. associate--r-47.7%

         \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      4. +-inverses47.7%

         \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      5. +-lft-identity47.7%

         \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. Simplified47.7%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   6. Taylor expanded in x around inf 0.0%

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

      1. associate-*r/0.0%

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

      2. unpow20.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

      3. rem-square-sqrt98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

      4. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

      5. associate-*r*98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

      6. metadata-eval98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

      7. associate-*r/98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

      8. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

      9. fma-def98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

   8. Simplified98.8%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]
   9. Step-by-step derivation

      1. fma-udef98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]

   10. Applied egg-rr98.8%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x - \sqrt{x \cdot x - \varepsilon} \leq -1 \cdot 10^{-154}:\\ \;\;\;\;\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}\\ \end{array} \]

1. Split input into 2 regimes

2. if (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps))) < -9.9999999999999997e-155

   1. Initial program 98.2%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. sub-neg98.2%

         \[\leadsto x - \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}} \]

      2. +-commutative98.2%

         \[\leadsto x - \sqrt{\color{blue}{\left(-\varepsilon\right) + x \cdot x}} \]

      3. add-sqr-sqrt98.3%

         \[\leadsto x - \sqrt{\color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}} + x \cdot x} \]

      4. hypot-def98.3%

         \[\leadsto x - \color{blue}{\mathsf{hypot}\left(\sqrt{-\varepsilon}, x\right)} \]

   3. Applied egg-rr98.3%

      \[\leadsto x - \color{blue}{\mathsf{hypot}\left(\sqrt{-\varepsilon}, x\right)} \]

   if -9.9999999999999997e-155 < (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps)))

   1. Initial program 9.4%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. flip--9.3%

         \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      2. div-inv9.3%

         \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      3. add-sqr-sqrt9.4%

         \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

      4. sub-neg9.4%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

      5. add-sqr-sqrt2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

      6. hypot-def2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Applied egg-rr2.5%

      \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
   4. Step-by-step derivation

      1. associate-*r/2.5%

         \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

      2. *-rgt-identity2.5%

         \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      3. associate--r-47.7%

         \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      4. +-inverses47.7%

         \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      5. +-lft-identity47.7%

         \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. Simplified47.7%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   6. Taylor expanded in x around inf 0.0%

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

      1. associate-*r/0.0%

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

      2. unpow20.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

      3. rem-square-sqrt98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

      4. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

      5. associate-*r*98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

      6. metadata-eval98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

      7. associate-*r/98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

      8. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

      9. fma-def98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

   8. Simplified98.8%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]
   9. Step-by-step derivation

      1. fma-udef98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]

   10. Applied egg-rr98.8%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]
3. Recombined 2 regimes into one program.

4. Final simplification98.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x - \sqrt{x \cdot x - \varepsilon} \leq -1 \cdot 10^{-154}:\\ \;\;\;\;x - \mathsf{hypot}\left(\sqrt{-\varepsilon}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}\\ \end{array} \]

1. Split input into 2 regimes

2. if (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps))) < -9.9999999999999997e-155

   1. Initial program 98.2%

      \[x - \sqrt{x \cdot x - \varepsilon} \]

   if -9.9999999999999997e-155 < (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps)))

   1. Initial program 9.4%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. flip--9.3%

         \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      2. div-inv9.3%

         \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      3. add-sqr-sqrt9.4%

         \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

      4. sub-neg9.4%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

      5. add-sqr-sqrt2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

      6. hypot-def2.5%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Applied egg-rr2.5%

      \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
   4. Step-by-step derivation

      1. associate-*r/2.5%

         \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

      2. *-rgt-identity2.5%

         \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      3. associate--r-47.7%

         \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      4. +-inverses47.7%

         \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      5. +-lft-identity47.7%

         \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. Simplified47.7%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   6. Taylor expanded in x around inf 0.0%

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

      1. associate-*r/0.0%

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

      2. unpow20.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

      3. rem-square-sqrt98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

      4. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

      5. associate-*r*98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

      6. metadata-eval98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

      7. associate-*r/98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

      8. *-commutative98.8%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

      9. fma-def98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

   8. Simplified98.8%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]
   9. Step-by-step derivation

      1. fma-udef98.8%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]

   10. Applied egg-rr98.8%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]
3. Recombined 2 regimes into one program.

4. Final simplification98.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x - \sqrt{x \cdot x - \varepsilon} \leq -1 \cdot 10^{-154}:\\ \;\;\;\;x - \sqrt{x \cdot x - \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}\\ \end{array} \]

1. Split input into 2 regimes

2. if x < 1.62000000000000004e-111

   1. Initial program 98.8%

      \[x - \sqrt{x \cdot x - \varepsilon} \]

   2. Taylor expanded in x around 0 96.7%

      \[\leadsto x - \sqrt{\color{blue}{-1 \cdot \varepsilon}} \]
   3. Step-by-step derivation

      1. neg-mul-196.7%

         \[\leadsto x - \sqrt{\color{blue}{-\varepsilon}} \]

   4. Simplified96.7%

      \[\leadsto x - \sqrt{\color{blue}{-\varepsilon}} \]

   if 1.62000000000000004e-111 < x

   1. Initial program 28.7%

      \[x - \sqrt{x \cdot x - \varepsilon} \]
   2. Step-by-step derivation

      1. flip--28.6%

         \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      2. div-inv28.6%

         \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

      3. add-sqr-sqrt28.6%

         \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

      4. sub-neg28.6%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

      5. add-sqr-sqrt24.7%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

      6. hypot-def24.7%

         \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Applied egg-rr24.7%

      \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
   4. Step-by-step derivation

      1. associate-*r/24.6%

         \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

      2. *-rgt-identity24.6%

         \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      3. associate--r-61.9%

         \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      4. +-inverses61.9%

         \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

      5. +-lft-identity61.9%

         \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. Simplified61.9%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   6. Taylor expanded in x around inf 0.0%

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

      1. associate-*r/0.0%

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

      2. unpow20.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

      3. rem-square-sqrt81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

      4. *-commutative81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

      5. associate-*r*81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

      6. metadata-eval81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

      7. associate-*r/81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

      8. *-commutative81.0%

         \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

      9. fma-def81.0%

         \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

   8. Simplified81.0%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

   9. Taylor expanded in x around 0 81.0%

      \[\leadsto \frac{\varepsilon}{\color{blue}{-0.5 \cdot \frac{\varepsilon}{x} + 2 \cdot x}} \]
3. Recombined 2 regimes into one program.

4. Final simplification89.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 1.62 \cdot 10^{-111}:\\ \;\;\;\;x - \sqrt{-\varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{\frac{\varepsilon}{x} \cdot -0.5 + x \cdot 2}\\ \end{array} \]

1. Initial program 68.4%

   \[x - \sqrt{x \cdot x - \varepsilon} \]
2. Step-by-step derivation

   1. flip--68.3%

      \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   2. div-inv68.1%

      \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   3. add-sqr-sqrt67.9%

      \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

   4. sub-neg67.9%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

   5. add-sqr-sqrt65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

   6. hypot-def65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

3. Applied egg-rr65.6%

   \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
4. Step-by-step derivation

   1. associate-*r/65.7%

      \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   2. *-rgt-identity65.7%

      \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   3. associate--r-81.9%

      \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   4. +-inverses81.9%

      \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. +-lft-identity81.9%

      \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

5. Simplified81.9%

   \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

6. Taylor expanded in x around inf 0.0%

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

   1. associate-*r/0.0%

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

   2. unpow20.0%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

   3. rem-square-sqrt39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

   4. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

   5. associate-*r*39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

   6. metadata-eval39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

   7. associate-*r/39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

   8. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

   9. fma-def39.6%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

8. Simplified39.6%

   \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]
9. Step-by-step derivation

   1. fma-udef39.6%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]

10. Applied egg-rr39.6%

    \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\frac{\varepsilon}{x} \cdot -0.5 + x\right)}} \]

11. Final simplification39.6%

    \[\leadsto \frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)} \]

1. Initial program 68.4%

   \[x - \sqrt{x \cdot x - \varepsilon} \]
2. Step-by-step derivation

   1. flip--68.3%

      \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   2. div-inv68.1%

      \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   3. add-sqr-sqrt67.9%

      \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

   4. sub-neg67.9%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

   5. add-sqr-sqrt65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

   6. hypot-def65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

3. Applied egg-rr65.6%

   \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
4. Step-by-step derivation

   1. associate-*r/65.7%

      \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   2. *-rgt-identity65.7%

      \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   3. associate--r-81.9%

      \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   4. +-inverses81.9%

      \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. +-lft-identity81.9%

      \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

5. Simplified81.9%

   \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

6. Taylor expanded in x around inf 0.0%

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

   1. associate-*r/0.0%

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

   2. unpow20.0%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

   3. rem-square-sqrt39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

   4. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

   5. associate-*r*39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

   6. metadata-eval39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

   7. associate-*r/39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

   8. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

   9. fma-def39.6%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

8. Simplified39.6%

   \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

9. Taylor expanded in x around 0 39.6%

   \[\leadsto \frac{\varepsilon}{\color{blue}{-0.5 \cdot \frac{\varepsilon}{x} + 2 \cdot x}} \]

10. Final simplification39.6%

    \[\leadsto \frac{\varepsilon}{\frac{\varepsilon}{x} \cdot -0.5 + x \cdot 2} \]

1. Initial program 68.4%

   \[x - \sqrt{x \cdot x - \varepsilon} \]

2. Taylor expanded in x around inf 38.2%

   \[\leadsto \color{blue}{0.5 \cdot \frac{\varepsilon}{x}} \]

3. Final simplification38.2%

   \[\leadsto \frac{\varepsilon}{x} \cdot 0.5 \]

1. Initial program 68.4%

   \[x - \sqrt{x \cdot x - \varepsilon} \]
2. Step-by-step derivation

   1. flip--68.3%

      \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   2. div-inv68.1%

      \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   3. add-sqr-sqrt67.9%

      \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

   4. sub-neg67.9%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

   5. add-sqr-sqrt65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

   6. hypot-def65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

3. Applied egg-rr65.6%

   \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
4. Step-by-step derivation

   1. associate-*r/65.7%

      \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   2. *-rgt-identity65.7%

      \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   3. associate--r-81.9%

      \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   4. +-inverses81.9%

      \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. +-lft-identity81.9%

      \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

5. Simplified81.9%

   \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

6. Taylor expanded in x around inf 0.0%

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

   1. associate-*r/0.0%

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

   2. unpow20.0%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

   3. rem-square-sqrt39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

   4. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

   5. associate-*r*39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

   6. metadata-eval39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

   7. associate-*r/39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

   8. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

   9. fma-def39.6%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

8. Simplified39.6%

   \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

9. Taylor expanded in eps around inf 5.5%

   \[\leadsto \color{blue}{-2 \cdot x} \]
10. Step-by-step derivation

    1. *-commutative5.5%

       \[\leadsto \color{blue}{x \cdot -2} \]

11. Simplified5.5%

    \[\leadsto \color{blue}{x \cdot -2} \]

12. Final simplification5.5%

    \[\leadsto x \cdot -2 \]

1. Initial program 68.4%

   \[x - \sqrt{x \cdot x - \varepsilon} \]
2. Step-by-step derivation

   1. flip--68.3%

      \[\leadsto \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   2. div-inv68.1%

      \[\leadsto \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]

   3. add-sqr-sqrt67.9%

      \[\leadsto \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

   4. sub-neg67.9%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]

   5. add-sqr-sqrt65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]

   6. hypot-def65.6%

      \[\leadsto \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

3. Applied egg-rr65.6%

   \[\leadsto \color{blue}{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
4. Step-by-step derivation

   1. associate-*r/65.7%

      \[\leadsto \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   2. *-rgt-identity65.7%

      \[\leadsto \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   3. associate--r-81.9%

      \[\leadsto \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   4. +-inverses81.9%

      \[\leadsto \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   5. +-lft-identity81.9%

      \[\leadsto \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

5. Simplified81.9%

   \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

6. Taylor expanded in x around inf 0.0%

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

   1. associate-*r/0.0%

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

   2. unpow20.0%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x} + x\right)} \]

   3. rem-square-sqrt39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x} + x\right)} \]

   4. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x} + x\right)} \]

   5. associate-*r*39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x} + x\right)} \]

   6. metadata-eval39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\frac{\color{blue}{-0.5} \cdot \varepsilon}{x} + x\right)} \]

   7. associate-*r/39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{-0.5 \cdot \frac{\varepsilon}{x}} + x\right)} \]

   8. *-commutative39.6%

      \[\leadsto \frac{\varepsilon}{x + \left(\color{blue}{\frac{\varepsilon}{x} \cdot -0.5} + x\right)} \]

   9. fma-def39.6%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

8. Simplified39.6%

   \[\leadsto \frac{\varepsilon}{x + \color{blue}{\mathsf{fma}\left(\frac{\varepsilon}{x}, -0.5, x\right)}} \]

9. Taylor expanded in eps around inf 10.7%

   \[\leadsto \frac{\varepsilon}{x + \color{blue}{-0.5 \cdot \frac{\varepsilon}{x}}} \]
10. Step-by-step derivation

    1. *-commutative10.7%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\frac{\varepsilon}{x} \cdot -0.5}} \]

    2. associate-*l/10.7%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\frac{\varepsilon \cdot -0.5}{x}}} \]

    3. *-lft-identity10.7%

       \[\leadsto \frac{\varepsilon}{x + \frac{\varepsilon \cdot -0.5}{\color{blue}{1 \cdot x}}} \]

    4. times-frac10.7%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\frac{\varepsilon}{1} \cdot \frac{-0.5}{x}}} \]

    5. rem-square-sqrt3.3%

       \[\leadsto \frac{\varepsilon}{x + \frac{\color{blue}{\sqrt{\varepsilon} \cdot \sqrt{\varepsilon}}}{1} \cdot \frac{-0.5}{x}} \]

    6. associate-*r/3.3%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(\sqrt{\varepsilon} \cdot \frac{\sqrt{\varepsilon}}{1}\right)} \cdot \frac{-0.5}{x}} \]

    7. /-rgt-identity3.3%

       \[\leadsto \frac{\varepsilon}{x + \left(\sqrt{\varepsilon} \cdot \color{blue}{\sqrt{\varepsilon}}\right) \cdot \frac{-0.5}{x}} \]

    8. rem-square-sqrt10.7%

       \[\leadsto \frac{\varepsilon}{x + \color{blue}{\varepsilon} \cdot \frac{-0.5}{x}} \]

11. Simplified10.7%

    \[\leadsto \frac{\varepsilon}{x + \color{blue}{\varepsilon \cdot \frac{-0.5}{x}}} \]

12. Taylor expanded in eps around 0 10.7%

    \[\leadsto \color{blue}{\frac{\varepsilon}{x}} \]

13. Final simplification10.7%

    \[\leadsto \frac{\varepsilon}{x} \]

herbie shell --seed 2023167 
(FPCore (x eps)
  :name "ENA, Section 1.4, Exercise 4d"
  :precision binary64
  :pre (and (and (<= 0.0 x) (<= x 1000000000.0)) (and (<= -1.0 eps) (<= eps 1.0)))

  :herbie-target
  (/ eps (+ x (sqrt (- (* x x) eps))))

  (- x (sqrt (- (* x x) eps))))