1. Initial program 53.0%

   \[\sqrt{x + 1} - \sqrt{x} \]
2. Step-by-step derivation

   1. flip--53.8%

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

   2. div-inv53.8%

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

   3. add-sqr-sqrt53.7%

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

   4. add-sqr-sqrt54.2%

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

3. Applied egg-rr54.2%

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

   1. associate-*r/54.2%

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

   2. *-rgt-identity54.2%

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

   3. remove-double-neg54.2%

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

   4. sub-neg54.2%

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

   5. div-sub53.1%

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

   6. rem-square-sqrt52.9%

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

   7. sqr-neg52.9%

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

   8. div-sub53.7%

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

   9. sqr-neg53.7%

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

   10. +-commutative53.7%

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

   11. rem-square-sqrt54.2%

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

   12. associate--l+99.7%

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

   13. +-inverses99.7%

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

   14. metadata-eval99.7%

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

   15. sub-neg99.7%

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

5. Simplified99.7%

   \[\leadsto \color{blue}{\frac{1}{\sqrt{1 + x} + \sqrt{x}}} \]

6. Final simplification99.7%

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

1. Split input into 2 regimes

2. if (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)) < 1.00000000000000005e-4

   1. Initial program 5.8%

      \[\sqrt{x + 1} - \sqrt{x} \]
   2. Step-by-step derivation

      1. flip3--4.3%

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

      2. div-inv4.3%

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

      3. sqrt-pow24.2%

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

      4. metadata-eval4.2%

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

      5. sqrt-pow24.4%

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

      6. metadata-eval4.4%

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

      7. add-sqr-sqrt4.4%

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

      8. add-sqr-sqrt4.4%

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

      9. associate-+r+4.4%

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

      10. sqrt-unprod4.4%

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

   3. Applied egg-rr4.4%

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

   4. Taylor expanded in x around inf 98.8%

      \[\leadsto \color{blue}{0.5 \cdot \sqrt{\frac{1}{x}}} \]
   5. Step-by-step derivation

      1. *-commutative98.8%

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

   6. Simplified98.8%

      \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot 0.5} \]
   7. Step-by-step derivation

      1. expm1-log1p-u98.8%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)\right)} \cdot 0.5 \]

      2. expm1-udef7.8%

         \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)} - 1\right)} \cdot 0.5 \]

      3. inv-pow7.8%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{{x}^{-1}}}\right)} - 1\right) \cdot 0.5 \]

      4. sqrt-pow17.8%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{{x}^{\left(\frac{-1}{2}\right)}}\right)} - 1\right) \cdot 0.5 \]

      5. metadata-eval7.8%

         \[\leadsto \left(e^{\mathsf{log1p}\left({x}^{\color{blue}{-0.5}}\right)} - 1\right) \cdot 0.5 \]

   8. Applied egg-rr7.8%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left({x}^{-0.5}\right)} - 1\right)} \cdot 0.5 \]
   9. Step-by-step derivation

      1. expm1-def99.0%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({x}^{-0.5}\right)\right)} \cdot 0.5 \]

      2. expm1-log1p99.0%

         \[\leadsto \color{blue}{{x}^{-0.5}} \cdot 0.5 \]

   10. Simplified99.0%

       \[\leadsto \color{blue}{{x}^{-0.5}} \cdot 0.5 \]

   if 1.00000000000000005e-4 < (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x))

   1. Initial program 99.5%

      \[\sqrt{x + 1} - \sqrt{x} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\sqrt{1 + x} - \sqrt{x} \leq 0.0001:\\ \;\;\;\;{x}^{-0.5} \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1 + x} - \sqrt{x}\\ \end{array} \]

1. Split input into 2 regimes

2. if x < 1

   1. Initial program 100.0%

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

   2. Taylor expanded in x around 0 98.7%

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

      1. +-commutative98.7%

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

      2. associate--l+98.7%

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

      3. *-commutative98.7%

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

   4. Applied egg-rr98.7%

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

   if 1 < x

   1. Initial program 8.3%

      \[\sqrt{x + 1} - \sqrt{x} \]
   2. Step-by-step derivation

      1. flip3--6.8%

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

      2. div-inv6.8%

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

      3. sqrt-pow26.7%

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

      4. metadata-eval6.7%

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

      5. sqrt-pow27.0%

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

      6. metadata-eval7.0%

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

      7. add-sqr-sqrt7.0%

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

      8. add-sqr-sqrt7.0%

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

      9. associate-+r+7.0%

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

      10. sqrt-unprod7.0%

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

   3. Applied egg-rr7.0%

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

   4. Taylor expanded in x around inf 96.9%

      \[\leadsto \color{blue}{0.5 \cdot \sqrt{\frac{1}{x}}} \]
   5. Step-by-step derivation

      1. *-commutative96.9%

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

   6. Simplified96.9%

      \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot 0.5} \]
   7. Step-by-step derivation

      1. expm1-log1p-u96.9%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)\right)} \cdot 0.5 \]

      2. expm1-udef8.6%

         \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)} - 1\right)} \cdot 0.5 \]

      3. inv-pow8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{{x}^{-1}}}\right)} - 1\right) \cdot 0.5 \]

      4. sqrt-pow18.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{{x}^{\left(\frac{-1}{2}\right)}}\right)} - 1\right) \cdot 0.5 \]

      5. metadata-eval8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left({x}^{\color{blue}{-0.5}}\right)} - 1\right) \cdot 0.5 \]

   8. Applied egg-rr8.6%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left({x}^{-0.5}\right)} - 1\right)} \cdot 0.5 \]
   9. Step-by-step derivation

      1. expm1-def97.1%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({x}^{-0.5}\right)\right)} \cdot 0.5 \]

      2. expm1-log1p97.1%

         \[\leadsto \color{blue}{{x}^{-0.5}} \cdot 0.5 \]

   10. Simplified97.1%

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

4. Final simplification97.9%

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

1. Split input into 2 regimes

2. if x < 1

   1. Initial program 100.0%

      \[\sqrt{x + 1} - \sqrt{x} \]
   2. Step-by-step derivation

      1. flip--99.9%

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

      2. div-inv99.9%

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

      3. add-sqr-sqrt100.0%

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

      4. add-sqr-sqrt100.0%

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

   3. Applied egg-rr100.0%

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

      1. associate-*r/100.0%

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

      2. *-rgt-identity100.0%

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

      3. remove-double-neg100.0%

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

      4. sub-neg100.0%

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

      5. div-sub99.9%

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

      6. rem-square-sqrt99.9%

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

      7. sqr-neg99.9%

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

      8. div-sub100.0%

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

      9. sqr-neg100.0%

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

      10. +-commutative100.0%

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

      11. rem-square-sqrt100.0%

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

      12. associate--l+100.0%

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

      13. +-inverses100.0%

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

      14. metadata-eval100.0%

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

      15. sub-neg100.0%

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

   5. Simplified100.0%

      \[\leadsto \color{blue}{\frac{1}{\sqrt{1 + x} + \sqrt{x}}} \]
   6. Step-by-step derivation

      1. add-sqr-sqrt99.9%

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

      2. pow299.9%

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

      3. pow1/299.9%

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

      4. +-commutative99.9%

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

      5. sqrt-pow199.9%

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

      6. metadata-eval99.9%

         \[\leadsto \frac{1}{{\left({\left(x + 1\right)}^{\color{blue}{0.25}}\right)}^{2} + \sqrt{x}} \]

   7. Applied egg-rr99.9%

      \[\leadsto \frac{1}{\color{blue}{{\left({\left(x + 1\right)}^{0.25}\right)}^{2}} + \sqrt{x}} \]

   8. Taylor expanded in x around 0 97.7%

      \[\leadsto \frac{1}{\color{blue}{1} + \sqrt{x}} \]

   if 1 < x

   1. Initial program 8.3%

      \[\sqrt{x + 1} - \sqrt{x} \]
   2. Step-by-step derivation

      1. flip3--6.8%

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

      2. div-inv6.8%

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

      3. sqrt-pow26.7%

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

      4. metadata-eval6.7%

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

      5. sqrt-pow27.0%

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

      6. metadata-eval7.0%

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

      7. add-sqr-sqrt7.0%

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

      8. add-sqr-sqrt7.0%

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

      9. associate-+r+7.0%

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

      10. sqrt-unprod7.0%

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

   3. Applied egg-rr7.0%

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

   4. Taylor expanded in x around inf 96.9%

      \[\leadsto \color{blue}{0.5 \cdot \sqrt{\frac{1}{x}}} \]
   5. Step-by-step derivation

      1. *-commutative96.9%

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

   6. Simplified96.9%

      \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot 0.5} \]
   7. Step-by-step derivation

      1. expm1-log1p-u96.9%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)\right)} \cdot 0.5 \]

      2. expm1-udef8.6%

         \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)} - 1\right)} \cdot 0.5 \]

      3. inv-pow8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{{x}^{-1}}}\right)} - 1\right) \cdot 0.5 \]

      4. sqrt-pow18.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{{x}^{\left(\frac{-1}{2}\right)}}\right)} - 1\right) \cdot 0.5 \]

      5. metadata-eval8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left({x}^{\color{blue}{-0.5}}\right)} - 1\right) \cdot 0.5 \]

   8. Applied egg-rr8.6%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left({x}^{-0.5}\right)} - 1\right)} \cdot 0.5 \]
   9. Step-by-step derivation

      1. expm1-def97.1%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({x}^{-0.5}\right)\right)} \cdot 0.5 \]

      2. expm1-log1p97.1%

         \[\leadsto \color{blue}{{x}^{-0.5}} \cdot 0.5 \]

   10. Simplified97.1%

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

4. Final simplification97.4%

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

1. Split input into 2 regimes

2. if x < 0.25

   1. Initial program 100.0%

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

   2. Taylor expanded in x around 0 96.6%

      \[\leadsto \color{blue}{1} \]

   if 0.25 < x

   1. Initial program 8.3%

      \[\sqrt{x + 1} - \sqrt{x} \]
   2. Step-by-step derivation

      1. flip3--6.8%

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

      2. div-inv6.8%

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

      3. sqrt-pow26.7%

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

      4. metadata-eval6.7%

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

      5. sqrt-pow27.0%

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

      6. metadata-eval7.0%

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

      7. add-sqr-sqrt7.0%

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

      8. add-sqr-sqrt7.0%

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

      9. associate-+r+7.0%

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

      10. sqrt-unprod7.0%

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

   3. Applied egg-rr7.0%

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

   4. Taylor expanded in x around inf 96.9%

      \[\leadsto \color{blue}{0.5 \cdot \sqrt{\frac{1}{x}}} \]
   5. Step-by-step derivation

      1. *-commutative96.9%

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

   6. Simplified96.9%

      \[\leadsto \color{blue}{\sqrt{\frac{1}{x}} \cdot 0.5} \]
   7. Step-by-step derivation

      1. expm1-log1p-u96.9%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)\right)} \cdot 0.5 \]

      2. expm1-udef8.6%

         \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left(\sqrt{\frac{1}{x}}\right)} - 1\right)} \cdot 0.5 \]

      3. inv-pow8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\sqrt{\color{blue}{{x}^{-1}}}\right)} - 1\right) \cdot 0.5 \]

      4. sqrt-pow18.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left(\color{blue}{{x}^{\left(\frac{-1}{2}\right)}}\right)} - 1\right) \cdot 0.5 \]

      5. metadata-eval8.6%

         \[\leadsto \left(e^{\mathsf{log1p}\left({x}^{\color{blue}{-0.5}}\right)} - 1\right) \cdot 0.5 \]

   8. Applied egg-rr8.6%

      \[\leadsto \color{blue}{\left(e^{\mathsf{log1p}\left({x}^{-0.5}\right)} - 1\right)} \cdot 0.5 \]
   9. Step-by-step derivation

      1. expm1-def97.1%

         \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({x}^{-0.5}\right)\right)} \cdot 0.5 \]

      2. expm1-log1p97.1%

         \[\leadsto \color{blue}{{x}^{-0.5}} \cdot 0.5 \]

   10. Simplified97.1%

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

4. Final simplification96.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.25:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;{x}^{-0.5} \cdot 0.5\\ \end{array} \]

1. Initial program 53.0%

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

2. Taylor expanded in x around 0 50.7%

   \[\leadsto \color{blue}{1} \]

3. Final simplification50.7%

   \[\leadsto 1 \]

herbie shell --seed 2023166 
(FPCore (x)
  :name "2sqrt (example 3.1)"
  :precision binary64

  :herbie-target
  (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x)))

  (- (sqrt (+ x 1.0)) (sqrt x)))