Average Error: 9.7 → 0.7
Time: 20.4s
Precision: 64
\[\left(0 \lt x \land x \lt y\right) \land \left(0 \lt z \land z \lt 2\right)\]
\[\frac{\frac{x}{y}}{z}\]
\[\frac{\frac{\sqrt{x}}{\sqrt{y}}}{z} \cdot \frac{\sqrt{x}}{\sqrt{y}}\]
\frac{\frac{x}{y}}{z}
\frac{\frac{\sqrt{x}}{\sqrt{y}}}{z} \cdot \frac{\sqrt{x}}{\sqrt{y}}
double f(double x, double y, double z) {
        double r23226998 = x;
        double r23226999 = y;
        double r23227000 = r23226998 / r23226999;
        double r23227001 = z;
        double r23227002 = r23227000 / r23227001;
        return r23227002;
}

double f(double x, double y, double z) {
        double r23227003 = x;
        double r23227004 = sqrt(r23227003);
        double r23227005 = y;
        double r23227006 = sqrt(r23227005);
        double r23227007 = r23227004 / r23227006;
        double r23227008 = z;
        double r23227009 = r23227007 / r23227008;
        double r23227010 = r23227009 * r23227007;
        return r23227010;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 9.7

    \[\frac{\frac{x}{y}}{z}\]
  2. Using strategy rm
  3. Applied *-un-lft-identity9.7

    \[\leadsto \frac{\frac{x}{y}}{\color{blue}{1 \cdot z}}\]
  4. Applied add-sqr-sqrt10.0

    \[\leadsto \frac{\frac{x}{\color{blue}{\sqrt{y} \cdot \sqrt{y}}}}{1 \cdot z}\]
  5. Applied add-sqr-sqrt10.1

    \[\leadsto \frac{\frac{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}{\sqrt{y} \cdot \sqrt{y}}}{1 \cdot z}\]
  6. Applied times-frac10.1

    \[\leadsto \frac{\color{blue}{\frac{\sqrt{x}}{\sqrt{y}} \cdot \frac{\sqrt{x}}{\sqrt{y}}}}{1 \cdot z}\]
  7. Applied times-frac0.7

    \[\leadsto \color{blue}{\frac{\frac{\sqrt{x}}{\sqrt{y}}}{1} \cdot \frac{\frac{\sqrt{x}}{\sqrt{y}}}{z}}\]
  8. Simplified0.7

    \[\leadsto \color{blue}{\frac{\sqrt{x}}{\sqrt{y}}} \cdot \frac{\frac{\sqrt{x}}{\sqrt{y}}}{z}\]
  9. Final simplification0.7

    \[\leadsto \frac{\frac{\sqrt{x}}{\sqrt{y}}}{z} \cdot \frac{\sqrt{x}}{\sqrt{y}}\]

Reproduce

herbie shell --seed 1 
(FPCore (x y z)
  :name "(x/y)/z"
  :pre (and (and (< 0 x) (< x y)) (and (< 0 z) (< z 2)))
  (/ (/ x y) z))