Average Error: 0.8 → 0.6
Time: 30.3s
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 r2084690 = x;
        double r2084691 = 1.0;
        double r2084692 = /* ERROR: no posit support in C */;
        double r2084693 = r2084690 + r2084692;
        double r2084694 = sqrt(r2084693);
        double r2084695 = sqrt(r2084690);
        double r2084696 = r2084694 - r2084695;
        return r2084696;
}
↓
double f(double x) {
        double r2084697 = 1.0;
        double r2084698 = x;
        double r2084699 = r2084697 + r2084698;
        double r2084700 = sqrt(r2084699);
        double r2084701 = sqrt(r2084698);
        double r2084702 = r2084700 + r2084701;
        double r2084703 = r2084700 * r2084702;
        double r2084704 = -r2084701;
        double r2084705 = r2084704 * r2084702;
        double r2084706 = r2084703 + r2084705;
        double r2084707 = r2084706 / r2084702;
        return r2084707;
}

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 +o rules:numerics
(FPCore (x)
  :name "2sqrt (example 3.1)"
  (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))