Initial program 1.1
\[\sqrt{\frac{1}{2} \cdot \left(1 + \frac{1}{\sqrt{1 + {\left(\frac{2 \cdot \ell}{Om}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}\right)}
\]
Simplified1.1
\[\leadsto \color{blue}{\sqrt{0.5 + 0.5 \cdot \frac{1}{\sqrt{1 + {\left(\frac{2}{\frac{Om}{\ell}}\right)}^{2} \cdot \left({\sin kx}^{2} + {\sin ky}^{2}\right)}}}}
\]
Proof
(sqrt.f64 (+.f64 1/2 (*.f64 1/2 (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (/.f64 2 (/.f64 Om l)) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (+.f64 (Rewrite<= metadata-eval (*.f64 1/2 1)) (*.f64 1/2 (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (/.f64 2 (/.f64 Om l)) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (+.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 1 2)) 1) (*.f64 1/2 (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (/.f64 2 (/.f64 Om l)) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (+.f64 (*.f64 (/.f64 1 2) 1) (*.f64 (Rewrite<= metadata-eval (/.f64 1 2)) (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (/.f64 2 (/.f64 Om l)) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (+.f64 (*.f64 (/.f64 1 2) 1) (*.f64 (/.f64 1 2) (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 2 l) Om)) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2))))))))): 0 points increase in error, 0 points decrease in error
(sqrt.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 (/.f64 1 2) (+.f64 1 (/.f64 1 (sqrt.f64 (+.f64 1 (*.f64 (pow.f64 (/.f64 (*.f64 2 l) Om) 2) (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2)))))))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \sqrt{0.5 + 0.5 \cdot \frac{1}{\color{blue}{e^{\mathsf{log1p}\left(\mathsf{hypot}\left(1, \left(2 \cdot \frac{\ell}{Om}\right) \cdot \mathsf{hypot}\left(\sin kx, \sin ky\right)\right)\right)} - 1}}}
\]
Simplified0.0
\[\leadsto \sqrt{0.5 + 0.5 \cdot \frac{1}{\color{blue}{\mathsf{hypot}\left(1, \mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \left(2 \cdot \frac{\ell}{Om}\right)\right)}}}
\]
Proof
(hypot.f64 1 (*.f64 (hypot.f64 (sin.f64 ky) (sin.f64 kx)) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 (sin.f64 ky) (sin.f64 ky)) (*.f64 (sin.f64 kx) (sin.f64 kx))))) (*.f64 2 (/.f64 l Om)))): 2 points increase in error, 6 points decrease in error
(hypot.f64 1 (*.f64 (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 (sin.f64 ky) 2)) (*.f64 (sin.f64 kx) (sin.f64 kx)))) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (sqrt.f64 (+.f64 (pow.f64 (sin.f64 ky) 2) (Rewrite<= unpow2_binary64 (pow.f64 (sin.f64 kx) 2)))) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (sqrt.f64 (Rewrite=> +-commutative_binary64 (+.f64 (pow.f64 (sin.f64 kx) 2) (pow.f64 (sin.f64 ky) 2)))) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (sqrt.f64 (+.f64 (Rewrite=> unpow2_binary64 (*.f64 (sin.f64 kx) (sin.f64 kx))) (pow.f64 (sin.f64 ky) 2))) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (sqrt.f64 (+.f64 (*.f64 (sin.f64 kx) (sin.f64 kx)) (Rewrite=> unpow2_binary64 (*.f64 (sin.f64 ky) (sin.f64 ky))))) (*.f64 2 (/.f64 l Om)))): 0 points increase in error, 0 points decrease in error
(hypot.f64 1 (*.f64 (Rewrite=> hypot-def_binary64 (hypot.f64 (sin.f64 kx) (sin.f64 ky))) (*.f64 2 (/.f64 l Om)))): 6 points increase in error, 2 points decrease in error
(hypot.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 (/.f64 l Om)) (hypot.f64 (sin.f64 kx) (sin.f64 ky))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (hypot.f64 1 (*.f64 (*.f64 2 (/.f64 l Om)) (hypot.f64 (sin.f64 kx) (sin.f64 ky))))))): 41 points increase in error, 42 points decrease in error
(Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (hypot.f64 1 (*.f64 (*.f64 2 (/.f64 l Om)) (hypot.f64 (sin.f64 kx) (sin.f64 ky)))))) 1)): 8 points increase in error, 8 points decrease in error
Applied egg-rr0.0
\[\leadsto \sqrt{0.5 + \color{blue}{\left(0 + \frac{0.5}{\mathsf{hypot}\left(1, \mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \left(2 \cdot \frac{\ell}{Om}\right)\right)}\right)}}
\]
Simplified0.0
\[\leadsto \sqrt{0.5 + \color{blue}{\frac{0.5}{\mathsf{hypot}\left(1, \mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \frac{2 \cdot \ell}{Om}\right)}}}
\]
Proof
(/.f64 1/2 (hypot.f64 1 (*.f64 (hypot.f64 (sin.f64 ky) (sin.f64 kx)) (/.f64 (*.f64 2 l) Om)))): 0 points increase in error, 0 points decrease in error
(/.f64 1/2 (hypot.f64 1 (*.f64 (hypot.f64 (sin.f64 ky) (sin.f64 kx)) (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 l Om)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (/.f64 1/2 (hypot.f64 1 (*.f64 (hypot.f64 (sin.f64 ky) (sin.f64 kx)) (*.f64 2 (/.f64 l Om))))))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, \mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \frac{2 \cdot \ell}{Om}\right)}}
\]