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