Initial program 76.3%
\[\begin{array}{l}
\mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\
\end{array}
\]
Applied rewrites76.3%
\[\leadsto \color{blue}{\begin{array}{l}
\color{blue}{\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
}
\end{array}}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites65.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites65.0%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites59.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor \color{blue}{0}\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites59.2%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor \color{blue}{0}\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites58.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor \color{blue}{0}\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites58.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor \color{blue}{0}\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites50.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor \color{blue}{0}\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor \color{blue}{0}\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites50.6%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor \color{blue}{0}\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites42.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor w\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites42.5%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites41.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Taylor expanded in undef-var around zero
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites41.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Step-by-step derivation
lift-fma.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor } \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
add-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor - \left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)} \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
sub-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)\right)\right)} \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor }\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left\lfloor 0\right\rfloor \cdot \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)}\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \color{blue}{\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)}\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(\color{blue}{\left(dX.u \cdot \left\lfloor 0\right\rfloor \right)} \cdot dX.u\right)\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \color{blue}{\left(dX.u \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)}\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(dX.u \cdot \color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)} \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
distribute-lft-neg-inN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites41.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\color{blue}{\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)} \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Step-by-step derivation
lift-fma.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor }\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
add-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor - \left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
sub-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \color{blue}{\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)\right)\right)}\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor }\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left\lfloor 0\right\rfloor \cdot \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)}\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \color{blue}{\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)}\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(\color{blue}{\left(dX.u \cdot \left\lfloor 0\right\rfloor \right)} \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \color{blue}{\left(dX.u \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)}\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(dX.u \cdot \color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)} \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
distribute-lft-neg-inN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)}\right)\right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites41.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \color{blue}{\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)}\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Step-by-step derivation
lift-fma.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
add-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor - \left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
sub-flipN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
*-commutativeN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(\left(dX.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(dX.u \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot \left(dX.u \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
associate-*l*N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
lift-*.f32N/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
distribute-lft-neg-inN/A
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \left(\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot dX.u\right)\right)\right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
Applied rewrites41.8%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right) \geq \mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right):\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot \left\lfloor 0\right\rfloor \right) \cdot dY.u, \left\lfloor 0\right\rfloor , \left(\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor 0\right\rfloor \right) \cdot \left\lfloor 0\right\rfloor \right)\right)}} \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\\
\end{array}
\]
- Add Preprocessing