Diagrams.TwoD.Apollonian:initialConfig from diagrams-contrib-1.3.0.5, A

Percentage Accurate: 68.3% → 99.9%
Time: 3.2s
Alternatives: 7
Speedup: 1.2×

Specification

?
\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
(FPCore (x y z)
  :precision binary64
  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))
double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = (((x * x) + (y * y)) - (z * z)) / (y * 2.0d0)
end function
public static double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}
def code(x, y, z):
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0)
function code(x, y, z)
	return Float64(Float64(Float64(Float64(x * x) + Float64(y * y)) - Float64(z * z)) / Float64(y * 2.0))
end
function tmp = code(x, y, z)
	tmp = (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
end
code[x_, y_, z_] := N[(N[(N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision] - N[(z * z), $MachinePrecision]), $MachinePrecision] / N[(y * 2.0), $MachinePrecision]), $MachinePrecision]
\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 7 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 68.3% accurate, 1.0× speedup?

\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
(FPCore (x y z)
  :precision binary64
  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))
double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = (((x * x) + (y * y)) - (z * z)) / (y * 2.0d0)
end function
public static double code(double x, double y, double z) {
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
}
def code(x, y, z):
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0)
function code(x, y, z)
	return Float64(Float64(Float64(Float64(x * x) + Float64(y * y)) - Float64(z * z)) / Float64(y * 2.0))
end
function tmp = code(x, y, z)
	tmp = (((x * x) + (y * y)) - (z * z)) / (y * 2.0);
end
code[x_, y_, z_] := N[(N[(N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision] - N[(z * z), $MachinePrecision]), $MachinePrecision] / N[(y * 2.0), $MachinePrecision]), $MachinePrecision]
\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}

Alternative 1: 99.9% accurate, 1.2× speedup?

\[\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5 \]
(FPCore (x y z)
  :precision binary64
  (* (fma (/ (- x z) y) (+ z x) y) 0.5))
double code(double x, double y, double z) {
	return fma(((x - z) / y), (z + x), y) * 0.5;
}
function code(x, y, z)
	return Float64(fma(Float64(Float64(x - z) / y), Float64(z + x), y) * 0.5)
end
code[x_, y_, z_] := N[(N[(N[(N[(x - z), $MachinePrecision] / y), $MachinePrecision] * N[(z + x), $MachinePrecision] + y), $MachinePrecision] * 0.5), $MachinePrecision]
\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5
Derivation
  1. Initial program 68.3%

    \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
  2. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
    2. lift--.f64N/A

      \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
    3. lift-+.f64N/A

      \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
    4. associate--l+N/A

      \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
    5. div-addN/A

      \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
    6. lift-*.f64N/A

      \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
    7. associate-/l*N/A

      \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
    8. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
    9. lower-/.f64N/A

      \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
    10. lift-*.f64N/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
    11. *-commutativeN/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
    12. count-2-revN/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
    13. lower-+.f64N/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
    14. lift-*.f64N/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
    15. associate-/r*N/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
    16. lower-/.f64N/A

      \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
  3. Applied rewrites94.0%

    \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
  4. Step-by-step derivation
    1. lift-fma.f64N/A

      \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
    2. +-commutativeN/A

      \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
    3. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
    4. lift--.f64N/A

      \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
    5. div-subN/A

      \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
    6. associate-+l-N/A

      \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
    7. lift-/.f64N/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
    8. associate-*r/N/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
    9. lift-+.f64N/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
    10. count-2N/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
    11. *-commutativeN/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
    12. associate-/r*N/A

      \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
    13. sub-divN/A

      \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
  5. Applied rewrites99.9%

    \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
  6. Add Preprocessing

Alternative 2: 98.3% accurate, 0.2× speedup?

\[\begin{array}{l} t_0 := \left|x\right| - \left|z\right|\\ t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\ \;\;\;\;\mathsf{fma}\left(\left|z\right|, \frac{\left|z\right|}{-2 \cdot \left|y\right|}, \left|y\right| \cdot 0.5\right)\\ \mathbf{elif}\;t\_1 \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(t\_0, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{t\_0}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\ \end{array} \end{array} \]
(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (- (fabs x) (fabs z)))
       (t_1
        (/
         (-
          (+ (* (fabs x) (fabs x)) (* (fabs y) (fabs y)))
          (* (fabs z) (fabs z)))
         (* (fabs y) 2.0))))
  (*
   (copysign 1.0 y)
   (if (<= t_1 -5e-81)
     (fma (fabs z) (/ (fabs z) (* -2.0 (fabs y))) (* (fabs y) 0.5))
     (if (<= t_1 INFINITY)
       (* (fma t_0 (/ (fabs x) (fabs y)) (fabs y)) 0.5)
       (* (fma (/ t_0 (fabs y)) (fabs z) (fabs y)) 0.5))))))
double code(double x, double y, double z) {
	double t_0 = fabs(x) - fabs(z);
	double t_1 = (((fabs(x) * fabs(x)) + (fabs(y) * fabs(y))) - (fabs(z) * fabs(z))) / (fabs(y) * 2.0);
	double tmp;
	if (t_1 <= -5e-81) {
		tmp = fma(fabs(z), (fabs(z) / (-2.0 * fabs(y))), (fabs(y) * 0.5));
	} else if (t_1 <= ((double) INFINITY)) {
		tmp = fma(t_0, (fabs(x) / fabs(y)), fabs(y)) * 0.5;
	} else {
		tmp = fma((t_0 / fabs(y)), fabs(z), fabs(y)) * 0.5;
	}
	return copysign(1.0, y) * tmp;
}
function code(x, y, z)
	t_0 = Float64(abs(x) - abs(z))
	t_1 = Float64(Float64(Float64(Float64(abs(x) * abs(x)) + Float64(abs(y) * abs(y))) - Float64(abs(z) * abs(z))) / Float64(abs(y) * 2.0))
	tmp = 0.0
	if (t_1 <= -5e-81)
		tmp = fma(abs(z), Float64(abs(z) / Float64(-2.0 * abs(y))), Float64(abs(y) * 0.5));
	elseif (t_1 <= Inf)
		tmp = Float64(fma(t_0, Float64(abs(x) / abs(y)), abs(y)) * 0.5);
	else
		tmp = Float64(fma(Float64(t_0 / abs(y)), abs(z), abs(y)) * 0.5);
	end
	return Float64(copysign(1.0, y) * tmp)
end
code[x_, y_, z_] := Block[{t$95$0 = N[(N[Abs[x], $MachinePrecision] - N[Abs[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(N[(N[(N[Abs[x], $MachinePrecision] * N[Abs[x], $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[Abs[z], $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Abs[y], $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[t$95$1, -5e-81], N[(N[Abs[z], $MachinePrecision] * N[(N[Abs[z], $MachinePrecision] / N[(-2.0 * N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, Infinity], N[(N[(t$95$0 * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], N[(N[(N[(t$95$0 / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision]]]), $MachinePrecision]]]
\begin{array}{l}
t_0 := \left|x\right| - \left|z\right|\\
t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\
\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l}
\mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\
\;\;\;\;\mathsf{fma}\left(\left|z\right|, \frac{\left|z\right|}{-2 \cdot \left|y\right|}, \left|y\right| \cdot 0.5\right)\\

\mathbf{elif}\;t\_1 \leq \infty:\\
\;\;\;\;\mathsf{fma}\left(t\_0, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{t\_0}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < -4.9999999999999998e-81

    1. Initial program 68.3%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
    2. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
      2. frac-2negN/A

        \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(\left(x \cdot x + y \cdot y\right) - z \cdot z\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)}} \]
      3. lift--.f64N/A

        \[\leadsto \frac{\mathsf{neg}\left(\color{blue}{\left(\left(x \cdot x + y \cdot y\right) - z \cdot z\right)}\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      4. sub-negate-revN/A

        \[\leadsto \frac{\color{blue}{z \cdot z - \left(x \cdot x + y \cdot y\right)}}{\mathsf{neg}\left(y \cdot 2\right)} \]
      5. sub-flipN/A

        \[\leadsto \frac{\color{blue}{z \cdot z + \left(\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)\right)}}{\mathsf{neg}\left(y \cdot 2\right)} \]
      6. div-addN/A

        \[\leadsto \color{blue}{\frac{z \cdot z}{\mathsf{neg}\left(y \cdot 2\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)}} \]
      7. distribute-neg-frac2N/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\frac{z \cdot z}{y \cdot 2}\right)\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{z \cdot z}}{y \cdot 2}\right)\right) + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      9. associate-/l*N/A

        \[\leadsto \left(\mathsf{neg}\left(\color{blue}{z \cdot \frac{z}{y \cdot 2}}\right)\right) + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      10. distribute-rgt-neg-inN/A

        \[\leadsto \color{blue}{z \cdot \left(\mathsf{neg}\left(\frac{z}{y \cdot 2}\right)\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      11. distribute-frac-negN/A

        \[\leadsto z \cdot \color{blue}{\frac{\mathsf{neg}\left(z\right)}{y \cdot 2}} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
      12. frac-2negN/A

        \[\leadsto z \cdot \frac{\mathsf{neg}\left(z\right)}{y \cdot 2} + \color{blue}{\frac{x \cdot x + y \cdot y}{y \cdot 2}} \]
      13. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(z, \frac{\mathsf{neg}\left(z\right)}{y \cdot 2}, \frac{x \cdot x + y \cdot y}{y \cdot 2}\right)} \]
    3. Applied rewrites87.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \left(y + \frac{x \cdot x}{y}\right) \cdot 0.5\right)} \]
    4. Taylor expanded in x around 0

      \[\leadsto \mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \color{blue}{y} \cdot 0.5\right) \]
    5. Step-by-step derivation
      1. Applied rewrites66.8%

        \[\leadsto \mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \color{blue}{y} \cdot 0.5\right) \]

      if -4.9999999999999998e-81 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < +inf.0

      1. Initial program 68.3%

        \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
      2. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
        2. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
        3. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
        4. associate--l+N/A

          \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
        5. div-addN/A

          \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
        6. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
        7. associate-/l*N/A

          \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
        8. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
        9. lower-/.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        10. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        11. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        12. count-2-revN/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        13. lower-+.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        14. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
        15. associate-/r*N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
        16. lower-/.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
      3. Applied rewrites94.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
      4. Step-by-step derivation
        1. lift-fma.f64N/A

          \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
        2. +-commutativeN/A

          \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
        4. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
        5. div-subN/A

          \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
        6. associate-+l-N/A

          \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
        7. lift-/.f64N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
        8. associate-*r/N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
        9. lift-+.f64N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
        10. count-2N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
        11. *-commutativeN/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
        12. associate-/r*N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
        13. sub-divN/A

          \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
      5. Applied rewrites99.9%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
      6. Step-by-step derivation
        1. lift-fma.f64N/A

          \[\leadsto \color{blue}{\left(\frac{x - z}{y} \cdot \left(z + x\right) + y\right)} \cdot \frac{1}{2} \]
        2. lift-/.f64N/A

          \[\leadsto \left(\color{blue}{\frac{x - z}{y}} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
        3. mult-flipN/A

          \[\leadsto \left(\color{blue}{\left(\left(x - z\right) \cdot \frac{1}{y}\right)} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
        4. lift-+.f64N/A

          \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(z + x\right)} + y\right) \cdot \frac{1}{2} \]
        5. +-commutativeN/A

          \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
        6. lift-+.f64N/A

          \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
        7. associate-*l*N/A

          \[\leadsto \left(\color{blue}{\left(x - z\right) \cdot \left(\frac{1}{y} \cdot \left(x + z\right)\right)} + y\right) \cdot \frac{1}{2} \]
        8. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(x + z\right), y\right)} \cdot \frac{1}{2} \]
        9. lower-*.f64N/A

          \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y} \cdot \left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
        10. lower-/.f6499.8%

          \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y}} \cdot \left(x + z\right), y\right) \cdot 0.5 \]
        11. lift-+.f64N/A

          \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
        12. +-commutativeN/A

          \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot \frac{1}{2} \]
        13. lift-+.f6499.8%

          \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot 0.5 \]
      7. Applied rewrites99.8%

        \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(z + x\right), y\right)} \cdot 0.5 \]
      8. Taylor expanded in x around inf

        \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]
      9. Step-by-step derivation
        1. lower-/.f6472.1%

          \[\leadsto \mathsf{fma}\left(x - z, \frac{x}{\color{blue}{y}}, y\right) \cdot 0.5 \]
      10. Applied rewrites72.1%

        \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]

      if +inf.0 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64)))

      1. Initial program 68.3%

        \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
      2. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
        2. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
        3. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
        4. associate--l+N/A

          \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
        5. div-addN/A

          \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
        6. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
        7. associate-/l*N/A

          \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
        8. lower-fma.f64N/A

          \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
        9. lower-/.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        10. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        11. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        12. count-2-revN/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        13. lower-+.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
        14. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
        15. associate-/r*N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
        16. lower-/.f64N/A

          \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
      3. Applied rewrites94.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
      4. Step-by-step derivation
        1. lift-fma.f64N/A

          \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
        2. +-commutativeN/A

          \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
        4. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
        5. div-subN/A

          \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
        6. associate-+l-N/A

          \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
        7. lift-/.f64N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
        8. associate-*r/N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
        9. lift-+.f64N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
        10. count-2N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
        11. *-commutativeN/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
        12. associate-/r*N/A

          \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
        13. sub-divN/A

          \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
      5. Applied rewrites99.9%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
      6. Taylor expanded in x around 0

        \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
      7. Step-by-step derivation
        1. Applied rewrites73.1%

          \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
      8. Recombined 3 regimes into one program.
      9. Add Preprocessing

      Alternative 3: 98.3% accurate, 0.2× speedup?

      \[\begin{array}{l} t_0 := \left|x\right| - \left|z\right|\\ t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\ \;\;\;\;\mathsf{fma}\left(\left|z\right|, \frac{-0.5}{\left|y\right|} \cdot \left|z\right|, \left|y\right| \cdot 0.5\right)\\ \mathbf{elif}\;t\_1 \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(t\_0, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{t\_0}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\ \end{array} \end{array} \]
      (FPCore (x y z)
        :precision binary64
        (let* ((t_0 (- (fabs x) (fabs z)))
             (t_1
              (/
               (-
                (+ (* (fabs x) (fabs x)) (* (fabs y) (fabs y)))
                (* (fabs z) (fabs z)))
               (* (fabs y) 2.0))))
        (*
         (copysign 1.0 y)
         (if (<= t_1 -5e-81)
           (fma (fabs z) (* (/ -0.5 (fabs y)) (fabs z)) (* (fabs y) 0.5))
           (if (<= t_1 INFINITY)
             (* (fma t_0 (/ (fabs x) (fabs y)) (fabs y)) 0.5)
             (* (fma (/ t_0 (fabs y)) (fabs z) (fabs y)) 0.5))))))
      double code(double x, double y, double z) {
      	double t_0 = fabs(x) - fabs(z);
      	double t_1 = (((fabs(x) * fabs(x)) + (fabs(y) * fabs(y))) - (fabs(z) * fabs(z))) / (fabs(y) * 2.0);
      	double tmp;
      	if (t_1 <= -5e-81) {
      		tmp = fma(fabs(z), ((-0.5 / fabs(y)) * fabs(z)), (fabs(y) * 0.5));
      	} else if (t_1 <= ((double) INFINITY)) {
      		tmp = fma(t_0, (fabs(x) / fabs(y)), fabs(y)) * 0.5;
      	} else {
      		tmp = fma((t_0 / fabs(y)), fabs(z), fabs(y)) * 0.5;
      	}
      	return copysign(1.0, y) * tmp;
      }
      
      function code(x, y, z)
      	t_0 = Float64(abs(x) - abs(z))
      	t_1 = Float64(Float64(Float64(Float64(abs(x) * abs(x)) + Float64(abs(y) * abs(y))) - Float64(abs(z) * abs(z))) / Float64(abs(y) * 2.0))
      	tmp = 0.0
      	if (t_1 <= -5e-81)
      		tmp = fma(abs(z), Float64(Float64(-0.5 / abs(y)) * abs(z)), Float64(abs(y) * 0.5));
      	elseif (t_1 <= Inf)
      		tmp = Float64(fma(t_0, Float64(abs(x) / abs(y)), abs(y)) * 0.5);
      	else
      		tmp = Float64(fma(Float64(t_0 / abs(y)), abs(z), abs(y)) * 0.5);
      	end
      	return Float64(copysign(1.0, y) * tmp)
      end
      
      code[x_, y_, z_] := Block[{t$95$0 = N[(N[Abs[x], $MachinePrecision] - N[Abs[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(N[(N[(N[Abs[x], $MachinePrecision] * N[Abs[x], $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[Abs[z], $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Abs[y], $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[t$95$1, -5e-81], N[(N[Abs[z], $MachinePrecision] * N[(N[(-0.5 / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, Infinity], N[(N[(t$95$0 * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], N[(N[(N[(t$95$0 / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision]]]), $MachinePrecision]]]
      
      \begin{array}{l}
      t_0 := \left|x\right| - \left|z\right|\\
      t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\
      \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l}
      \mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\
      \;\;\;\;\mathsf{fma}\left(\left|z\right|, \frac{-0.5}{\left|y\right|} \cdot \left|z\right|, \left|y\right| \cdot 0.5\right)\\
      
      \mathbf{elif}\;t\_1 \leq \infty:\\
      \;\;\;\;\mathsf{fma}\left(t\_0, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{fma}\left(\frac{t\_0}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < -4.9999999999999998e-81

        1. Initial program 68.3%

          \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
        2. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
          2. frac-2negN/A

            \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(\left(x \cdot x + y \cdot y\right) - z \cdot z\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)}} \]
          3. lift--.f64N/A

            \[\leadsto \frac{\mathsf{neg}\left(\color{blue}{\left(\left(x \cdot x + y \cdot y\right) - z \cdot z\right)}\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          4. sub-negate-revN/A

            \[\leadsto \frac{\color{blue}{z \cdot z - \left(x \cdot x + y \cdot y\right)}}{\mathsf{neg}\left(y \cdot 2\right)} \]
          5. sub-flipN/A

            \[\leadsto \frac{\color{blue}{z \cdot z + \left(\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)\right)}}{\mathsf{neg}\left(y \cdot 2\right)} \]
          6. div-addN/A

            \[\leadsto \color{blue}{\frac{z \cdot z}{\mathsf{neg}\left(y \cdot 2\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)}} \]
          7. distribute-neg-frac2N/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(\frac{z \cdot z}{y \cdot 2}\right)\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          8. lift-*.f64N/A

            \[\leadsto \left(\mathsf{neg}\left(\frac{\color{blue}{z \cdot z}}{y \cdot 2}\right)\right) + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          9. associate-/l*N/A

            \[\leadsto \left(\mathsf{neg}\left(\color{blue}{z \cdot \frac{z}{y \cdot 2}}\right)\right) + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          10. distribute-rgt-neg-inN/A

            \[\leadsto \color{blue}{z \cdot \left(\mathsf{neg}\left(\frac{z}{y \cdot 2}\right)\right)} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          11. distribute-frac-negN/A

            \[\leadsto z \cdot \color{blue}{\frac{\mathsf{neg}\left(z\right)}{y \cdot 2}} + \frac{\mathsf{neg}\left(\left(x \cdot x + y \cdot y\right)\right)}{\mathsf{neg}\left(y \cdot 2\right)} \]
          12. frac-2negN/A

            \[\leadsto z \cdot \frac{\mathsf{neg}\left(z\right)}{y \cdot 2} + \color{blue}{\frac{x \cdot x + y \cdot y}{y \cdot 2}} \]
          13. lower-fma.f64N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(z, \frac{\mathsf{neg}\left(z\right)}{y \cdot 2}, \frac{x \cdot x + y \cdot y}{y \cdot 2}\right)} \]
        3. Applied rewrites87.5%

          \[\leadsto \color{blue}{\mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \left(y + \frac{x \cdot x}{y}\right) \cdot 0.5\right)} \]
        4. Taylor expanded in x around 0

          \[\leadsto \mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \color{blue}{y} \cdot 0.5\right) \]
        5. Step-by-step derivation
          1. Applied rewrites66.8%

            \[\leadsto \mathsf{fma}\left(z, \frac{z}{-2 \cdot y}, \color{blue}{y} \cdot 0.5\right) \]
          2. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{z}{-2 \cdot y}}, y \cdot \frac{1}{2}\right) \]
            2. mult-flipN/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{z \cdot \frac{1}{-2 \cdot y}}, y \cdot \frac{1}{2}\right) \]
            3. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{1}{-2 \cdot y} \cdot z}, y \cdot \frac{1}{2}\right) \]
            4. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{1}{-2 \cdot y} \cdot z}, y \cdot \frac{1}{2}\right) \]
            5. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(z, \frac{1}{\color{blue}{-2 \cdot y}} \cdot z, y \cdot \frac{1}{2}\right) \]
            6. associate-/r*N/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{\frac{1}{-2}}{y}} \cdot z, y \cdot \frac{1}{2}\right) \]
            7. lower-/.f64N/A

              \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{\frac{1}{-2}}{y}} \cdot z, y \cdot \frac{1}{2}\right) \]
            8. metadata-eval66.8%

              \[\leadsto \mathsf{fma}\left(z, \frac{\color{blue}{-0.5}}{y} \cdot z, y \cdot 0.5\right) \]
          3. Applied rewrites66.8%

            \[\leadsto \mathsf{fma}\left(z, \color{blue}{\frac{-0.5}{y} \cdot z}, y \cdot 0.5\right) \]

          if -4.9999999999999998e-81 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < +inf.0

          1. Initial program 68.3%

            \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
          2. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
            2. lift--.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
            3. lift-+.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
            4. associate--l+N/A

              \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
            5. div-addN/A

              \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
            6. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
            7. associate-/l*N/A

              \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
            8. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
            9. lower-/.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            11. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            12. count-2-revN/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            14. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
            15. associate-/r*N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
            16. lower-/.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
          3. Applied rewrites94.0%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
          4. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
            3. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
            4. lift--.f64N/A

              \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
            5. div-subN/A

              \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
            6. associate-+l-N/A

              \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
            7. lift-/.f64N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
            8. associate-*r/N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
            9. lift-+.f64N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
            10. count-2N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
            11. *-commutativeN/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
            12. associate-/r*N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
            13. sub-divN/A

              \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
          5. Applied rewrites99.9%

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
          6. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{\left(\frac{x - z}{y} \cdot \left(z + x\right) + y\right)} \cdot \frac{1}{2} \]
            2. lift-/.f64N/A

              \[\leadsto \left(\color{blue}{\frac{x - z}{y}} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
            3. mult-flipN/A

              \[\leadsto \left(\color{blue}{\left(\left(x - z\right) \cdot \frac{1}{y}\right)} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
            4. lift-+.f64N/A

              \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(z + x\right)} + y\right) \cdot \frac{1}{2} \]
            5. +-commutativeN/A

              \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
            6. lift-+.f64N/A

              \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
            7. associate-*l*N/A

              \[\leadsto \left(\color{blue}{\left(x - z\right) \cdot \left(\frac{1}{y} \cdot \left(x + z\right)\right)} + y\right) \cdot \frac{1}{2} \]
            8. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(x + z\right), y\right)} \cdot \frac{1}{2} \]
            9. lower-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y} \cdot \left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
            10. lower-/.f6499.8%

              \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y}} \cdot \left(x + z\right), y\right) \cdot 0.5 \]
            11. lift-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
            12. +-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot \frac{1}{2} \]
            13. lift-+.f6499.8%

              \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot 0.5 \]
          7. Applied rewrites99.8%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(z + x\right), y\right)} \cdot 0.5 \]
          8. Taylor expanded in x around inf

            \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]
          9. Step-by-step derivation
            1. lower-/.f6472.1%

              \[\leadsto \mathsf{fma}\left(x - z, \frac{x}{\color{blue}{y}}, y\right) \cdot 0.5 \]
          10. Applied rewrites72.1%

            \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]

          if +inf.0 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64)))

          1. Initial program 68.3%

            \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
          2. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
            2. lift--.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
            3. lift-+.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
            4. associate--l+N/A

              \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
            5. div-addN/A

              \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
            6. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
            7. associate-/l*N/A

              \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
            8. lower-fma.f64N/A

              \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
            9. lower-/.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            10. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            11. *-commutativeN/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            12. count-2-revN/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            13. lower-+.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
            14. lift-*.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
            15. associate-/r*N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
            16. lower-/.f64N/A

              \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
          3. Applied rewrites94.0%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
          4. Step-by-step derivation
            1. lift-fma.f64N/A

              \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
            2. +-commutativeN/A

              \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
            3. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
            4. lift--.f64N/A

              \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
            5. div-subN/A

              \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
            6. associate-+l-N/A

              \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
            7. lift-/.f64N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
            8. associate-*r/N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
            9. lift-+.f64N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
            10. count-2N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
            11. *-commutativeN/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
            12. associate-/r*N/A

              \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
            13. sub-divN/A

              \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
          5. Applied rewrites99.9%

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
          6. Taylor expanded in x around 0

            \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
          7. Step-by-step derivation
            1. Applied rewrites73.1%

              \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
          8. Recombined 3 regimes into one program.
          9. Add Preprocessing

          Alternative 4: 98.2% accurate, 0.2× speedup?

          \[\begin{array}{l} t_0 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\ t_1 := \left|x\right| - \left|z\right|\\ t_2 := \mathsf{fma}\left(\frac{t\_1}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;t\_0 \leq -5 \cdot 10^{-81}:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_0 \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(t\_1, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \end{array} \]
          (FPCore (x y z)
            :precision binary64
            (let* ((t_0
                  (/
                   (-
                    (+ (* (fabs x) (fabs x)) (* (fabs y) (fabs y)))
                    (* (fabs z) (fabs z)))
                   (* (fabs y) 2.0)))
                 (t_1 (- (fabs x) (fabs z)))
                 (t_2 (* (fma (/ t_1 (fabs y)) (fabs z) (fabs y)) 0.5)))
            (*
             (copysign 1.0 y)
             (if (<= t_0 -5e-81)
               t_2
               (if (<= t_0 INFINITY)
                 (* (fma t_1 (/ (fabs x) (fabs y)) (fabs y)) 0.5)
                 t_2)))))
          double code(double x, double y, double z) {
          	double t_0 = (((fabs(x) * fabs(x)) + (fabs(y) * fabs(y))) - (fabs(z) * fabs(z))) / (fabs(y) * 2.0);
          	double t_1 = fabs(x) - fabs(z);
          	double t_2 = fma((t_1 / fabs(y)), fabs(z), fabs(y)) * 0.5;
          	double tmp;
          	if (t_0 <= -5e-81) {
          		tmp = t_2;
          	} else if (t_0 <= ((double) INFINITY)) {
          		tmp = fma(t_1, (fabs(x) / fabs(y)), fabs(y)) * 0.5;
          	} else {
          		tmp = t_2;
          	}
          	return copysign(1.0, y) * tmp;
          }
          
          function code(x, y, z)
          	t_0 = Float64(Float64(Float64(Float64(abs(x) * abs(x)) + Float64(abs(y) * abs(y))) - Float64(abs(z) * abs(z))) / Float64(abs(y) * 2.0))
          	t_1 = Float64(abs(x) - abs(z))
          	t_2 = Float64(fma(Float64(t_1 / abs(y)), abs(z), abs(y)) * 0.5)
          	tmp = 0.0
          	if (t_0 <= -5e-81)
          		tmp = t_2;
          	elseif (t_0 <= Inf)
          		tmp = Float64(fma(t_1, Float64(abs(x) / abs(y)), abs(y)) * 0.5);
          	else
          		tmp = t_2;
          	end
          	return Float64(copysign(1.0, y) * tmp)
          end
          
          code[x_, y_, z_] := Block[{t$95$0 = N[(N[(N[(N[(N[Abs[x], $MachinePrecision] * N[Abs[x], $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[Abs[z], $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Abs[y], $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[Abs[x], $MachinePrecision] - N[Abs[z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(N[(t$95$1 / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[t$95$0, -5e-81], t$95$2, If[LessEqual[t$95$0, Infinity], N[(N[(t$95$1 * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], t$95$2]]), $MachinePrecision]]]]
          
          \begin{array}{l}
          t_0 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\
          t_1 := \left|x\right| - \left|z\right|\\
          t_2 := \mathsf{fma}\left(\frac{t\_1}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\
          \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l}
          \mathbf{if}\;t\_0 \leq -5 \cdot 10^{-81}:\\
          \;\;\;\;t\_2\\
          
          \mathbf{elif}\;t\_0 \leq \infty:\\
          \;\;\;\;\mathsf{fma}\left(t\_1, \frac{\left|x\right|}{\left|y\right|}, \left|y\right|\right) \cdot 0.5\\
          
          \mathbf{else}:\\
          \;\;\;\;t\_2\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < -4.9999999999999998e-81 or +inf.0 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64)))

            1. Initial program 68.3%

              \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
            2. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
              2. lift--.f64N/A

                \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
              3. lift-+.f64N/A

                \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
              4. associate--l+N/A

                \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
              5. div-addN/A

                \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
              6. lift-*.f64N/A

                \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
              7. associate-/l*N/A

                \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
              8. lower-fma.f64N/A

                \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
              9. lower-/.f64N/A

                \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
              10. lift-*.f64N/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
              11. *-commutativeN/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
              12. count-2-revN/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
              13. lower-+.f64N/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
              14. lift-*.f64N/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
              15. associate-/r*N/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
              16. lower-/.f64N/A

                \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
            3. Applied rewrites94.0%

              \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
            4. Step-by-step derivation
              1. lift-fma.f64N/A

                \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
              2. +-commutativeN/A

                \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
              3. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
              4. lift--.f64N/A

                \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
              5. div-subN/A

                \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
              6. associate-+l-N/A

                \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
              7. lift-/.f64N/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
              8. associate-*r/N/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
              9. lift-+.f64N/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
              10. count-2N/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
              11. *-commutativeN/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
              12. associate-/r*N/A

                \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
              13. sub-divN/A

                \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
            5. Applied rewrites99.9%

              \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
            6. Taylor expanded in x around 0

              \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
            7. Step-by-step derivation
              1. Applied rewrites73.1%

                \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]

              if -4.9999999999999998e-81 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < +inf.0

              1. Initial program 68.3%

                \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
              2. Step-by-step derivation
                1. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
                2. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
                3. lift-+.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
                4. associate--l+N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
                5. div-addN/A

                  \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
                6. lift-*.f64N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                7. associate-/l*N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                8. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
                9. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                10. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                12. count-2-revN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                13. lower-+.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                14. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
                15. associate-/r*N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
                16. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
              3. Applied rewrites94.0%

                \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
              4. Step-by-step derivation
                1. lift-fma.f64N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
                2. +-commutativeN/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
                3. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
                4. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
                5. div-subN/A

                  \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
                6. associate-+l-N/A

                  \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
                7. lift-/.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
                8. associate-*r/N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
                9. lift-+.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
                10. count-2N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
                12. associate-/r*N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
                13. sub-divN/A

                  \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
              5. Applied rewrites99.9%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
              6. Step-by-step derivation
                1. lift-fma.f64N/A

                  \[\leadsto \color{blue}{\left(\frac{x - z}{y} \cdot \left(z + x\right) + y\right)} \cdot \frac{1}{2} \]
                2. lift-/.f64N/A

                  \[\leadsto \left(\color{blue}{\frac{x - z}{y}} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
                3. mult-flipN/A

                  \[\leadsto \left(\color{blue}{\left(\left(x - z\right) \cdot \frac{1}{y}\right)} \cdot \left(z + x\right) + y\right) \cdot \frac{1}{2} \]
                4. lift-+.f64N/A

                  \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(z + x\right)} + y\right) \cdot \frac{1}{2} \]
                5. +-commutativeN/A

                  \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
                6. lift-+.f64N/A

                  \[\leadsto \left(\left(\left(x - z\right) \cdot \frac{1}{y}\right) \cdot \color{blue}{\left(x + z\right)} + y\right) \cdot \frac{1}{2} \]
                7. associate-*l*N/A

                  \[\leadsto \left(\color{blue}{\left(x - z\right) \cdot \left(\frac{1}{y} \cdot \left(x + z\right)\right)} + y\right) \cdot \frac{1}{2} \]
                8. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(x + z\right), y\right)} \cdot \frac{1}{2} \]
                9. lower-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y} \cdot \left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
                10. lower-/.f6499.8%

                  \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{1}{y}} \cdot \left(x + z\right), y\right) \cdot 0.5 \]
                11. lift-+.f64N/A

                  \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(x + z\right)}, y\right) \cdot \frac{1}{2} \]
                12. +-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot \frac{1}{2} \]
                13. lift-+.f6499.8%

                  \[\leadsto \mathsf{fma}\left(x - z, \frac{1}{y} \cdot \color{blue}{\left(z + x\right)}, y\right) \cdot 0.5 \]
              7. Applied rewrites99.8%

                \[\leadsto \color{blue}{\mathsf{fma}\left(x - z, \frac{1}{y} \cdot \left(z + x\right), y\right)} \cdot 0.5 \]
              8. Taylor expanded in x around inf

                \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]
              9. Step-by-step derivation
                1. lower-/.f6472.1%

                  \[\leadsto \mathsf{fma}\left(x - z, \frac{x}{\color{blue}{y}}, y\right) \cdot 0.5 \]
              10. Applied rewrites72.1%

                \[\leadsto \mathsf{fma}\left(x - z, \color{blue}{\frac{x}{y}}, y\right) \cdot 0.5 \]
            8. Recombined 2 regimes into one program.
            9. Add Preprocessing

            Alternative 5: 98.2% accurate, 0.2× speedup?

            \[\begin{array}{l} t_0 := \mathsf{fma}\left(\frac{\left|x\right| - \left|z\right|}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\ t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq \infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{\left|x\right|}{\left|y\right|}, \left|z\right| + \left|x\right|, \left|y\right|\right) \cdot 0.5\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
            (FPCore (x y z)
              :precision binary64
              (let* ((t_0
                    (*
                     (fma (/ (- (fabs x) (fabs z)) (fabs y)) (fabs z) (fabs y))
                     0.5))
                   (t_1
                    (/
                     (-
                      (+ (* (fabs x) (fabs x)) (* (fabs y) (fabs y)))
                      (* (fabs z) (fabs z)))
                     (* (fabs y) 2.0))))
              (*
               (copysign 1.0 y)
               (if (<= t_1 -5e-81)
                 t_0
                 (if (<= t_1 INFINITY)
                   (*
                    (fma (/ (fabs x) (fabs y)) (+ (fabs z) (fabs x)) (fabs y))
                    0.5)
                   t_0)))))
            double code(double x, double y, double z) {
            	double t_0 = fma(((fabs(x) - fabs(z)) / fabs(y)), fabs(z), fabs(y)) * 0.5;
            	double t_1 = (((fabs(x) * fabs(x)) + (fabs(y) * fabs(y))) - (fabs(z) * fabs(z))) / (fabs(y) * 2.0);
            	double tmp;
            	if (t_1 <= -5e-81) {
            		tmp = t_0;
            	} else if (t_1 <= ((double) INFINITY)) {
            		tmp = fma((fabs(x) / fabs(y)), (fabs(z) + fabs(x)), fabs(y)) * 0.5;
            	} else {
            		tmp = t_0;
            	}
            	return copysign(1.0, y) * tmp;
            }
            
            function code(x, y, z)
            	t_0 = Float64(fma(Float64(Float64(abs(x) - abs(z)) / abs(y)), abs(z), abs(y)) * 0.5)
            	t_1 = Float64(Float64(Float64(Float64(abs(x) * abs(x)) + Float64(abs(y) * abs(y))) - Float64(abs(z) * abs(z))) / Float64(abs(y) * 2.0))
            	tmp = 0.0
            	if (t_1 <= -5e-81)
            		tmp = t_0;
            	elseif (t_1 <= Inf)
            		tmp = Float64(fma(Float64(abs(x) / abs(y)), Float64(abs(z) + abs(x)), abs(y)) * 0.5);
            	else
            		tmp = t_0;
            	end
            	return Float64(copysign(1.0, y) * tmp)
            end
            
            code[x_, y_, z_] := Block[{t$95$0 = N[(N[(N[(N[(N[Abs[x], $MachinePrecision] - N[Abs[z], $MachinePrecision]), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision]}, Block[{t$95$1 = N[(N[(N[(N[(N[Abs[x], $MachinePrecision] * N[Abs[x], $MachinePrecision]), $MachinePrecision] + N[(N[Abs[y], $MachinePrecision] * N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[Abs[z], $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[Abs[y], $MachinePrecision] * 2.0), $MachinePrecision]), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[t$95$1, -5e-81], t$95$0, If[LessEqual[t$95$1, Infinity], N[(N[(N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[(N[Abs[z], $MachinePrecision] + N[Abs[x], $MachinePrecision]), $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision], t$95$0]]), $MachinePrecision]]]
            
            \begin{array}{l}
            t_0 := \mathsf{fma}\left(\frac{\left|x\right| - \left|z\right|}{\left|y\right|}, \left|z\right|, \left|y\right|\right) \cdot 0.5\\
            t_1 := \frac{\left(\left|x\right| \cdot \left|x\right| + \left|y\right| \cdot \left|y\right|\right) - \left|z\right| \cdot \left|z\right|}{\left|y\right| \cdot 2}\\
            \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l}
            \mathbf{if}\;t\_1 \leq -5 \cdot 10^{-81}:\\
            \;\;\;\;t\_0\\
            
            \mathbf{elif}\;t\_1 \leq \infty:\\
            \;\;\;\;\mathsf{fma}\left(\frac{\left|x\right|}{\left|y\right|}, \left|z\right| + \left|x\right|, \left|y\right|\right) \cdot 0.5\\
            
            \mathbf{else}:\\
            \;\;\;\;t\_0\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < -4.9999999999999998e-81 or +inf.0 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64)))

              1. Initial program 68.3%

                \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
              2. Step-by-step derivation
                1. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
                2. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
                3. lift-+.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
                4. associate--l+N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
                5. div-addN/A

                  \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
                6. lift-*.f64N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                7. associate-/l*N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                8. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
                9. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                10. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                12. count-2-revN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                13. lower-+.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                14. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
                15. associate-/r*N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
                16. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
              3. Applied rewrites94.0%

                \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
              4. Step-by-step derivation
                1. lift-fma.f64N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
                2. +-commutativeN/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
                3. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
                4. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
                5. div-subN/A

                  \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
                6. associate-+l-N/A

                  \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
                7. lift-/.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
                8. associate-*r/N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
                9. lift-+.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
                10. count-2N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
                12. associate-/r*N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
                13. sub-divN/A

                  \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
              5. Applied rewrites99.9%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
              6. Taylor expanded in x around 0

                \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
              7. Step-by-step derivation
                1. Applied rewrites73.1%

                  \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]

                if -4.9999999999999998e-81 < (/.f64 (-.f64 (+.f64 (*.f64 x x) (*.f64 y y)) (*.f64 z z)) (*.f64 y #s(literal 2 binary64))) < +inf.0

                1. Initial program 68.3%

                  \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
                2. Step-by-step derivation
                  1. lift-/.f64N/A

                    \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
                  2. lift--.f64N/A

                    \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
                  3. lift-+.f64N/A

                    \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
                  4. associate--l+N/A

                    \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
                  5. div-addN/A

                    \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
                  6. lift-*.f64N/A

                    \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                  7. associate-/l*N/A

                    \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                  8. lower-fma.f64N/A

                    \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
                  9. lower-/.f64N/A

                    \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                  10. lift-*.f64N/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                  11. *-commutativeN/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                  12. count-2-revN/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                  13. lower-+.f64N/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                  14. lift-*.f64N/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
                  15. associate-/r*N/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
                  16. lower-/.f64N/A

                    \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
                3. Applied rewrites94.0%

                  \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
                4. Step-by-step derivation
                  1. lift-fma.f64N/A

                    \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
                  2. +-commutativeN/A

                    \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
                  3. lift-/.f64N/A

                    \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
                  4. lift--.f64N/A

                    \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
                  5. div-subN/A

                    \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
                  6. associate-+l-N/A

                    \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
                  7. lift-/.f64N/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
                  8. associate-*r/N/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
                  9. lift-+.f64N/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
                  10. count-2N/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
                  11. *-commutativeN/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
                  12. associate-/r*N/A

                    \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
                  13. sub-divN/A

                    \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
                5. Applied rewrites99.9%

                  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
                6. Taylor expanded in x around inf

                  \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{x}{y}}, z + x, y\right) \cdot 0.5 \]
                7. Step-by-step derivation
                  1. lower-/.f6471.9%

                    \[\leadsto \mathsf{fma}\left(\frac{x}{\color{blue}{y}}, z + x, y\right) \cdot 0.5 \]
                8. Applied rewrites71.9%

                  \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{x}{y}}, z + x, y\right) \cdot 0.5 \]
              8. Recombined 2 regimes into one program.
              9. Add Preprocessing

              Alternative 6: 79.5% accurate, 1.2× speedup?

              \[\mathsf{fma}\left(\frac{\left|x\right| - \left|z\right|}{y}, \left|z\right|, y\right) \cdot 0.5 \]
              (FPCore (x y z)
                :precision binary64
                (* (fma (/ (- (fabs x) (fabs z)) y) (fabs z) y) 0.5))
              double code(double x, double y, double z) {
              	return fma(((fabs(x) - fabs(z)) / y), fabs(z), y) * 0.5;
              }
              
              function code(x, y, z)
              	return Float64(fma(Float64(Float64(abs(x) - abs(z)) / y), abs(z), y) * 0.5)
              end
              
              code[x_, y_, z_] := N[(N[(N[(N[(N[Abs[x], $MachinePrecision] - N[Abs[z], $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision] * N[Abs[z], $MachinePrecision] + y), $MachinePrecision] * 0.5), $MachinePrecision]
              
              \mathsf{fma}\left(\frac{\left|x\right| - \left|z\right|}{y}, \left|z\right|, y\right) \cdot 0.5
              
              Derivation
              1. Initial program 68.3%

                \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
              2. Step-by-step derivation
                1. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}} \]
                2. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right) - z \cdot z}}{y \cdot 2} \]
                3. lift-+.f64N/A

                  \[\leadsto \frac{\color{blue}{\left(x \cdot x + y \cdot y\right)} - z \cdot z}{y \cdot 2} \]
                4. associate--l+N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x + \left(y \cdot y - z \cdot z\right)}}{y \cdot 2} \]
                5. div-addN/A

                  \[\leadsto \color{blue}{\frac{x \cdot x}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2}} \]
                6. lift-*.f64N/A

                  \[\leadsto \frac{\color{blue}{x \cdot x}}{y \cdot 2} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                7. associate-/l*N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y \cdot 2}} + \frac{y \cdot y - z \cdot z}{y \cdot 2} \]
                8. lower-fma.f64N/A

                  \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y \cdot 2}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right)} \]
                9. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \color{blue}{\frac{x}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                10. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y \cdot 2}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{2 \cdot y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                12. count-2-revN/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                13. lower-+.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{\color{blue}{y + y}}, \frac{y \cdot y - z \cdot z}{y \cdot 2}\right) \]
                14. lift-*.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y \cdot y - z \cdot z}{\color{blue}{y \cdot 2}}\right) \]
                15. associate-/r*N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
                16. lower-/.f64N/A

                  \[\leadsto \mathsf{fma}\left(x, \frac{x}{y + y}, \color{blue}{\frac{\frac{y \cdot y - z \cdot z}{y}}{2}}\right) \]
              3. Applied rewrites94.0%

                \[\leadsto \color{blue}{\mathsf{fma}\left(x, \frac{x}{y + y}, \frac{y - z \cdot \frac{z}{y}}{2}\right)} \]
              4. Step-by-step derivation
                1. lift-fma.f64N/A

                  \[\leadsto \color{blue}{x \cdot \frac{x}{y + y} + \frac{y - z \cdot \frac{z}{y}}{2}} \]
                2. +-commutativeN/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2} + x \cdot \frac{x}{y + y}} \]
                3. lift-/.f64N/A

                  \[\leadsto \color{blue}{\frac{y - z \cdot \frac{z}{y}}{2}} + x \cdot \frac{x}{y + y} \]
                4. lift--.f64N/A

                  \[\leadsto \frac{\color{blue}{y - z \cdot \frac{z}{y}}}{2} + x \cdot \frac{x}{y + y} \]
                5. div-subN/A

                  \[\leadsto \color{blue}{\left(\frac{y}{2} - \frac{z \cdot \frac{z}{y}}{2}\right)} + x \cdot \frac{x}{y + y} \]
                6. associate-+l-N/A

                  \[\leadsto \color{blue}{\frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \frac{x}{y + y}\right)} \]
                7. lift-/.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - x \cdot \color{blue}{\frac{x}{y + y}}\right) \]
                8. associate-*r/N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{x \cdot x}{y + y}}\right) \]
                9. lift-+.f64N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y + y}}\right) \]
                10. count-2N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{2 \cdot y}}\right) \]
                11. *-commutativeN/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \frac{x \cdot x}{\color{blue}{y \cdot 2}}\right) \]
                12. associate-/r*N/A

                  \[\leadsto \frac{y}{2} - \left(\frac{z \cdot \frac{z}{y}}{2} - \color{blue}{\frac{\frac{x \cdot x}{y}}{2}}\right) \]
                13. sub-divN/A

                  \[\leadsto \frac{y}{2} - \color{blue}{\frac{z \cdot \frac{z}{y} - \frac{x \cdot x}{y}}{2}} \]
              5. Applied rewrites99.9%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, z + x, y\right) \cdot 0.5} \]
              6. Taylor expanded in x around 0

                \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
              7. Step-by-step derivation
                1. Applied rewrites73.1%

                  \[\leadsto \mathsf{fma}\left(\frac{x - z}{y}, \color{blue}{z}, y\right) \cdot 0.5 \]
                2. Add Preprocessing

                Alternative 7: 35.5% accurate, 5.5× speedup?

                \[0.5 \cdot y \]
                (FPCore (x y z)
                  :precision binary64
                  (* 0.5 y))
                double code(double x, double y, double z) {
                	return 0.5 * y;
                }
                
                module fmin_fmax_functions
                    implicit none
                    private
                    public fmax
                    public fmin
                
                    interface fmax
                        module procedure fmax88
                        module procedure fmax44
                        module procedure fmax84
                        module procedure fmax48
                    end interface
                    interface fmin
                        module procedure fmin88
                        module procedure fmin44
                        module procedure fmin84
                        module procedure fmin48
                    end interface
                contains
                    real(8) function fmax88(x, y) result (res)
                        real(8), intent (in) :: x
                        real(8), intent (in) :: y
                        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                    end function
                    real(4) function fmax44(x, y) result (res)
                        real(4), intent (in) :: x
                        real(4), intent (in) :: y
                        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                    end function
                    real(8) function fmax84(x, y) result(res)
                        real(8), intent (in) :: x
                        real(4), intent (in) :: y
                        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                    end function
                    real(8) function fmax48(x, y) result(res)
                        real(4), intent (in) :: x
                        real(8), intent (in) :: y
                        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                    end function
                    real(8) function fmin88(x, y) result (res)
                        real(8), intent (in) :: x
                        real(8), intent (in) :: y
                        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                    end function
                    real(4) function fmin44(x, y) result (res)
                        real(4), intent (in) :: x
                        real(4), intent (in) :: y
                        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                    end function
                    real(8) function fmin84(x, y) result(res)
                        real(8), intent (in) :: x
                        real(4), intent (in) :: y
                        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                    end function
                    real(8) function fmin48(x, y) result(res)
                        real(4), intent (in) :: x
                        real(8), intent (in) :: y
                        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                    end function
                end module
                
                real(8) function code(x, y, z)
                use fmin_fmax_functions
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    real(8), intent (in) :: z
                    code = 0.5d0 * y
                end function
                
                public static double code(double x, double y, double z) {
                	return 0.5 * y;
                }
                
                def code(x, y, z):
                	return 0.5 * y
                
                function code(x, y, z)
                	return Float64(0.5 * y)
                end
                
                function tmp = code(x, y, z)
                	tmp = 0.5 * y;
                end
                
                code[x_, y_, z_] := N[(0.5 * y), $MachinePrecision]
                
                0.5 \cdot y
                
                Derivation
                1. Initial program 68.3%

                  \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
                2. Taylor expanded in y around inf

                  \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
                3. Step-by-step derivation
                  1. lower-*.f6435.5%

                    \[\leadsto 0.5 \cdot \color{blue}{y} \]
                4. Applied rewrites35.5%

                  \[\leadsto \color{blue}{0.5 \cdot y} \]
                5. Add Preprocessing

                Reproduce

                ?
                herbie shell --seed 2025212 
                (FPCore (x y z)
                  :name "Diagrams.TwoD.Apollonian:initialConfig from diagrams-contrib-1.3.0.5, A"
                  :precision binary64
                  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2.0)))