Anisotropic x16 LOD (line direction, v)

Percentage Accurate: 75.4% → 75.5%

Time: 18.2s

Alternatives: 6

Speedup: N/A×

Specification

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_2 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_3 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_1 \cdot t\_1 + t\_4 \cdot t\_4\\ t_6 := \frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}}\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;t\_6 \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot t\_4\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (* (floor w) dY.u))
        (t_2 (* (floor w) dX.u))
        (t_3 (+ (* t_2 t_2) (* t_0 t_0)))
        (t_4 (* (floor h) dY.v))
        (t_5 (+ (* t_1 t_1) (* t_4 t_4)))
        (t_6 (/ 1.0 (sqrt (fmax t_3 t_5)))))
   (if (>= t_3 t_5) (* t_6 t_0) (* t_6 t_4))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = floorf(w) * dY_46_u;
	float t_2 = floorf(w) * dX_46_u;
	float t_3 = (t_2 * t_2) + (t_0 * t_0);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_1 * t_1) + (t_4 * t_4);
	float t_6 = 1.0f / sqrtf(fmaxf(t_3, t_5));
	float tmp;
	if (t_3 >= t_5) {
		tmp = t_6 * t_0;
	} else {
		tmp = t_6 * t_4;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = Float32(floor(w) * dY_46_u)
	t_2 = Float32(floor(w) * dX_46_u)
	t_3 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_1 * t_1) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(1.0) / sqrt(fmax(t_3, t_5)))
	tmp = Float32(0.0)
	if (t_3 >= t_5)
		tmp = Float32(t_6 * t_0);
	else
		tmp = Float32(t_6 * t_4);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(w) * dY_46_u;
	t_2 = floor(w) * dX_46_u;
	t_3 = (t_2 * t_2) + (t_0 * t_0);
	t_4 = floor(h) * dY_46_v;
	t_5 = (t_1 * t_1) + (t_4 * t_4);
	t_6 = single(1.0) / sqrt(max(t_3, t_5));
	tmp = single(0.0);
	if (t_3 >= t_5)
		tmp = t_6 * t_0;
	else
		tmp = t_6 * t_4;
	end
	tmp_2 = tmp;
end

Initial Program: 75.4% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_2 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_3 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_1 \cdot t\_1 + t\_4 \cdot t\_4\\ t_6 := \frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}}\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;t\_6 \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot t\_4\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (* (floor w) dY.u))
        (t_2 (* (floor w) dX.u))
        (t_3 (+ (* t_2 t_2) (* t_0 t_0)))
        (t_4 (* (floor h) dY.v))
        (t_5 (+ (* t_1 t_1) (* t_4 t_4)))
        (t_6 (/ 1.0 (sqrt (fmax t_3 t_5)))))
   (if (>= t_3 t_5) (* t_6 t_0) (* t_6 t_4))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = floorf(w) * dY_46_u;
	float t_2 = floorf(w) * dX_46_u;
	float t_3 = (t_2 * t_2) + (t_0 * t_0);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_1 * t_1) + (t_4 * t_4);
	float t_6 = 1.0f / sqrtf(fmaxf(t_3, t_5));
	float tmp;
	if (t_3 >= t_5) {
		tmp = t_6 * t_0;
	} else {
		tmp = t_6 * t_4;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = Float32(floor(w) * dY_46_u)
	t_2 = Float32(floor(w) * dX_46_u)
	t_3 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_1 * t_1) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(1.0) / sqrt(fmax(t_3, t_5)))
	tmp = Float32(0.0)
	if (t_3 >= t_5)
		tmp = Float32(t_6 * t_0);
	else
		tmp = Float32(t_6 * t_4);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(w) * dY_46_u;
	t_2 = floor(w) * dX_46_u;
	t_3 = (t_2 * t_2) + (t_0 * t_0);
	t_4 = floor(h) * dY_46_v;
	t_5 = (t_1 * t_1) + (t_4 * t_4);
	t_6 = single(1.0) / sqrt(max(t_3, t_5));
	tmp = single(0.0);
	if (t_3 >= t_5)
		tmp = t_6 * t_0;
	else
		tmp = t_6 * t_4;
	end
	tmp_2 = tmp;
end

Alternative 1: 75.5% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ t_2 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_3 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_4 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_5 := -1 \cdot \left\lfloor w\right\rfloor \\ t_6 := t\_5 \cdot dY.u\\ t_7 := t\_6 \cdot t\_6 + t\_3 \cdot t\_3\\ \mathbf{if}\;t\_4 \geq t\_7:\\ \;\;\;\;\frac{t\_0}{\sqrt{\mathsf{max}\left(\left(t\_1 \cdot dX.v\right) \cdot dX.v - \left(t\_2 \cdot t\_5\right) \cdot \left(-1 \cdot dX.u\right), \left(t\_1 \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_4, t\_7\right)}} \cdot t\_3\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor h) 2.0))
        (t_2 (* -1.0 (* (floor w) dX.u)))
        (t_3 (* (floor h) dY.v))
        (t_4 (+ (* t_2 t_2) (* t_0 t_0)))
        (t_5 (* -1.0 (floor w)))
        (t_6 (* t_5 dY.u))
        (t_7 (+ (* t_6 t_6) (* t_3 t_3))))
   (if (>= t_4 t_7)
     (/
      t_0
      (sqrt
       (fmax
        (- (* (* t_1 dX.v) dX.v) (* (* t_2 t_5) (* -1.0 dX.u)))
        (-
         (* (* t_1 dY.v) dY.v)
         (* (* -1.0 (* dY.u (pow (floor w) 2.0))) dY.u)))))
     (* (/ 1.0 (sqrt (fmax t_4 t_7))) t_3))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(h), 2.0f);
	float t_2 = -1.0f * (floorf(w) * dX_46_u);
	float t_3 = floorf(h) * dY_46_v;
	float t_4 = (t_2 * t_2) + (t_0 * t_0);
	float t_5 = -1.0f * floorf(w);
	float t_6 = t_5 * dY_46_u;
	float t_7 = (t_6 * t_6) + (t_3 * t_3);
	float tmp;
	if (t_4 >= t_7) {
		tmp = t_0 / sqrtf(fmaxf((((t_1 * dX_46_v) * dX_46_v) - ((t_2 * t_5) * (-1.0f * dX_46_u))), (((t_1 * dY_46_v) * dY_46_v) - ((-1.0f * (dY_46_u * powf(floorf(w), 2.0f))) * dY_46_u))));
	} else {
		tmp = (1.0f / sqrtf(fmaxf(t_4, t_7))) * t_3;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(h) ^ Float32(2.0)
	t_2 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_3 = Float32(floor(h) * dY_46_v)
	t_4 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_5 = Float32(Float32(-1.0) * floor(w))
	t_6 = Float32(t_5 * dY_46_u)
	t_7 = Float32(Float32(t_6 * t_6) + Float32(t_3 * t_3))
	tmp = Float32(0.0)
	if (t_4 >= t_7)
		tmp = Float32(t_0 / sqrt(fmax(Float32(Float32(Float32(t_1 * dX_46_v) * dX_46_v) - Float32(Float32(t_2 * t_5) * Float32(Float32(-1.0) * dX_46_u))), Float32(Float32(Float32(t_1 * dY_46_v) * dY_46_v) - Float32(Float32(Float32(-1.0) * Float32(dY_46_u * (floor(w) ^ Float32(2.0)))) * dY_46_u)))));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(t_4, t_7))) * t_3);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(h) ^ single(2.0);
	t_2 = single(-1.0) * (floor(w) * dX_46_u);
	t_3 = floor(h) * dY_46_v;
	t_4 = (t_2 * t_2) + (t_0 * t_0);
	t_5 = single(-1.0) * floor(w);
	t_6 = t_5 * dY_46_u;
	t_7 = (t_6 * t_6) + (t_3 * t_3);
	tmp = single(0.0);
	if (t_4 >= t_7)
		tmp = t_0 / sqrt(max((((t_1 * dX_46_v) * dX_46_v) - ((t_2 * t_5) * (single(-1.0) * dX_46_u))), (((t_1 * dY_46_v) * dY_46_v) - ((single(-1.0) * (dY_46_u * (floor(w) ^ single(2.0)))) * dY_46_u))));
	else
		tmp = (single(1.0) / sqrt(max(t_4, t_7))) * t_3;
	end
	tmp_2 = tmp;
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]
5. Step-by-step derivation

   1. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   2. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\color{blue}{\left(\left\lfloor w\right\rfloor \right)}}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   3. lift-pow.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{{\left(\left\lfloor w\right\rfloor \right)}^{2}}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   4. unpow2 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   5. associate-*r* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   6. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   7. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\color{blue}{\left\lfloor w\right\rfloor } \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   8. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   9. lower-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   10. lift-floor.f32 76.8

       \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \color{blue}{\left\lfloor w\right\rfloor }\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

6. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

7. Final simplification 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot 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{\left\lfloor h\right\rfloor \cdot dX.v}{\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left\lfloor w\right\rfloor \right)\right) \cdot \left(-1 \cdot dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.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} \]
8. Add Preprocessing

Alternative 2: 75.5% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ t_2 := \left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\\ t_3 := {\left(\left\lfloor w\right\rfloor \right)}^{2}\\ t_4 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_5 := \left\lfloor h\right\rfloor \cdot dY.v\\ \mathbf{if}\;t\_4 \cdot t\_4 + t\_0 \cdot t\_0 \geq t\_2 \cdot t\_2 + t\_5 \cdot t\_5:\\ \;\;\;\;\frac{t\_0}{\sqrt{\mathsf{max}\left(\left(t\_1 \cdot dX.v\right) \cdot dX.v - \left(-1 \cdot \left(dX.u \cdot t\_3\right)\right) \cdot dX.u, \left(t\_1 \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot t\_3\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot -1}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot t\_1 - \left(\left(t\_3 \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot t\_1 - \left(\left(t\_3 \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)} \cdot -1}\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor h) 2.0))
        (t_2 (* (* -1.0 (floor w)) dY.u))
        (t_3 (pow (floor w) 2.0))
        (t_4 (* -1.0 (* (floor w) dX.u)))
        (t_5 (* (floor h) dY.v)))
   (if (>= (+ (* t_4 t_4) (* t_0 t_0)) (+ (* t_2 t_2) (* t_5 t_5)))
     (/
      t_0
      (sqrt
       (fmax
        (- (* (* t_1 dX.v) dX.v) (* (* -1.0 (* dX.u t_3)) dX.u))
        (- (* (* t_1 dY.v) dY.v) (* (* -1.0 (* dY.u t_3)) dY.u)))))
     (/
      (* (* dY.v (floor h)) -1.0)
      (*
       (sqrt
        (fmax
         (- (* (* dX.v dX.v) t_1) (* (* (* t_3 dX.u) dX.u) -1.0))
         (- (* (* dY.v dY.v) t_1) (* (* (* t_3 dY.u) dY.u) -1.0))))
       -1.0)))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(h), 2.0f);
	float t_2 = (-1.0f * floorf(w)) * dY_46_u;
	float t_3 = powf(floorf(w), 2.0f);
	float t_4 = -1.0f * (floorf(w) * dX_46_u);
	float t_5 = floorf(h) * dY_46_v;
	float tmp;
	if (((t_4 * t_4) + (t_0 * t_0)) >= ((t_2 * t_2) + (t_5 * t_5))) {
		tmp = t_0 / sqrtf(fmaxf((((t_1 * dX_46_v) * dX_46_v) - ((-1.0f * (dX_46_u * t_3)) * dX_46_u)), (((t_1 * dY_46_v) * dY_46_v) - ((-1.0f * (dY_46_u * t_3)) * dY_46_u))));
	} else {
		tmp = ((dY_46_v * floorf(h)) * -1.0f) / (sqrtf(fmaxf((((dX_46_v * dX_46_v) * t_1) - (((t_3 * dX_46_u) * dX_46_u) * -1.0f)), (((dY_46_v * dY_46_v) * t_1) - (((t_3 * dY_46_u) * dY_46_u) * -1.0f)))) * -1.0f);
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(h) ^ Float32(2.0)
	t_2 = Float32(Float32(Float32(-1.0) * floor(w)) * dY_46_u)
	t_3 = floor(w) ^ Float32(2.0)
	t_4 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_5 = Float32(floor(h) * dY_46_v)
	tmp = Float32(0.0)
	if (Float32(Float32(t_4 * t_4) + Float32(t_0 * t_0)) >= Float32(Float32(t_2 * t_2) + Float32(t_5 * t_5)))
		tmp = Float32(t_0 / sqrt(fmax(Float32(Float32(Float32(t_1 * dX_46_v) * dX_46_v) - Float32(Float32(Float32(-1.0) * Float32(dX_46_u * t_3)) * dX_46_u)), Float32(Float32(Float32(t_1 * dY_46_v) * dY_46_v) - Float32(Float32(Float32(-1.0) * Float32(dY_46_u * t_3)) * dY_46_u)))));
	else
		tmp = Float32(Float32(Float32(dY_46_v * floor(h)) * Float32(-1.0)) / Float32(sqrt(fmax(Float32(Float32(Float32(dX_46_v * dX_46_v) * t_1) - Float32(Float32(Float32(t_3 * dX_46_u) * dX_46_u) * Float32(-1.0))), Float32(Float32(Float32(dY_46_v * dY_46_v) * t_1) - Float32(Float32(Float32(t_3 * dY_46_u) * dY_46_u) * Float32(-1.0))))) * Float32(-1.0)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(h) ^ single(2.0);
	t_2 = (single(-1.0) * floor(w)) * dY_46_u;
	t_3 = floor(w) ^ single(2.0);
	t_4 = single(-1.0) * (floor(w) * dX_46_u);
	t_5 = floor(h) * dY_46_v;
	tmp = single(0.0);
	if (((t_4 * t_4) + (t_0 * t_0)) >= ((t_2 * t_2) + (t_5 * t_5)))
		tmp = t_0 / sqrt(max((((t_1 * dX_46_v) * dX_46_v) - ((single(-1.0) * (dX_46_u * t_3)) * dX_46_u)), (((t_1 * dY_46_v) * dY_46_v) - ((single(-1.0) * (dY_46_u * t_3)) * dY_46_u))));
	else
		tmp = ((dY_46_v * floor(h)) * single(-1.0)) / (sqrt(max((((dX_46_v * dX_46_v) * t_1) - (((t_3 * dX_46_u) * dX_46_u) * single(-1.0))), (((dY_46_v * dY_46_v) * t_1) - (((t_3 * dY_46_u) * dY_46_u) * single(-1.0))))) * single(-1.0));
	end
	tmp_2 = tmp;
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

6. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(dY.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \right) \cdot -1}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)} \cdot -1}\\ \end{array} \]

7. Final simplification 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot 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{\left\lfloor h\right\rfloor \cdot dX.v}{\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(-1 \cdot \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dX.u, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot -1}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)} \cdot -1}\\ \end{array} \]
8. Add Preprocessing

Alternative 3: 75.4% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ t_2 := \left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\\ t_3 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_2 \cdot t\_2 + t\_4 \cdot t\_4\\ t_6 := t\_3 \cdot t\_3 + t\_0 \cdot t\_0\\ t_7 := {\left(\left\lfloor w\right\rfloor \right)}^{2}\\ \mathbf{if}\;t\_6 \geq t\_5:\\ \;\;\;\;\frac{t\_0}{\sqrt{\mathsf{max}\left(\left(t\_1 \cdot dX.v\right) \cdot dX.v - \left(-1 \cdot \left(dX.u \cdot t\_7\right)\right) \cdot dX.u, \left(t\_1 \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot t\_7\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_6, t\_5\right)}} \cdot t\_4\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor h) 2.0))
        (t_2 (* (* -1.0 (floor w)) dY.u))
        (t_3 (* -1.0 (* (floor w) dX.u)))
        (t_4 (* (floor h) dY.v))
        (t_5 (+ (* t_2 t_2) (* t_4 t_4)))
        (t_6 (+ (* t_3 t_3) (* t_0 t_0)))
        (t_7 (pow (floor w) 2.0)))
   (if (>= t_6 t_5)
     (/
      t_0
      (sqrt
       (fmax
        (- (* (* t_1 dX.v) dX.v) (* (* -1.0 (* dX.u t_7)) dX.u))
        (- (* (* t_1 dY.v) dY.v) (* (* -1.0 (* dY.u t_7)) dY.u)))))
     (* (/ 1.0 (sqrt (fmax t_6 t_5))) t_4))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(h), 2.0f);
	float t_2 = (-1.0f * floorf(w)) * dY_46_u;
	float t_3 = -1.0f * (floorf(w) * dX_46_u);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_2 * t_2) + (t_4 * t_4);
	float t_6 = (t_3 * t_3) + (t_0 * t_0);
	float t_7 = powf(floorf(w), 2.0f);
	float tmp;
	if (t_6 >= t_5) {
		tmp = t_0 / sqrtf(fmaxf((((t_1 * dX_46_v) * dX_46_v) - ((-1.0f * (dX_46_u * t_7)) * dX_46_u)), (((t_1 * dY_46_v) * dY_46_v) - ((-1.0f * (dY_46_u * t_7)) * dY_46_u))));
	} else {
		tmp = (1.0f / sqrtf(fmaxf(t_6, t_5))) * t_4;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(h) ^ Float32(2.0)
	t_2 = Float32(Float32(Float32(-1.0) * floor(w)) * dY_46_u)
	t_3 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_2 * t_2) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(t_3 * t_3) + Float32(t_0 * t_0))
	t_7 = floor(w) ^ Float32(2.0)
	tmp = Float32(0.0)
	if (t_6 >= t_5)
		tmp = Float32(t_0 / sqrt(fmax(Float32(Float32(Float32(t_1 * dX_46_v) * dX_46_v) - Float32(Float32(Float32(-1.0) * Float32(dX_46_u * t_7)) * dX_46_u)), Float32(Float32(Float32(t_1 * dY_46_v) * dY_46_v) - Float32(Float32(Float32(-1.0) * Float32(dY_46_u * t_7)) * dY_46_u)))));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(t_6, t_5))) * t_4);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(h) ^ single(2.0);
	t_2 = (single(-1.0) * floor(w)) * dY_46_u;
	t_3 = single(-1.0) * (floor(w) * dX_46_u);
	t_4 = floor(h) * dY_46_v;
	t_5 = (t_2 * t_2) + (t_4 * t_4);
	t_6 = (t_3 * t_3) + (t_0 * t_0);
	t_7 = floor(w) ^ single(2.0);
	tmp = single(0.0);
	if (t_6 >= t_5)
		tmp = t_0 / sqrt(max((((t_1 * dX_46_v) * dX_46_v) - ((single(-1.0) * (dX_46_u * t_7)) * dX_46_u)), (((t_1 * dY_46_v) * dY_46_v) - ((single(-1.0) * (dY_46_u * t_7)) * dY_46_u))));
	else
		tmp = (single(1.0) / sqrt(max(t_6, t_5))) * t_4;
	end
	tmp_2 = tmp;
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

5. Final simplification 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot 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{\left\lfloor h\right\rfloor \cdot dX.v}{\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(-1 \cdot \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dX.u, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(-1 \cdot \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right) \cdot dY.u\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.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} \]
6. Add Preprocessing

Alternative 4: 75.4% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ t_2 := \left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\\ t_3 := {\left(\left\lfloor w\right\rfloor \right)}^{2}\\ t_4 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_5 := t\_4 \cdot t\_4 + t\_0 \cdot t\_0\\ t_6 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_7 := t\_2 \cdot t\_2 + t\_6 \cdot t\_6\\ \mathbf{if}\;t\_5 \geq t\_7:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dX.v}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot t\_1 - \left(\left(t\_3 \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot t\_1 - \left(\left(t\_3 \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_5, t\_7\right)}} \cdot t\_6\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor h) 2.0))
        (t_2 (* (* -1.0 (floor w)) dY.u))
        (t_3 (pow (floor w) 2.0))
        (t_4 (* -1.0 (* (floor w) dX.u)))
        (t_5 (+ (* t_4 t_4) (* t_0 t_0)))
        (t_6 (* (floor h) dY.v))
        (t_7 (+ (* t_2 t_2) (* t_6 t_6))))
   (if (>= t_5 t_7)
     (*
      (floor h)
      (/
       dX.v
       (sqrt
        (fmax
         (- (* (* dX.v dX.v) t_1) (* (* (* t_3 dX.u) dX.u) -1.0))
         (- (* (* dY.v dY.v) t_1) (* (* (* t_3 dY.u) dY.u) -1.0))))))
     (* (/ 1.0 (sqrt (fmax t_5 t_7))) t_6))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(h), 2.0f);
	float t_2 = (-1.0f * floorf(w)) * dY_46_u;
	float t_3 = powf(floorf(w), 2.0f);
	float t_4 = -1.0f * (floorf(w) * dX_46_u);
	float t_5 = (t_4 * t_4) + (t_0 * t_0);
	float t_6 = floorf(h) * dY_46_v;
	float t_7 = (t_2 * t_2) + (t_6 * t_6);
	float tmp;
	if (t_5 >= t_7) {
		tmp = floorf(h) * (dX_46_v / sqrtf(fmaxf((((dX_46_v * dX_46_v) * t_1) - (((t_3 * dX_46_u) * dX_46_u) * -1.0f)), (((dY_46_v * dY_46_v) * t_1) - (((t_3 * dY_46_u) * dY_46_u) * -1.0f)))));
	} else {
		tmp = (1.0f / sqrtf(fmaxf(t_5, t_7))) * t_6;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(h) ^ Float32(2.0)
	t_2 = Float32(Float32(Float32(-1.0) * floor(w)) * dY_46_u)
	t_3 = floor(w) ^ Float32(2.0)
	t_4 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_5 = Float32(Float32(t_4 * t_4) + Float32(t_0 * t_0))
	t_6 = Float32(floor(h) * dY_46_v)
	t_7 = Float32(Float32(t_2 * t_2) + Float32(t_6 * t_6))
	tmp = Float32(0.0)
	if (t_5 >= t_7)
		tmp = Float32(floor(h) * Float32(dX_46_v / sqrt(fmax(Float32(Float32(Float32(dX_46_v * dX_46_v) * t_1) - Float32(Float32(Float32(t_3 * dX_46_u) * dX_46_u) * Float32(-1.0))), Float32(Float32(Float32(dY_46_v * dY_46_v) * t_1) - Float32(Float32(Float32(t_3 * dY_46_u) * dY_46_u) * Float32(-1.0)))))));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(t_5, t_7))) * t_6);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(h) ^ single(2.0);
	t_2 = (single(-1.0) * floor(w)) * dY_46_u;
	t_3 = floor(w) ^ single(2.0);
	t_4 = single(-1.0) * (floor(w) * dX_46_u);
	t_5 = (t_4 * t_4) + (t_0 * t_0);
	t_6 = floor(h) * dY_46_v;
	t_7 = (t_2 * t_2) + (t_6 * t_6);
	tmp = single(0.0);
	if (t_5 >= t_7)
		tmp = floor(h) * (dX_46_v / sqrt(max((((dX_46_v * dX_46_v) * t_1) - (((t_3 * dX_46_u) * dX_46_u) * single(-1.0))), (((dY_46_v * dY_46_v) * t_1) - (((t_3 * dY_46_u) * dY_46_u) * single(-1.0))))));
	else
		tmp = (single(1.0) / sqrt(max(t_5, t_7))) * t_6;
	end
	tmp_2 = tmp;
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

6. Applied rewrites 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\left\lfloor h\right\rfloor \cdot \frac{-1 \cdot dX.v}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)} \cdot -1}}\\ \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} \]

7. Final simplification 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dX.v}{\sqrt{\mathsf{max}\left(\left(dX.v \cdot dX.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u\right) \cdot -1, \left(dY.v \cdot dY.v\right) \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.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} \]
8. Add Preprocessing

Alternative 5: 75.4% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor w\right\rfloor \right)}^{2}\\ t_2 := \left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\\ t_3 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_2 \cdot t\_2 + t\_4 \cdot t\_4\\ t_6 := t\_3 \cdot t\_3 + t\_0 \cdot t\_0\\ t_7 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ \mathbf{if}\;t\_6 \geq t\_5:\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left(t\_1 \cdot dX.u\right) \cdot dX.u, 1, \left(t\_7 \cdot dX.v\right) \cdot dX.v\right), \left(t\_7 \cdot dY.v\right) \cdot dY.v - \left(\left(t\_1 \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_6, t\_5\right)}} \cdot t\_4\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor w) 2.0))
        (t_2 (* (* -1.0 (floor w)) dY.u))
        (t_3 (* -1.0 (* (floor w) dX.u)))
        (t_4 (* (floor h) dY.v))
        (t_5 (+ (* t_2 t_2) (* t_4 t_4)))
        (t_6 (+ (* t_3 t_3) (* t_0 t_0)))
        (t_7 (pow (floor h) 2.0)))
   (if (>= t_6 t_5)
     (*
      (pow
       (fmax
        (fma (* (* t_1 dX.u) dX.u) 1.0 (* (* t_7 dX.v) dX.v))
        (- (* (* t_7 dY.v) dY.v) (* (* (* t_1 dY.u) dY.u) -1.0)))
       -0.5)
      (* dX.v (floor h)))
     (* (/ 1.0 (sqrt (fmax t_6 t_5))) t_4))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(w), 2.0f);
	float t_2 = (-1.0f * floorf(w)) * dY_46_u;
	float t_3 = -1.0f * (floorf(w) * dX_46_u);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_2 * t_2) + (t_4 * t_4);
	float t_6 = (t_3 * t_3) + (t_0 * t_0);
	float t_7 = powf(floorf(h), 2.0f);
	float tmp;
	if (t_6 >= t_5) {
		tmp = powf(fmaxf(fmaf(((t_1 * dX_46_u) * dX_46_u), 1.0f, ((t_7 * dX_46_v) * dX_46_v)), (((t_7 * dY_46_v) * dY_46_v) - (((t_1 * dY_46_u) * dY_46_u) * -1.0f))), -0.5f) * (dX_46_v * floorf(h));
	} else {
		tmp = (1.0f / sqrtf(fmaxf(t_6, t_5))) * t_4;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(w) ^ Float32(2.0)
	t_2 = Float32(Float32(Float32(-1.0) * floor(w)) * dY_46_u)
	t_3 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_2 * t_2) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(t_3 * t_3) + Float32(t_0 * t_0))
	t_7 = floor(h) ^ Float32(2.0)
	tmp = Float32(0.0)
	if (t_6 >= t_5)
		tmp = Float32((fmax(fma(Float32(Float32(t_1 * dX_46_u) * dX_46_u), Float32(1.0), Float32(Float32(t_7 * dX_46_v) * dX_46_v)), Float32(Float32(Float32(t_7 * dY_46_v) * dY_46_v) - Float32(Float32(Float32(t_1 * dY_46_u) * dY_46_u) * Float32(-1.0)))) ^ Float32(-0.5)) * Float32(dX_46_v * floor(h)));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(t_6, t_5))) * t_4);
	end
	return tmp
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]
5. Step-by-step derivation

   1. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   2. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\color{blue}{\left(\left\lfloor w\right\rfloor \right)}}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   3. lift-pow.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{{\left(\left\lfloor w\right\rfloor \right)}^{2}}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   4. unpow2 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   5. associate-*r* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   6. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   7. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\color{blue}{\left\lfloor w\right\rfloor } \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   8. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   9. lower-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   10. lift-floor.f32 76.8

       \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \color{blue}{\left\lfloor w\right\rfloor }\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

6. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

7. Taylor expanded in w around 0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot \sqrt{\frac{1}{\mathsf{max}\left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - -1 \cdot \left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right), {dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - -1 \cdot \left({dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\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} \]

9. Applied rewrites 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \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} \]

10. Final simplification 76.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.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} \]
11. Add Preprocessing

Alternative 6: 68.5% accurate, N/A× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := {\left(\left\lfloor w\right\rfloor \right)}^{2}\\ t_2 := -1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ t_3 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_4 := \left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\\ t_5 := {\left(\left\lfloor w\right\rfloor \right)}^{1}\\ t_6 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_7 := {\left(\left\lfloor h\right\rfloor \right)}^{2}\\ \mathbf{if}\;t\_6 \geq t\_4 \cdot t\_4 + t\_3 \cdot t\_3:\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left(t\_1 \cdot dX.u\right) \cdot dX.u, 1, \left(t\_7 \cdot dX.v\right) \cdot dX.v\right), \left(t\_7 \cdot dY.v\right) \cdot dY.v - \left(\left(t\_1 \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_6, \mathsf{fma}\left(t\_5, t\_5, \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot t\_3\\ \end{array} \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
 :precision binary32
 (let* ((t_0 (* (floor h) dX.v))
        (t_1 (pow (floor w) 2.0))
        (t_2 (* -1.0 (* (floor w) dX.u)))
        (t_3 (* (floor h) dY.v))
        (t_4 (* (* -1.0 (floor w)) dY.u))
        (t_5 (pow (floor w) 1.0))
        (t_6 (+ (* t_2 t_2) (* t_0 t_0)))
        (t_7 (pow (floor h) 2.0)))
   (if (>= t_6 (+ (* t_4 t_4) (* t_3 t_3)))
     (*
      (pow
       (fmax
        (fma (* (* t_1 dX.u) dX.u) 1.0 (* (* t_7 dX.v) dX.v))
        (- (* (* t_7 dY.v) dY.v) (* (* (* t_1 dY.u) dY.u) -1.0)))
       -0.5)
      (* dX.v (floor h)))
     (*
      (/
       1.0
       (sqrt
        (fmax
         t_6
         (*
          (fma t_5 t_5 (/ (pow (* dY.v (floor h)) 2.0) (* dY.u dY.u)))
          (* dY.u dY.u)))))
      t_3))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = powf(floorf(w), 2.0f);
	float t_2 = -1.0f * (floorf(w) * dX_46_u);
	float t_3 = floorf(h) * dY_46_v;
	float t_4 = (-1.0f * floorf(w)) * dY_46_u;
	float t_5 = powf(floorf(w), 1.0f);
	float t_6 = (t_2 * t_2) + (t_0 * t_0);
	float t_7 = powf(floorf(h), 2.0f);
	float tmp;
	if (t_6 >= ((t_4 * t_4) + (t_3 * t_3))) {
		tmp = powf(fmaxf(fmaf(((t_1 * dX_46_u) * dX_46_u), 1.0f, ((t_7 * dX_46_v) * dX_46_v)), (((t_7 * dY_46_v) * dY_46_v) - (((t_1 * dY_46_u) * dY_46_u) * -1.0f))), -0.5f) * (dX_46_v * floorf(h));
	} else {
		tmp = (1.0f / sqrtf(fmaxf(t_6, (fmaf(t_5, t_5, (powf((dY_46_v * floorf(h)), 2.0f) / (dY_46_u * dY_46_u))) * (dY_46_u * dY_46_u))))) * t_3;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = floor(w) ^ Float32(2.0)
	t_2 = Float32(Float32(-1.0) * Float32(floor(w) * dX_46_u))
	t_3 = Float32(floor(h) * dY_46_v)
	t_4 = Float32(Float32(Float32(-1.0) * floor(w)) * dY_46_u)
	t_5 = floor(w) ^ Float32(1.0)
	t_6 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_7 = floor(h) ^ Float32(2.0)
	tmp = Float32(0.0)
	if (t_6 >= Float32(Float32(t_4 * t_4) + Float32(t_3 * t_3)))
		tmp = Float32((fmax(fma(Float32(Float32(t_1 * dX_46_u) * dX_46_u), Float32(1.0), Float32(Float32(t_7 * dX_46_v) * dX_46_v)), Float32(Float32(Float32(t_7 * dY_46_v) * dY_46_v) - Float32(Float32(Float32(t_1 * dY_46_u) * dY_46_u) * Float32(-1.0)))) ^ Float32(-0.5)) * Float32(dX_46_v * floor(h)));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(t_6, Float32(fma(t_5, t_5, Float32((Float32(dY_46_v * floor(h)) ^ Float32(2.0)) / Float32(dY_46_u * dY_46_u))) * Float32(dY_46_u * dY_46_u))))) * t_3);
	end
	return tmp
end

Derivation

1. Initial program 76.7%

   \[\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} \]
2. Add Preprocessing

4. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\frac{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]
5. Step-by-step derivation

   1. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(dX.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   2. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot {\color{blue}{\left(\left\lfloor w\right\rfloor \right)}}^{2}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   3. lift-pow.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{{\left(\left\lfloor w\right\rfloor \right)}^{2}}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   4. unpow2 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(dX.u \cdot \color{blue}{\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)}\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   5. associate-*r* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   6. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   7. lift-floor.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\color{blue}{\left\lfloor w\right\rfloor } \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   8. lift-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\color{blue}{\left(\left\lfloor w\right\rfloor \cdot dX.u\right)} \cdot \left\lfloor w\right\rfloor \right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   9. lower-*.f32 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

   10. lift-floor.f32 76.8

       \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \color{blue}{\left\lfloor w\right\rfloor }\right) \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

6. Applied rewrites 76.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot 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{\left(\left(1 \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot -1}{-\sqrt{\mathsf{max}\left(\left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v - \color{blue}{\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right)} \cdot \left(-dX.u\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(dY.u \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot \left(-dY.u\right)\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} \]

7. Taylor expanded in w around 0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{\left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot \sqrt{\frac{1}{\mathsf{max}\left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - -1 \cdot \left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right), {dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} - -1 \cdot \left({dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\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} \]

9. Applied rewrites 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\color{blue}{{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \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} \]

10. Taylor expanded in dY.u around inf

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{\frac{-1}{2}} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), {dY.u}^{2} \cdot \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
11. Step-by-step derivation

    1. *-commutative N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{\frac{-1}{2}} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot {dY.u}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

    2. lower-*.f32 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{\frac{-1}{2}} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\frac{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}{{dY.u}^{2}} + {\left(\left\lfloor w\right\rfloor \right)}^{2}\right) \cdot {dY.u}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

12. Applied rewrites 70.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(\left(dX.v \cdot 1\right) \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left({\left(\left\lfloor w\right\rfloor \right)}^{1}, {\left(\left\lfloor w\right\rfloor \right)}^{1}, \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

13. Final simplification 70.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) \cdot \left(\left(-1 \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;{\left(\mathsf{max}\left(\mathsf{fma}\left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dX.u\right) \cdot dX.u, 1, \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dX.v\right) \cdot dX.v\right), \left({\left(\left\lfloor h\right\rfloor \right)}^{2} \cdot dY.v\right) \cdot dY.v - \left(\left({\left(\left\lfloor w\right\rfloor \right)}^{2} \cdot dY.u\right) \cdot dY.u\right) \cdot -1\right)\right)}^{-0.5} \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) \cdot \left(-1 \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \mathsf{fma}\left({\left(\left\lfloor w\right\rfloor \right)}^{1}, {\left(\left\lfloor w\right\rfloor \right)}^{1}, \frac{{\left(dY.v \cdot \left\lfloor h\right\rfloor \right)}^{2}}{dY.u \cdot dY.u}\right) \cdot \left(dY.u \cdot dY.u\right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
14. Add Preprocessing

Reproduce

herbie shell --seed 2025066 
(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :name "Anisotropic x16 LOD (line direction, v)"
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0)) (and (<= 1.0 h) (<= h 16384.0))) (and (<= 1e-20 (fabs dX.u)) (<= (fabs dX.u) 1e+20))) (and (<= 1e-20 (fabs dX.v)) (<= (fabs dX.v) 1e+20))) (and (<= 1e-20 (fabs dY.u)) (<= (fabs dY.u) 1e+20))) (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20))) (== maxAniso 16.0))
  (if (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (* (/ 1.0 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor h) dX.v)) (* (/ 1.0 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor h) dY.v))))