Average Error: 0.8 → 0.6
Time: 32.1s
Precision: 64
\[\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)\]
↓
\[\frac{\sqrt{1 + x} \cdot \left(\sqrt{1 + x} + \sqrt{x}\right) + \left(-\sqrt{x}\right) \cdot \left(\sqrt{1 + x} + \sqrt{x}\right)}{\sqrt{1 + x} + \sqrt{x}}\]
\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)
↓
\frac{\sqrt{1 + x} \cdot \left(\sqrt{1 + x} + \sqrt{x}\right) + \left(-\sqrt{x}\right) \cdot \left(\sqrt{1 + x} + \sqrt{x}\right)}{\sqrt{1 + x} + \sqrt{x}}
double f(double x) {
        double r1944840 = x;
        double r1944841 = 1.0;
        double r1944842 = /* ERROR: no posit support in C */;
        double r1944843 = r1944840 + r1944842;
        double r1944844 = sqrt(r1944843);
        double r1944845 = sqrt(r1944840);
        double r1944846 = r1944844 - r1944845;
        return r1944846;
}
↓
double f(double x) {
        double r1944847 = 1.0;
        double r1944848 = x;
        double r1944849 = r1944847 + r1944848;
        double r1944850 = sqrt(r1944849);
        double r1944851 = sqrt(r1944848);
        double r1944852 = r1944850 + r1944851;
        double r1944853 = r1944850 * r1944852;
        double r1944854 = -r1944851;
        double r1944855 = r1944854 * r1944852;
        double r1944856 = r1944853 + r1944855;
        double r1944857 = r1944856 / r1944852;
        return r1944857;
}

Error

Bits error versus x

Derivation

  1. Initial program 0.8

    \[\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)\]
  2. Using strategy rm

  3. Applied p16-flip--0.6

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

  4. Simplified0.8

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

  5. Simplified0.8

    \[\leadsto \frac{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}{\left(\sqrt{x}\right)}\right) \cdot \left(\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right) - \left(\sqrt{x}\right)\right)\right)}{\color{blue}{\left(\frac{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}{\left(\sqrt{x}\right)}\right)}}\]
  6. Using strategy rm

  7. Applied sub-neg0.8

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

  8. Applied distribute-rgt-in0.6

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

  9. Final simplification0.6

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

Reproduce

herbie shell --seed 2019152 
(FPCore (x)
  :name "2sqrt (example 3.1)"
  (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))