Initial program 44.6%
\[\mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, a\right)\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(g\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(g, g\right), \mathsf{*.f64}\left(h, h\right)\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, a\right)\right), \mathsf{\_.f64}\left(\mathsf{neg.f64}\left(g\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(g, g\right), \mathsf{*.f64}\left(h, h\right)\right)\right)\right)\right)\right)\right)
\]
Simplified44.6%
\[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)}
\]
Proof
[Start]44.6 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, a\right)\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(g\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(g, g\right), \mathsf{*.f64}\left(h, h\right)\right)\right)\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, a\right)\right), \mathsf{\_.f64}\left(\mathsf{neg.f64}\left(g\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(g, g\right), \mathsf{*.f64}\left(h, h\right)\right)\right)\right)\right)\right)\right)
\] |
|---|
Taylor expanded in g around inf 23.3%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{+.f64}\left(h, \mathsf{*.f64}\left(-1, h\right)\right)\right)}, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\]
Simplified23.3%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\color{blue}{0}, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\]
Proof
[Start]23.3 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{+.f64}\left(h, \mathsf{*.f64}\left(-1, h\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\] |
|---|
distribute-rgt1-in [=>]23.3 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(-1, 1\right), h\right)}\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\] |
|---|
metadata-eval [=>]23.3 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{*.f64}\left(\color{blue}{0}, h\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\] |
|---|
mul0-lft [=>]23.3 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \color{blue}{0}\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\] |
|---|
metadata-eval [=>]23.3 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\color{blue}{0}, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(g, h\right), \mathsf{\_.f64}\left(g, h\right)\right)\right)\right), \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right)\right)
\] |
|---|
Taylor expanded in g around inf 73.2%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(g, a\right)\right)}\right)\right)
\]
Simplified73.2%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(g\right), a\right)}\right)\right)
\]
Proof
[Start]73.2 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(g, a\right)\right)\right)\right)
\] |
|---|
associate-*r/ [=>]73.2 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, g\right), a\right)}\right)\right)
\] |
|---|
mul-1-neg [=>]73.2 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(g\right)}, a\right)\right)\right)
\] |
|---|
Applied egg-rr95.8%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{cbrt.f64}\left(g\right), \mathsf{cbrt.f64}\left(\mathsf{neg.f64}\left(a\right)\right)\right)}\right)
\]
Proof
[Start]73.2 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(g\right), a\right)\right)\right)
\] |
|---|
frac-2neg [=>]73.2 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{cbrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(g\right)\right), \mathsf{neg.f64}\left(a\right)\right)}\right)\right)
\] |
|---|
cbrt-div [=>]95.8 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(g\right)\right)\right), \mathsf{cbrt.f64}\left(\mathsf{neg.f64}\left(a\right)\right)\right)}\right)
\] |
|---|
remove-double-neg [=>]95.8 | \[ \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{/.f64}\left(\mathsf{cbrt.f64}\left(\color{blue}{g}\right), \mathsf{cbrt.f64}\left(\mathsf{neg.f64}\left(a\right)\right)\right)\right)
\] |
|---|
Final simplification95.8%
\[\leadsto \mathsf{+.f64}\left(\mathsf{cbrt.f64}\left(\mathsf{*.f64}\left(0, \mathsf{/.f64}\left(\frac{-1}{2}, a\right)\right)\right), \mathsf{/.f64}\left(\mathsf{cbrt.f64}\left(g\right), \mathsf{cbrt.f64}\left(\mathsf{neg.f64}\left(a\right)\right)\right)\right)
\]