Initial program 30.3
\[\sqrt{2 \cdot {x}^{2}}
\]
Simplified30.3
\[\leadsto \color{blue}{\sqrt{2 \cdot \left(x \cdot x\right)}}
\]
Proof
(sqrt.f64 (*.f64 2 (*.f64 x x))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 x 2)))): 2 points increase in error, 0 points decrease in error
Taylor expanded in x around 0 31.7
\[\leadsto \color{blue}{\sqrt{2} \cdot x}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{hypot}\left(x, x\right)}
\]
Proof
(hypot.f64 x x): 0 points increase in error, 0 points decrease in error
(Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 x x)))): 11 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 x (+.f64 x x)))): 11 points increase in error, 1 points decrease in error
(sqrt.f64 (*.f64 x (Rewrite=> count-2_binary64 (*.f64 2 x)))): 0 points increase in error, 10 points decrease in error
(sqrt.f64 (*.f64 x (Rewrite=> *-commutative_binary64 (*.f64 x 2)))): 0 points increase in error, 5 points decrease in error
(sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x x) 2))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (*.f64 (*.f64 x x) (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 2) (sqrt.f64 2))))): 11 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 x (sqrt.f64 2)) (*.f64 x (sqrt.f64 2))))): 10 points increase in error, 0 points decrease in error
(Rewrite=> rem-sqrt-square_binary64 (fabs.f64 (*.f64 x (sqrt.f64 2)))): 2 points increase in error, 8 points decrease in error
(fabs.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (*.f64 x (sqrt.f64 2))) (sqrt.f64 (*.f64 x (sqrt.f64 2)))))): 8 points increase in error, 4 points decrease in error
(Rewrite=> fabs-sqr_binary64 (*.f64 (sqrt.f64 (*.f64 x (sqrt.f64 2))) (sqrt.f64 (*.f64 x (sqrt.f64 2))))): 11 points increase in error, 0 points decrease in error
(Rewrite=> rem-square-sqrt_binary64 (*.f64 x (sqrt.f64 2))): 0 points increase in error, 12 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 2) x)): 11 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{hypot}\left(x, x\right)
\]