Initial program 76.4%
\[\log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
Step-by-step derivation
lift--.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \color{blue}{\left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \color{blue}{\left(\left\lfloor h\right\rfloor \cdot dX.v\right)} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \color{blue}{\left\lfloor h\right\rfloor \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
fp-cancel-sub-sign-invN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)} + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)} + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left(\left\lfloor h\right\rfloor \cdot dY.v\right)} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right)} + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
distribute-lft-neg-inN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \color{blue}{\left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
distribute-rgt-neg-inN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \color{blue}{\left\lfloor h\right\rfloor \cdot \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
distribute-lft-outN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \left(\color{blue}{\left(dY.v \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u} + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
Applied rewrites76.4%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
Step-by-step derivation
lift--.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) - \left\lfloor h\right\rfloor \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
fp-cancel-sub-sign-invN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \right)\right) \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right|}{\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)}}\\
\end{array}
\]
distribute-lft-neg-inN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\mathsf{neg}\left(\left\lfloor h\right\rfloor \cdot \left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
distribute-rgt-neg-inN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left\lfloor h\right\rfloor \cdot \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
distribute-lft-outN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(dY.v \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
associate-*r*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \left(\left(dY.v \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u + \left(\mathsf{neg}\left(dX.v \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right)\right)\right)\right|}{\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)}}\\
\end{array}
\]
Applied rewrites76.4%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
Step-by-step derivation
lift-+.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
fabs-sqrN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\left|\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\left|\color{blue}{\left\lfloor w\right\rfloor \cdot \left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right)}\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\left|\color{blue}{\left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left\lfloor w\right\rfloor }\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
fabs-mulN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right| \cdot \left|\left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lower-fma.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{\mathsf{fma}\left(\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right|, \left|\left\lfloor w\right\rfloor \right|, \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
Applied rewrites70.6%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
Step-by-step derivation
lift-+.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
fabs-sqrN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\left|\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\left|\color{blue}{\left\lfloor w\right\rfloor \cdot \left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right)}\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\left|\color{blue}{\left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left\lfloor w\right\rfloor }\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
fabs-mulN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right| \cdot \left|\left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
lower-fma.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{\mathsf{fma}\left(\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right|, \left|\left\lfloor w\right\rfloor \right|, \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
Applied rewrites69.3%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
Step-by-step derivation
lift-+.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor } \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\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)}}\\
\end{array}
\]
fabs-sqrN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor } \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}}\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\left|\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\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)}}\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor \color{blue}{h}\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\left|\left\lfloor w\right\rfloor \cdot \left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right)\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)}}\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor \color{blue}{h}\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\left|\left(dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
fabs-mulN/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor } \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right| \cdot \left|\left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-fma.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right|, \left|\left\lfloor w\right\rfloor \right|, \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Applied rewrites71.0%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Taylor expanded in dX.u around inf
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Step-by-step derivation
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \color{blue}{\left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \color{blue}{\left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\color{blue}{\left|\left\lfloor w\right\rfloor \right|} \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \color{blue}{\left\lfloor w\right\rfloor }\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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor \color{blue}{w}\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f3260.1%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Applied rewrites60.1%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(\color{blue}{dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Taylor expanded in dX.u around inf
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Step-by-step derivation
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \color{blue}{\left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \color{blue}{\left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\color{blue}{\left|\left\lfloor w\right\rfloor \right|} \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \color{blue}{\left\lfloor w\right\rfloor }\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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor \color{blue}{w}\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f3256.4%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Applied rewrites56.4%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\color{blue}{dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left|dX.u\right| \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right), \left|\left\lfloor w\right\rfloor \right|, \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor \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)}}\\
\end{array}
\]
Taylor expanded in dX.u around inf
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
Step-by-step derivation
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \color{blue}{\mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , \color{blue}{dX.u}, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-*.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-fabs.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f32N/A
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
lower-floor.f3259.7%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
Applied rewrites59.7%
\[\leadsto \log_{2} \begin{array}{l}
\mathbf{if}\;\frac{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}{\left|\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)\right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\color{blue}{\left\lfloor h\right\rfloor \cdot \mathsf{fma}\left(dY.v \cdot \left\lfloor w\right\rfloor , dX.u, \left(dY.u \cdot dX.v\right) \cdot \left(-\left\lfloor w\right\rfloor \right)\right)}\right|}{\sqrt{\mathsf{max}\left(dX.u \cdot \left(\left|dX.u\right| \cdot \left(\left|\left\lfloor w\right\rfloor \right| \cdot \left\lfloor w\right\rfloor \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)}}\\
\end{array}
\]
Applied rewrites64.4%
\[\leadsto \log_{2} \color{blue}{\begin{array}{l}
\color{blue}{\mathbf{if}\;\frac{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot dY.v, \left\lfloor h\right\rfloor \cdot dY.v, \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right), \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)}{\left|\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.v - \left(dX.v \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left\lfloor h\right\rfloor \right|} > \left\lfloor maxAniso\right\rfloor :\\
\;\;\;\;\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot dY.v, \left\lfloor h\right\rfloor \cdot dY.v, \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right), \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)}}{\left\lfloor maxAniso\right\rfloor }\\
\mathbf{else}:\\
\;\;\;\;\frac{\left|\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.v - \left(dX.v \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left\lfloor h\right\rfloor \right|}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloor h\right\rfloor \cdot dY.v, \left\lfloor h\right\rfloor \cdot dY.v, \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\right), \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)}}\\
}
\end{array}}
\]
- Add Preprocessing