Initial program 75.9%
\[\begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around inf
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \color{blue}{{dY.u}^{2} \cdot \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \color{blue}{{dY.u}^{2}}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \color{blue}{{dY.u}^{2}}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites72.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \color{blue}{\mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around inf
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \color{blue}{{dY.u}^{2} \cdot \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \color{blue}{{dY.u}^{2}}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \color{blue}{{dY.u}^{2}}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites72.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \color{blue}{\mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around inf
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), {dY.u}^{2} \cdot \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot {dY.u}^{2}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot {dY.u}^{2}\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites65.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(\color{blue}{dY.u} \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-/.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites53.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(\color{blue}{dY.u} \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(\color{blue}{dY.u} \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-/.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites57.4%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(\color{blue}{dY.u} \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right), \frac{dY.v}{dY.u \cdot dY.u}, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Step-by-step derivation
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{\left(dY.v \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{{dY.u}^{2}} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \frac{dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lift-/.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites51.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(\frac{dY.v}{dY.u \cdot dY.u} \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \cdot dY.v\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
Applied rewrites52.1%
\[\leadsto \color{blue}{\begin{array}{l}
\color{blue}{\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
}
\end{array}}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Step-by-step derivation
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Applied rewrites52.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Step-by-step derivation
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Applied rewrites54.4%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left(\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \frac{dY.v}{dY.u \cdot dY.u}\right)\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.u\right) \cdot dY.u\right)}}\\
\end{array}
\]
Taylor expanded in dY.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
Step-by-step derivation
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)}^{2}}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \frac{\left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v}{dY.u} \cdot dY.u\right)}}\\
\end{array}
\]
associate-*l/N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\frac{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right) \cdot dY.u\right)}}\\
\end{array}
\]
Applied rewrites57.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right) \geq \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u:\\
\;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\mathbf{else}:\\
\;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left\lfloor w\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), \left(\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\frac{\left\lfloor h\right\rfloor }{dY.u} \cdot dY.v\right)\right) \cdot dY.u\right)}}\\
\end{array}
\]
- Add Preprocessing