jeff quadratic root 1

Percentage Accurate: 72.1% → 99.8%

Time: 12.9s

Alternatives: 8

Speedup: 1.3×

Specification

Math

\[\begin{array}{l} t_0 := \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\\ \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t\_0}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + t\_0}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (sqrt (- (* b b) (* (* 4 a) c)))))
  (if (>= b 0) (/ (- (- b) t_0) (* 2 a)) (/ (* 2 c) (+ (- b) t_0)))))

C

double code(double a, double b, double c) {
	double t_0 = sqrt(((b * b) - ((4.0 * a) * c)));
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - t_0) / (2.0 * a);
	} else {
		tmp = (2.0 * c) / (-b + t_0);
	}
	return tmp;
}

Fortran

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(a, b, c)
use fmin_fmax_functions
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    real(8), intent (in) :: c
    real(8) :: t_0
    real(8) :: tmp
    t_0 = sqrt(((b * b) - ((4.0d0 * a) * c)))
    if (b >= 0.0d0) then
        tmp = (-b - t_0) / (2.0d0 * a)
    else
        tmp = (2.0d0 * c) / (-b + t_0)
    end if
    code = tmp
end function

Java

public static double code(double a, double b, double c) {
	double t_0 = Math.sqrt(((b * b) - ((4.0 * a) * c)));
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - t_0) / (2.0 * a);
	} else {
		tmp = (2.0 * c) / (-b + t_0);
	}
	return tmp;
}

Python

def code(a, b, c):
	t_0 = math.sqrt(((b * b) - ((4.0 * a) * c)))
	tmp = 0
	if b >= 0.0:
		tmp = (-b - t_0) / (2.0 * a)
	else:
		tmp = (2.0 * c) / (-b + t_0)
	return tmp

Julia

function code(a, b, c)
	t_0 = sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))
	tmp = 0.0
	if (b >= 0.0)
		tmp = Float64(Float64(Float64(-b) - t_0) / Float64(2.0 * a));
	else
		tmp = Float64(Float64(2.0 * c) / Float64(Float64(-b) + t_0));
	end
	return tmp
end

MATLAB

function tmp_2 = code(a, b, c)
	t_0 = sqrt(((b * b) - ((4.0 * a) * c)));
	tmp = 0.0;
	if (b >= 0.0)
		tmp = (-b - t_0) / (2.0 * a);
	else
		tmp = (2.0 * c) / (-b + t_0);
	end
	tmp_2 = tmp;
end

Wolfram

code[a_, b_, c_] := Block[{t$95$0 = N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(N[(4 * a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, If[GreaterEqual[b, 0], N[(N[((-b) - t$95$0), $MachinePrecision] / N[(2 * a), $MachinePrecision]), $MachinePrecision], N[(N[(2 * c), $MachinePrecision] / N[((-b) + t$95$0), $MachinePrecision]), $MachinePrecision]]]

Initial Program: 72.1% accurate, 1.0× speedup

Math

\[\begin{array}{l} t_0 := \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\\ \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t\_0}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + t\_0}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (sqrt (- (* b b) (* (* 4 a) c)))))
  (if (>= b 0) (/ (- (- b) t_0) (* 2 a)) (/ (* 2 c) (+ (- b) t_0)))))

C

double code(double a, double b, double c) {
	double t_0 = sqrt(((b * b) - ((4.0 * a) * c)));
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - t_0) / (2.0 * a);
	} else {
		tmp = (2.0 * c) / (-b + t_0);
	}
	return tmp;
}

Fortran

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(a, b, c)
use fmin_fmax_functions
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    real(8), intent (in) :: c
    real(8) :: t_0
    real(8) :: tmp
    t_0 = sqrt(((b * b) - ((4.0d0 * a) * c)))
    if (b >= 0.0d0) then
        tmp = (-b - t_0) / (2.0d0 * a)
    else
        tmp = (2.0d0 * c) / (-b + t_0)
    end if
    code = tmp
end function

Java

public static double code(double a, double b, double c) {
	double t_0 = Math.sqrt(((b * b) - ((4.0 * a) * c)));
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - t_0) / (2.0 * a);
	} else {
		tmp = (2.0 * c) / (-b + t_0);
	}
	return tmp;
}

Python

def code(a, b, c):
	t_0 = math.sqrt(((b * b) - ((4.0 * a) * c)))
	tmp = 0
	if b >= 0.0:
		tmp = (-b - t_0) / (2.0 * a)
	else:
		tmp = (2.0 * c) / (-b + t_0)
	return tmp

Julia

function code(a, b, c)
	t_0 = sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))
	tmp = 0.0
	if (b >= 0.0)
		tmp = Float64(Float64(Float64(-b) - t_0) / Float64(2.0 * a));
	else
		tmp = Float64(Float64(2.0 * c) / Float64(Float64(-b) + t_0));
	end
	return tmp
end

MATLAB

function tmp_2 = code(a, b, c)
	t_0 = sqrt(((b * b) - ((4.0 * a) * c)));
	tmp = 0.0;
	if (b >= 0.0)
		tmp = (-b - t_0) / (2.0 * a);
	else
		tmp = (2.0 * c) / (-b + t_0);
	end
	tmp_2 = tmp;
end

Wolfram

code[a_, b_, c_] := Block[{t$95$0 = N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(N[(4 * a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, If[GreaterEqual[b, 0], N[(N[((-b) - t$95$0), $MachinePrecision] / N[(2 * a), $MachinePrecision]), $MachinePrecision], N[(N[(2 * c), $MachinePrecision] / N[((-b) + t$95$0), $MachinePrecision]), $MachinePrecision]]]

Alternative 1: 99.8% accurate, 1.3× speedup

Math

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (if (>= b 0)
  (* (/ (+ (4-sqrtz0z0z1z24 b c a) b) a) -1/2)
  (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))

Derivation

1. Initial program 72.1%

   \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
2. Step-by-step derivation

   1. lift-sqrt.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. lift--.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   5. associate-*l* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   6. fp-cancel-sub-sign-inv N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   7. distribute-lft-neg-in N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   8. distribute-rgt-neg-in N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   9. fp-cancel-sign-sub-inv N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   10. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   11. sqr-neg-rev N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   12. lift-neg.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   13. lift-neg.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   14. sqr-neg-rev N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   15. distribute-rgt-neg-in N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   16. distribute-lft-neg-in N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   17. metadata-eval N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   18. metadata-eval N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   19. associate-*l* N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   20. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   21. *-commutative N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   22. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   23. *-commutative N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

3. Applied rewrites 85.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
4. Step-by-step derivation

   1. lift-sqrt.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

   2. lift--.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   5. associate-*l* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

   6. fp-cancel-sub-sign-inv N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

   7. distribute-lft-neg-in N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

   8. distribute-rgt-neg-in N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   9. fp-cancel-sign-sub-inv N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   10. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   11. sqr-neg-rev N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   12. lift-neg.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   13. lift-neg.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   14. sqr-neg-rev N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

   15. distribute-rgt-neg-in N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

   16. distribute-lft-neg-in N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

   17. metadata-eval N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

   18. metadata-eval N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

   19. associate-*l* N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   20. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   21. *-commutative N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

   22. lift-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

   23. *-commutative N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

5. Applied rewrites 99.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

7. Applied rewrites 99.8%

   \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]
8. Add Preprocessing

Alternative 2: 99.7% accurate, 1.3× speedup

Math

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(b + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (if (>= b 0)
  (* (/ -1/2 a) (+ b (4-sqrtz0z0z1z24 b c a)))
  (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))

Derivation

1. Initial program 72.1%

   \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

3. Applied rewrites 99.7%

   \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(b + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]
4. Add Preprocessing

Alternative 3: 89.9% accurate, 1.1× speedup

Math

\[\begin{array}{l} t_0 := \frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \mathbf{if}\;b \leq \frac{7855335333859531}{7410693711188236507108543040556026102609279018600996098525285376506440296955904}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\frac{2 \cdot b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))
  (if (<=
       b
       7855335333859531/7410693711188236507108543040556026102609279018600996098525285376506440296955904)
    (if (>= b 0) (* (* c (sqrt (/ -4 (* a c)))) 1/2) t_0)
    (if (>= b 0) (* (/ (* 2 b) a) -1/2) t_0))))

Derivation

1. Split input into 2 regimes

2. if b < 1.06e-63

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Taylor expanded in a around -inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lower-/.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. Applied rewrites 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. *-commutative N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lower-*.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. *-commutative N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. lower-*.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(lift-*.f64, \left(2 \cdot c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(count-2-rev, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite<=}\left(lift-+.f64, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lower-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(lift-+.f64, \left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right)\right)}\\ \end{array} \]

      11. lower-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(+-commutative, \left(\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)\right)\right)}\\ \end{array} \]

   6. Applied rewrites 57.5%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   7. Taylor expanded in c around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   8. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      2. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      3. lower-/.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      4. lower-*.f64 64.3%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   9. Applied rewrites 64.3%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(c \cdot \sqrt{\frac{-4}{a \cdot c}}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   if 1.06e-63 < b

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   2. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 85.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

   5. Applied rewrites 99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

   7. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   8. Taylor expanded in b around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\color{blue}{2 \cdot b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   9. Step-by-step derivation

      1. lower-*.f64 83.5%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{2 \cdot \color{blue}{b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   10. Applied rewrites 83.5%

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\color{blue}{2 \cdot b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 85.3% accurate, 1.2× speedup

Math

\[\begin{array}{l} t_0 := \frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \mathbf{if}\;b \leq \frac{5687876567655377}{18347988927920572092886567162416695526372519913346248989900710715095383008707878464560148424881005492436992}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\frac{2 \cdot b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))
  (if (<=
       b
       5687876567655377/18347988927920572092886567162416695526372519913346248989900710715095383008707878464560148424881005492436992)
    (if (>= b 0) (* (sqrt (* -4 (/ c a))) -1/2) t_0)
    (if (>= b 0) (* (/ (* 2 b) a) -1/2) t_0))))

Derivation

1. Split input into 2 regimes

2. if b < 3.0999999999999998e-91

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   2. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 85.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

   5. Applied rewrites 99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

   7. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   8. Taylor expanded in a around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   9. Step-by-step derivation

      1. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      2. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      3. lower-/.f64 57.0%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   10. Applied rewrites 57.0%

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   if 3.0999999999999998e-91 < b

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   2. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 85.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

   5. Applied rewrites 99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

   7. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   8. Taylor expanded in b around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\color{blue}{2 \cdot b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   9. Step-by-step derivation

      1. lower-*.f64 83.5%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{2 \cdot \color{blue}{b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   10. Applied rewrites 83.5%

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\color{blue}{2 \cdot b}}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 85.2% accurate, 1.2× speedup

Math

\[\begin{array}{l} t_0 := \frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \mathbf{if}\;b \leq \frac{5687876567655377}{18347988927920572092886567162416695526372519913346248989900710715095383008707878464560148424881005492436992}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(2 \cdot b\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))
  (if (<=
       b
       5687876567655377/18347988927920572092886567162416695526372519913346248989900710715095383008707878464560148424881005492436992)
    (if (>= b 0) (* (sqrt (* -4 (/ c a))) -1/2) t_0)
    (if (>= b 0) (* (/ -1/2 a) (* 2 b)) t_0))))

Derivation

1. Split input into 2 regimes

2. if b < 3.0999999999999998e-91

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   2. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 85.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

   5. Applied rewrites 99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

   7. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   8. Taylor expanded in a around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   9. Step-by-step derivation

      1. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      2. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      3. lower-/.f64 57.0%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   10. Applied rewrites 57.0%

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   if 3.0999999999999998e-91 < b

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 99.7%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(b + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   4. Taylor expanded in b around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \color{blue}{\left(2 \cdot b\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   5. Step-by-step derivation

      1. lower-*.f64 83.4%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(2 \cdot \color{blue}{b}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   6. Applied rewrites 83.4%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \color{blue}{\left(2 \cdot b\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 64.3% accurate, 1.2× speedup

Math

\[\begin{array}{l} t_0 := \frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \mathbf{if}\;a \leq \frac{-2613896909433603}{580865979874134008905493163339804906301273516273200960568660882545289319203282958416081372850061074449140126480544130097833822361540978792105793195743122900696472984549789013258861878841522553464937185852481030158620214338624171909436366773573694563676580119318024965946783339380736}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (let* ((t_0 (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))
  (if (<=
       a
       -2613896909433603/580865979874134008905493163339804906301273516273200960568660882545289319203282958416081372850061074449140126480544130097833822361540978792105793195743122900696472984549789013258861878841522553464937185852481030158620214338624171909436366773573694563676580119318024965946783339380736)
    (if (>= b 0) (* (sqrt (* (/ c a) -4)) 1/2) t_0)
    (if (>= b 0) (* (sqrt (* -4 (/ c a))) -1/2) t_0))))

Derivation

1. Split input into 2 regimes

2. if a < -4.4999999999999999e-267

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Taylor expanded in a around -inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lower-/.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. Applied rewrites 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. *-commutative N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lower-*.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. *-commutative N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. lower-*.f64 43.6%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(lift-*.f64, \left(2 \cdot c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(count-2-rev, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite<=}\left(lift-+.f64, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lower-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(lift-+.f64, \left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right)\right)}\\ \end{array} \]

      11. lower-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(+-commutative, \left(\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)\right)\right)}\\ \end{array} \]

   6. Applied rewrites 57.5%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   if -4.4999999999999999e-267 < a

   1. Initial program 72.1%

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   2. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \color{blue}{4 \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \color{blue}{4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{b \cdot b} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(-b\right)} \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(-b\right) \cdot \color{blue}{\left(-b\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right)} - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\color{blue}{-4}\right)\right) \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{4} \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{\left(4 \cdot a\right)} \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \color{blue}{c \cdot \left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(4 \cdot a\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \color{blue}{\left(a \cdot 4\right)}}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. Applied rewrites 85.9%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
   4. Step-by-step derivation

      1. lift-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}\\ \end{array} \]

      2. lift--.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      3. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      4. lift-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      5. associate-*l* N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      6. fp-cancel-sub-sign-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      7. distribute-lft-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + \left(\mathsf{neg}\left(4 \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      8. distribute-rgt-neg-in N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b + 4 \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      9. fp-cancel-sign-sub-inv N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right)} + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      10. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{b \cdot b - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      11. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(b\right)\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      12. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(\mathsf{neg}\left(b\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      13. lift-neg.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(-b\right) \cdot \left(-b\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      14. sqr-neg-rev N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-\color{blue}{b}\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(4\right)\right) \cdot \left(\mathsf{neg}\left(a \cdot c\right)\right)}}\\ \end{array} \]

      15. distribute-rgt-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right) \cdot \left(a \cdot c\right)\right)\right)}}\\ \end{array} \]

      16. distribute-lft-neg-in N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(4\right)\right)\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      17. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(\mathsf{neg}\left(-4\right)\right) \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      18. metadata-eval N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - 4 \cdot \left(a \cdot c\right)}}\\ \end{array} \]

      19. associate-*l* N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      20. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

      21. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      22. lift-*.f64 N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(4 \cdot a\right)}}\\ \end{array} \]

      23. *-commutative N/A

          \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{\left(\mathsf{neg}\left(\left(-b\right)\right)\right) \cdot \left(\mathsf{neg}\left(\left(-b\right)\right)\right) - c \cdot \left(a \cdot 4\right)}}\\ \end{array} \]

   5. Applied rewrites 99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\color{blue}{\left(-b\right) + \mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right)}}\\ \end{array} \]

   7. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) + b}{a} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]

   8. Taylor expanded in a around inf

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
   9. Step-by-step derivation

      1. lower-sqrt.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      2. lower-*.f64 N/A

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

      3. lower-/.f64 57.0%

         \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   10. Applied rewrites 57.0%

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\sqrt{-4 \cdot \frac{c}{a}}} \cdot \frac{-1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 57.5% accurate, 1.3× speedup

Math

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (if (>= b 0)
  (* (sqrt (* (/ c a) -4)) 1/2)
  (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))

Derivation

1. Initial program 72.1%

   \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

2. Taylor expanded in a around -inf

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
3. Step-by-step derivation

   1. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. lower-sqrt.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lower-/.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

4. Applied rewrites 43.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lower-*.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   5. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   6. lower-*.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   7. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(lift-*.f64, \left(2 \cdot c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   8. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(count-2-rev, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   9. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite<=}\left(lift-+.f64, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   10. lower-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(lift-+.f64, \left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right)\right)}\\ \end{array} \]

   11. lower-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(+-commutative, \left(\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)\right)\right)}\\ \end{array} \]

6. Applied rewrites 57.5%

   \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]
7. Add Preprocessing

Alternative 8: 57.5% accurate, 1.3× speedup

Math

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{c \cdot \frac{-4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

FPCore

(FPCore (a b c)
  :precision binary64
  (if (>= b 0)
  (* (sqrt (* c (/ -4 a))) 1/2)
  (/ (+ c c) (- (4-sqrtz0z0z1z24 b c a) b))))

Derivation

1. Initial program 72.1%

   \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

2. Taylor expanded in a around -inf

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
3. Step-by-step derivation

   1. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. lower-sqrt.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lower-/.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

4. Applied rewrites 43.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{1}{2} \cdot \sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{1}{2} \cdot \color{blue}{\sqrt{-4 \cdot \frac{c}{a}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   3. lower-*.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \color{blue}{\frac{1}{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   4. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{-4 \cdot \frac{c}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   5. *-commutative N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   6. lower-*.f64 43.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   7. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(lift-*.f64, \left(2 \cdot c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   8. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite=>}\left(count-2-rev, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   9. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{Rewrite<=}\left(lift-+.f64, \left(c + c\right)\right)}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   10. lower-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(lift-+.f64, \left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right)\right)}\\ \end{array} \]

   11. lower-*.f64 N/A

       \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{Rewrite=>}\left(+-commutative, \left(\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)\right)\right)}\\ \end{array} \]

6. Applied rewrites 57.5%

   \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ } \end{array}} \]
7. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   2. lift-/.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c}{a} \cdot -4} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   3. associate-*l/ N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{\frac{c \cdot -4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   4. associate-/l* N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{c \cdot \frac{-4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   5. lower-*.f64 N/A

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{c \cdot \frac{-4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

   6. lower-/.f64 57.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{c \cdot \frac{-4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]

8. Applied rewrites 57.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\sqrt{c \cdot \frac{-4}{a}} \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c + c}{\mathsf{4\_sqrtz0z0z1z24}\left(b, c, a\right) - b}\\ \end{array} \]
9. Add Preprocessing

Reproduce

herbie shell --seed 2025271 -o generate:evaluate
(FPCore (a b c)
  :name "jeff quadratic root 1"
  :precision binary64
  (if (>= b 0) (/ (- (- b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (- b) (sqrt (- (* b b) (* (* 4 a) c)))))))