Initial program 37.6
\[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}
\]
Applied egg-rr0.9
\[\leadsto \color{blue}{\mathsf{hypot}\left(z, \mathsf{hypot}\left(x, y\right)\right) \cdot \frac{1}{\sqrt{3}}}
\]
Simplified0.4
\[\leadsto \color{blue}{\frac{\mathsf{hypot}\left(z, \mathsf{hypot}\left(y, x\right)\right)}{\sqrt{3}}}
\]
Proof
(/.f64 (hypot.f64 z (hypot.f64 y x)) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 y y) (*.f64 x x))))) (sqrt.f64 3)): 97 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) (*.f64 x x)))) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (sqrt.f64 (+.f64 (pow.f64 y 2) (Rewrite<= unpow2_binary64 (pow.f64 x 2))))) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (sqrt.f64 (Rewrite=> +-commutative_binary64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))))) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (sqrt.f64 (+.f64 (Rewrite=> unpow2_binary64 (*.f64 x x)) (pow.f64 y 2)))) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (sqrt.f64 (+.f64 (*.f64 x x) (Rewrite=> unpow2_binary64 (*.f64 y y))))) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(/.f64 (hypot.f64 z (Rewrite=> hypot-def_binary64 (hypot.f64 x y))) (sqrt.f64 3)): 0 points increase in error, 97 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (hypot.f64 z (hypot.f64 x y)) 1)) (sqrt.f64 3)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (hypot.f64 z (hypot.f64 x y)) (/.f64 1 (sqrt.f64 3)))): 105 points increase in error, 0 points decrease in error
Final simplification0.4
\[\leadsto \frac{\mathsf{hypot}\left(z, \mathsf{hypot}\left(y, x\right)\right)}{\sqrt{3}}
\]