Initial program 79.1%
\[\begin{array}{l}
\mathbf{if}\;\left(\left\lfloorw\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dX.u\right) + \left(\left\lfloorh\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloorw\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right) + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloorw\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dX.u\right) + \left(\left\lfloorh\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dX.v\right), \left(\left\lfloorw\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right) + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloorw\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloorw\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dX.u\right) + \left(\left\lfloorh\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dX.v\right), \left(\left\lfloorw\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right) + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Simplified79.3%
\[\leadsto \color{blue}{\begin{array}{l}
\color{blue}{\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right), \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right)\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right), \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right)\right)}}\\
}
\end{array}}
\]
Applied egg-rr79.4%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right), \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right)\right)}}\\
\mathbf{else}:\\
\;\;\;\;\color{blue}{\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}}\\
\end{array}
\]
Applied egg-rr79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{\color{blue}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\end{array}
\]
Step-by-step derivation
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot \color{blue}{dY.u}}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)\right)}^{0.5}}\\
\end{array}
\]
hypot-udef79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \sqrt{\left(\left\lfloorw\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right) + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)} \cdot \mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)\right)}^{0.5}}\\
\end{array}
\]
pow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \sqrt{{\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)} \cdot \mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)\right)}^{0.5}}\\
\end{array}
\]
hypot-udef79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \sqrt{{\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)} \cdot \sqrt{\left(\left\lfloorw\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right) + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)}\right)\right)}^{0.5}}\\
\end{array}
\]
pow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \sqrt{{\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)} \cdot \sqrt{{\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)}\right)\right)}^{0.5}}\\
\end{array}
\]
add-sqr-sqrt79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot \color{blue}{dY.u}}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right)\right)\right)}^{0.5}}\\
\end{array}
\]
+-commutative79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot \color{blue}{dY.u}}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \left(\left\lfloorh\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloorh\right\rfloor \cdot dY.v\right) + {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)}^{0.5}}\\
\end{array}
\]
pow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\left\lfloorh\right\rfloor \cdot dY.v\right)}^{2} + {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)}^{0.5}}\\
\end{array}
\]
pow-prod-down79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\left\lfloorh\right\rfloor\right)}^{2} \cdot {dY.v}^{2} + {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)}^{0.5}}\\
\end{array}
\]
fma-def79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot \color{blue}{dY.u}}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
Applied egg-rr79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left\lfloorh\right\rfloor, \left(dX.v \cdot dX.v\right) \cdot \left\lfloorh\right\rfloor, \left\lfloorw\right\rfloor \cdot \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloorw\right\rfloor\right)\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, dY.u \cdot \left(\left\lfloorw\right\rfloor \cdot dY.u\right), \left\lfloorh\right\rfloor \cdot \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloorh\right\rfloor\right)\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot \color{blue}{dY.u}}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
Taylor expanded in h around 0 79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\mathsf{fma}\left(\left\lfloorh\right\rfloor, {dX.v}^{2} \cdot \left\lfloorh\right\rfloor, {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2}\right) \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right)}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
Step-by-step derivation
fma-udef79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left\lfloorh\right\rfloor \cdot \left({dX.v}^{2} \cdot \left\lfloorh\right\rfloor\right) + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2}} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left\lfloorh\right\rfloor \cdot \left(\color{blue}{\left(dX.v \cdot dX.v\right)} \cdot \left\lfloorh\right\rfloor\right) + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
associate-*l*79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left\lfloorh\right\rfloor \cdot \color{blue}{\left(dX.v \cdot \left(dX.v \cdot \left\lfloorh\right\rfloor\right)\right)} + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
associate-*l*79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(\left\lfloorh\right\rfloor \cdot dX.v\right) \cdot \left(dX.v \cdot \left\lfloorh\right\rfloor\right)} + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
*-commutative79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)} \cdot \left(dX.v \cdot \left\lfloorh\right\rfloor\right) + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2}} + {dX.u}^{2} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} + \color{blue}{\left(dX.u \cdot dX.u\right)} \cdot {\left(\left\lfloorw\right\rfloor\right)}^{2} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} + \left(dX.u \cdot dX.u\right) \cdot \color{blue}{\left(\left\lfloorw\right\rfloor \cdot \left\lfloorw\right\rfloor\right)} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
swap-sqr79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} + \color{blue}{\left(dX.u \cdot \left\lfloorw\right\rfloor\right) \cdot \left(dX.u \cdot \left\lfloorw\right\rfloor\right)} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
unpow279.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} + \color{blue}{{\left(dX.u \cdot \left\lfloorw\right\rfloor\right)}^{2}} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
+-commutative79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{\left(dX.u \cdot \left\lfloorw\right\rfloor\right)}^{2} + {\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2}} \geq \mathsf{fma}\left(\left\lfloorw\right\rfloor, {dY.u}^{2} \cdot \left\lfloorw\right\rfloor, {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}\right):\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
fma-udef79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.u \cdot \left\lfloorw\right\rfloor\right)}^{2} + {\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} \geq \color{blue}{\left\lfloorw\right\rfloor \cdot \left({dY.u}^{2} \cdot \left\lfloorw\right\rfloor\right) + {dY.v}^{2} \cdot {\left(\left\lfloorh\right\rfloor\right)}^{2}}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
Simplified79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{\left(dX.u \cdot \left\lfloorw\right\rfloor\right)}^{2} + {\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} \geq {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + {\left(\left\lfloorh\right\rfloor \cdot dY.v\right)}^{2}}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dX.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dX.u, \left\lfloorh\right\rfloor \cdot dX.v\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]
Final simplification79.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(dX.u \cdot \left\lfloorw\right\rfloor\right)}^{2} + {\left(dX.v \cdot \left\lfloorh\right\rfloor\right)}^{2} \geq {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2} + {\left(\left\lfloorh\right\rfloor \cdot dY.v\right)}^{2}:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloorw\right\rfloor}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(dX.u \cdot \left\lfloorw\right\rfloor, dX.v \cdot \left\lfloorh\right\rfloor\right)\right)}^{2}, {\left(\mathsf{hypot}\left(\left\lfloorw\right\rfloor \cdot dY.u, \left\lfloorh\right\rfloor \cdot dY.v\right)\right)}^{2}\right)\right)}^{0.5}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\left\lfloorw\right\rfloor \cdot dY.u}{{\left(\mathsf{max}\left({\left(\mathsf{hypot}\left(dX.u \cdot \left\lfloorw\right\rfloor, dX.v \cdot \left\lfloorh\right\rfloor\right)\right)}^{2}, \mathsf{fma}\left({\left(\left\lfloorh\right\rfloor\right)}^{2}, {dY.v}^{2}, {\left(\left\lfloorw\right\rfloor \cdot dY.u\right)}^{2}\right)\right)\right)}^{0.5}}\\
\end{array}
\]