Initial program 76.1%
\[\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}
\]
Step-by-step derivation
lift-+.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\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}
\]
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) + \color{blue}{\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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)}^{2}} + \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)}}^{2} + \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{\left(\color{blue}{\left\lfloor w\right\rfloor } \cdot dX.u\right)}^{2} + \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}
\]
unpow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot {dX.u}^{2}} + \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}} + \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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + \color{blue}{{\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}^{2}} \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\color{blue}{\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}}^{2} \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(\color{blue}{\left\lfloor h\right\rfloor } \cdot dX.v\right)}^{2} \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\color{blue}{\left(dX.v \cdot \left\lfloor h\right\rfloor \right)}}^{2} \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}
\]
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + \color{blue}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}} \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}
\]
+-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}} \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}
\]
sum-to-multN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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}
\]
Applied rewrites73.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}
\]
Step-by-step derivation
lift-+.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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) + \color{blue}{\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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)}^{2}} + \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)}}^{2} + \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\left\lfloor w\right\rfloor } \cdot dX.u\right)}^{2} + \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}
\]
unpow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{{\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot {dX.u}^{2}} + \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}} + \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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + \color{blue}{{\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}^{2}}, \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\color{blue}{\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}}^{2}, \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(\color{blue}{\left\lfloor h\right\rfloor } \cdot dX.v\right)}^{2}, \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\color{blue}{\left(dX.v \cdot \left\lfloor h\right\rfloor \right)}}^{2}, \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}
\]
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + \color{blue}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}, \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}
\]
+-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}, \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}
\]
sum-to-multN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\left(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\left(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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 rewrites67.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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
lift-+.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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)}^{2} + \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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)}^{2} + \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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)}^{2} + \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}
\]
unpow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \right)}^{2} \cdot {dX.u}^{2} + \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + \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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}^{2}, \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}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}^{2}, \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}
\]
lift-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(\left\lfloor h\right\rfloor \cdot dX.v\right)}^{2}, \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}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {\left(dX.v \cdot \left\lfloor h\right\rfloor \right)}^{2}, \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}
\]
pow-prod-downN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}, \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}
\]
+-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}, \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}
\]
sum-to-multN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{{dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}}{{dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}\right) \cdot \left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}\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 rewrites67.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 dX.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{1} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites61.9%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{1} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 dX.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{1} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites56.4%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(\color{blue}{1} \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 + \frac{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)}{\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)}\right) \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 dX.u around 0
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites62.3%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites59.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \color{blue}{\mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites59.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \color{blue}{\mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 rewrites53.1%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \cdot dY.u} \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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 rewrites42.3%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(\color{blue}{dY.u} \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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 rewrites42.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \mathsf{fma}\left(dY.v \cdot dY.v, \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \frac{\left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{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}
\]
pow2N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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-floor.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\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 \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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(\left(dY.v \cdot dY.v\right) \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \frac{\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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 rewrites32.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right) \geq \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\right)\right)\right) \cdot \left(dY.u \cdot dY.u\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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(1 \cdot \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot dX.v\right)\right), \left(dY.v \cdot \left(dY.v \cdot \left(\left\lfloor h\right\rfloor \cdot \frac{\left\lfloor h\right\rfloor }{dY.u \cdot dY.u}\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}
\]
- Add Preprocessing