Average Error: 0.3 → 0.0
Time: 13.2s
Precision: 64
\[\log x - \log \left(\log x\right)\]
↓
\[\log \left(\frac{\sqrt{x}}{\log x} \cdot \sqrt{x}\right)\]
double f(double x) {
        double r5863094 = x;
        double r5863095 = log(r5863094);
        double r5863096 = log(r5863095);
        double r5863097 = r5863095 - r5863096;
        return r5863097;
}
↓
double f(double x) {
        double r5863098 = x;
        double r5863099 = sqrt(r5863098);
        double r5863100 = log(r5863098);
        double r5863101 = r5863099 / r5863100;
        double r5863102 = r5863101 * r5863099;
        double r5863103 = log(r5863102);
        return r5863103;
}


\log x - \log \left(\log x\right)
↓
\log \left(\frac{\sqrt{x}}{\log x} \cdot \sqrt{x}\right)

Error

Bits error versus x

Derivation

  1. Initial program 0.3

    \[\log x - \log \left(\log x\right)\]
  2. Using strategy rm

  3. Applied diff-log0.0

    \[\leadsto \color{blue}{\log \left(\frac{x}{\log x}\right)}\]
  4. Using strategy rm

  5. Applied *-un-lft-identity0.0

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

  6. Applied add-sqr-sqrt0.0

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

  7. Applied times-frac0.0

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

  8. Simplified0.0

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

  9. Final simplification0.0

    \[\leadsto \log \left(\frac{\sqrt{x}}{\log x} \cdot \sqrt{x}\right)\]

Reproduce

herbie shell --seed 2019101 +o rules:numerics
(FPCore (x)
  :name "Jmat.Real.lambertw, estimator"
  (- (log x) (log (log x))))