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;
}



# Try it out

Results

 In Out
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}}$

$\leadsto \frac{\frac{x}{\color{blue}{\sqrt{y} \cdot \sqrt{y}}}}{1 \cdot z}$

$\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))