Octave 3.8, jcobi/4

Percentage Accurate: 16.6% → 99.7%

Time: 5.9s

Alternatives: 1

Speedup: 0.9×

Specification

\[\left(\alpha > -1 \land \beta > -1\right) \land i > 1\]

Math

\[\begin{array}{l} t_0 := i \cdot \left(\left(\alpha + \beta\right) + i\right)\\ t_1 := \left(\alpha + \beta\right) + 2 \cdot i\\ t_2 := t\_1 \cdot t\_1\\ \frac{\frac{t\_0 \cdot \left(\beta \cdot \alpha + t\_0\right)}{t\_2}}{t\_2 - 1} \end{array} \]

FPCore

(FPCore (alpha beta i)
 :precision binary64
 (let* ((t_0 (* i (+ (+ alpha beta) i)))
        (t_1 (+ (+ alpha beta) (* 2.0 i)))
        (t_2 (* t_1 t_1)))
   (/ (/ (* t_0 (+ (* beta alpha) t_0)) t_2) (- t_2 1.0))))

C

double code(double alpha, double beta, double i) {
	double t_0 = i * ((alpha + beta) + i);
	double t_1 = (alpha + beta) + (2.0 * i);
	double t_2 = t_1 * t_1;
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
}

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(alpha, beta, i)
use fmin_fmax_functions
    real(8), intent (in) :: alpha
    real(8), intent (in) :: beta
    real(8), intent (in) :: i
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: t_2
    t_0 = i * ((alpha + beta) + i)
    t_1 = (alpha + beta) + (2.0d0 * i)
    t_2 = t_1 * t_1
    code = ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0d0)
end function

Java

public static double code(double alpha, double beta, double i) {
	double t_0 = i * ((alpha + beta) + i);
	double t_1 = (alpha + beta) + (2.0 * i);
	double t_2 = t_1 * t_1;
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
}

Python

def code(alpha, beta, i):
	t_0 = i * ((alpha + beta) + i)
	t_1 = (alpha + beta) + (2.0 * i)
	t_2 = t_1 * t_1
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0)

Julia

function code(alpha, beta, i)
	t_0 = Float64(i * Float64(Float64(alpha + beta) + i))
	t_1 = Float64(Float64(alpha + beta) + Float64(2.0 * i))
	t_2 = Float64(t_1 * t_1)
	return Float64(Float64(Float64(t_0 * Float64(Float64(beta * alpha) + t_0)) / t_2) / Float64(t_2 - 1.0))
end

MATLAB

function tmp = code(alpha, beta, i)
	t_0 = i * ((alpha + beta) + i);
	t_1 = (alpha + beta) + (2.0 * i);
	t_2 = t_1 * t_1;
	tmp = ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
end

Wolfram

code[alpha_, beta_, i_] := Block[{t$95$0 = N[(i * N[(N[(alpha + beta), $MachinePrecision] + i), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t$95$1 * t$95$1), $MachinePrecision]}, N[(N[(N[(t$95$0 * N[(N[(beta * alpha), $MachinePrecision] + t$95$0), $MachinePrecision]), $MachinePrecision] / t$95$2), $MachinePrecision] / N[(t$95$2 - 1.0), $MachinePrecision]), $MachinePrecision]]]]

Initial Program: 16.6% accurate, 1.0× speedup

Math

\[\begin{array}{l} t_0 := i \cdot \left(\left(\alpha + \beta\right) + i\right)\\ t_1 := \left(\alpha + \beta\right) + 2 \cdot i\\ t_2 := t\_1 \cdot t\_1\\ \frac{\frac{t\_0 \cdot \left(\beta \cdot \alpha + t\_0\right)}{t\_2}}{t\_2 - 1} \end{array} \]

FPCore

(FPCore (alpha beta i)
 :precision binary64
 (let* ((t_0 (* i (+ (+ alpha beta) i)))
        (t_1 (+ (+ alpha beta) (* 2.0 i)))
        (t_2 (* t_1 t_1)))
   (/ (/ (* t_0 (+ (* beta alpha) t_0)) t_2) (- t_2 1.0))))

C

double code(double alpha, double beta, double i) {
	double t_0 = i * ((alpha + beta) + i);
	double t_1 = (alpha + beta) + (2.0 * i);
	double t_2 = t_1 * t_1;
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
}

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(alpha, beta, i)
use fmin_fmax_functions
    real(8), intent (in) :: alpha
    real(8), intent (in) :: beta
    real(8), intent (in) :: i
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: t_2
    t_0 = i * ((alpha + beta) + i)
    t_1 = (alpha + beta) + (2.0d0 * i)
    t_2 = t_1 * t_1
    code = ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0d0)
end function

Java

public static double code(double alpha, double beta, double i) {
	double t_0 = i * ((alpha + beta) + i);
	double t_1 = (alpha + beta) + (2.0 * i);
	double t_2 = t_1 * t_1;
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
}

Python

def code(alpha, beta, i):
	t_0 = i * ((alpha + beta) + i)
	t_1 = (alpha + beta) + (2.0 * i)
	t_2 = t_1 * t_1
	return ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0)

Julia

function code(alpha, beta, i)
	t_0 = Float64(i * Float64(Float64(alpha + beta) + i))
	t_1 = Float64(Float64(alpha + beta) + Float64(2.0 * i))
	t_2 = Float64(t_1 * t_1)
	return Float64(Float64(Float64(t_0 * Float64(Float64(beta * alpha) + t_0)) / t_2) / Float64(t_2 - 1.0))
end

MATLAB

function tmp = code(alpha, beta, i)
	t_0 = i * ((alpha + beta) + i);
	t_1 = (alpha + beta) + (2.0 * i);
	t_2 = t_1 * t_1;
	tmp = ((t_0 * ((beta * alpha) + t_0)) / t_2) / (t_2 - 1.0);
end

Wolfram

code[alpha_, beta_, i_] := Block[{t$95$0 = N[(i * N[(N[(alpha + beta), $MachinePrecision] + i), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t$95$1 * t$95$1), $MachinePrecision]}, N[(N[(N[(t$95$0 * N[(N[(beta * alpha), $MachinePrecision] + t$95$0), $MachinePrecision]), $MachinePrecision] / t$95$2), $MachinePrecision] / N[(t$95$2 - 1.0), $MachinePrecision]), $MachinePrecision]]]]

Alternative 1: 99.7% accurate, 0.9× speedup

Math

\[\begin{array}{l} t_0 := \mathsf{fma}\left(2, i, \beta + \alpha\right)\\ t_1 := \left(\left(\alpha + \beta\right) + i\right) + i\\ t_2 := \left(\beta + \alpha\right) + i\\ \frac{\mathsf{fma}\left(\frac{i}{t\_1}, t\_2, \beta \cdot \frac{\alpha}{t\_1}\right)}{t\_1 - 1} \cdot \frac{\frac{i}{t\_0} \cdot t\_2}{t\_0 - -1} \end{array} \]

FPCore

(FPCore (alpha beta i)
 :precision binary64
 (let* ((t_0 (fma 2.0 i (+ beta alpha)))
        (t_1 (+ (+ (+ alpha beta) i) i))
        (t_2 (+ (+ beta alpha) i)))
   (*
    (/ (fma (/ i t_1) t_2 (* beta (/ alpha t_1))) (- t_1 1.0))
    (/ (* (/ i t_0) t_2) (- t_0 -1.0)))))

C

double code(double alpha, double beta, double i) {
	double t_0 = fma(2.0, i, (beta + alpha));
	double t_1 = ((alpha + beta) + i) + i;
	double t_2 = (beta + alpha) + i;
	return (fma((i / t_1), t_2, (beta * (alpha / t_1))) / (t_1 - 1.0)) * (((i / t_0) * t_2) / (t_0 - -1.0));
}

Julia

function code(alpha, beta, i)
	t_0 = fma(2.0, i, Float64(beta + alpha))
	t_1 = Float64(Float64(Float64(alpha + beta) + i) + i)
	t_2 = Float64(Float64(beta + alpha) + i)
	return Float64(Float64(fma(Float64(i / t_1), t_2, Float64(beta * Float64(alpha / t_1))) / Float64(t_1 - 1.0)) * Float64(Float64(Float64(i / t_0) * t_2) / Float64(t_0 - -1.0)))
end

Wolfram

code[alpha_, beta_, i_] := Block[{t$95$0 = N[(2.0 * i + N[(beta + alpha), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(N[(alpha + beta), $MachinePrecision] + i), $MachinePrecision] + i), $MachinePrecision]}, Block[{t$95$2 = N[(N[(beta + alpha), $MachinePrecision] + i), $MachinePrecision]}, N[(N[(N[(N[(i / t$95$1), $MachinePrecision] * t$95$2 + N[(beta * N[(alpha / t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(t$95$1 - 1.0), $MachinePrecision]), $MachinePrecision] * N[(N[(N[(i / t$95$0), $MachinePrecision] * t$95$2), $MachinePrecision] / N[(t$95$0 - -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]

Derivation

1. Initial program 16.6%

   \[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
2. Step-by-step derivation

   1. lift-/.f64 N/A

      \[\leadsto \color{blue}{\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}} \]

   2. lift-/.f64 N/A

      \[\leadsto \frac{\color{blue}{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]

   3. lift-*.f64 N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]

   4. *-commutative N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]

   5. lift-*.f64 N/A

      \[\leadsto \frac{\frac{\left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\color{blue}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]

   6. times-frac N/A

      \[\leadsto \frac{\color{blue}{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]

   7. lift--.f64 N/A

      \[\leadsto \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\color{blue}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}} \]

   8. lift-*.f64 N/A

      \[\leadsto \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\color{blue}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)} - 1} \]

3. Applied rewrites 43.2%

   \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(\left(\beta + \alpha\right) + i, i, \beta \cdot \alpha\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1}} \]
4. Step-by-step derivation

   1. lift-/.f64 N/A

      \[\leadsto \frac{\color{blue}{\frac{\mathsf{fma}\left(\left(\beta + \alpha\right) + i, i, \beta \cdot \alpha\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   2. lift-fma.f64 N/A

      \[\leadsto \frac{\frac{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) \cdot i + \beta \cdot \alpha}}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   3. div-add N/A

      \[\leadsto \frac{\color{blue}{\frac{\left(\left(\beta + \alpha\right) + i\right) \cdot i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} + \frac{\beta \cdot \alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   4. associate-*r/ N/A

      \[\leadsto \frac{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}} + \frac{\beta \cdot \alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   5. lift-/.f64 N/A

      \[\leadsto \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \color{blue}{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}} + \frac{\beta \cdot \alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   6. *-commutative N/A

      \[\leadsto \frac{\color{blue}{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} \cdot \left(\left(\beta + \alpha\right) + i\right)} + \frac{\beta \cdot \alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   7. lower-fma.f64 N/A

      \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \frac{\beta \cdot \alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   8. lift-*.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \frac{\color{blue}{\beta \cdot \alpha}}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   9. associate-/l* N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \color{blue}{\beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   10. lower-*.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \color{blue}{\beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   11. lower-/.f64 99.6%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \beta \cdot \color{blue}{\frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

5. Applied rewrites 99.6%

   \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]
6. Step-by-step derivation

   1. lift-fma.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{2 \cdot i + \left(\beta + \alpha\right)}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   2. +-commutative N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{\left(\beta + \alpha\right) + 2 \cdot i}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   3. count-2-rev N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\beta + \alpha\right) + \color{blue}{\left(i + i\right)}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   4. associate-+r+ N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   5. lift-+.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right)} + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   6. lower-+.f64 99.7%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   7. lift-+.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\color{blue}{\left(\beta + \alpha\right)} + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   8. +-commutative N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   9. lift-+.f64 99.7%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

7. Applied rewrites 99.7%

   \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\color{blue}{\left(\left(\alpha + \beta\right) + i\right) + i}}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]
8. Step-by-step derivation

   1. lift-fma.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{2 \cdot i + \left(\beta + \alpha\right)}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   2. +-commutative N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{\left(\beta + \alpha\right) + 2 \cdot i}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   3. count-2-rev N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\beta + \alpha\right) + \color{blue}{\left(i + i\right)}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   4. associate-+r+ N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   5. lift-+.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right)} + i}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   6. lower-+.f64 99.7%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   7. lift-+.f64 N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\color{blue}{\left(\beta + \alpha\right)} + i\right) + i}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   8. +-commutative N/A

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

   9. lift-+.f64 99.7%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

9. Applied rewrites 99.7%

   \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\color{blue}{\left(\left(\alpha + \beta\right) + i\right) + i}}\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]
10. Step-by-step derivation

    1. lift-fma.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\color{blue}{\left(2 \cdot i + \left(\beta + \alpha\right)\right)} - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    2. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\color{blue}{\left(\left(\beta + \alpha\right) + 2 \cdot i\right)} - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    3. count-2-rev N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\beta + \alpha\right) + \color{blue}{\left(i + i\right)}\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    4. associate-+r+ N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\color{blue}{\left(\left(\left(\beta + \alpha\right) + i\right) + i\right)} - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    5. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\color{blue}{\left(\left(\beta + \alpha\right) + i\right)} + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    6. lower-+.f64 99.7%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\color{blue}{\left(\left(\left(\beta + \alpha\right) + i\right) + i\right)} - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    7. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\color{blue}{\left(\beta + \alpha\right)} + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    8. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    9. lift-+.f64 99.7%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

11. Applied rewrites 99.7%

    \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\color{blue}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right)} - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]
12. Step-by-step derivation

    1. lift-fma.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{2 \cdot i + \left(\beta + \alpha\right)}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    2. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{\left(\beta + \alpha\right) + 2 \cdot i}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    3. count-2-rev N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\beta + \alpha\right) + \color{blue}{\left(i + i\right)}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    4. associate-+r+ N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    5. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right)} + i}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    6. lower-+.f64 99.7%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) + i}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    7. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\color{blue}{\left(\beta + \alpha\right)} + i\right) + i}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    8. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

    9. lift-+.f64 99.7%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]

13. Applied rewrites 99.7%

    \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\color{blue}{\left(\left(\alpha + \beta\right) + i\right) + i}}}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1} \]
14. Step-by-step derivation

    1. lift-fma.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\color{blue}{\left(2 \cdot i + \left(\beta + \alpha\right)\right)} - -1} \]

    2. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\color{blue}{\left(\left(\beta + \alpha\right) + 2 \cdot i\right)} - -1} \]

    3. count-2-rev N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\left(\left(\beta + \alpha\right) + \color{blue}{\left(i + i\right)}\right) - -1} \]

    4. associate-+r+ N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\color{blue}{\left(\left(\left(\beta + \alpha\right) + i\right) + i\right)} - -1} \]

    5. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\left(\color{blue}{\left(\left(\beta + \alpha\right) + i\right)} + i\right) - -1} \]

    6. lower-+.f64 99.6%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\color{blue}{\left(\left(\left(\beta + \alpha\right) + i\right) + i\right)} - -1} \]

    7. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\left(\left(\color{blue}{\left(\beta + \alpha\right)} + i\right) + i\right) - -1} \]

    8. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\left(\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i\right) - -1} \]

    9. lift-+.f64 99.6%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\left(\left(\color{blue}{\left(\alpha + \beta\right)} + i\right) + i\right) - -1} \]

15. Applied rewrites 99.6%

    \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}{\color{blue}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right)} - -1} \]
16. Step-by-step derivation

    1. lift-*.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\color{blue}{\left(\left(\beta + \alpha\right) + i\right) \cdot \frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}}}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    2. *-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\color{blue}{\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i} \cdot \left(\left(\beta + \alpha\right) + i\right)}}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    3. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i} \cdot \left(\color{blue}{\left(\beta + \alpha\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    4. +-commutative N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i} \cdot \left(\color{blue}{\left(\alpha + \beta\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    5. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i} \cdot \left(\color{blue}{\left(\alpha + \beta\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    6. lower-*.f64 99.6%

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\color{blue}{\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i} \cdot \left(\left(\alpha + \beta\right) + i\right)}}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    7. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\left(\alpha + \beta\right) + i\right) + i}} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    8. lift-+.f64 N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\left(\alpha + \beta\right) + i\right)} + i} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    9. associate-+l+ N/A

       \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\alpha + \beta\right) + \left(i + i\right)}} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    10. lift-+.f64 N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\alpha + \beta\right)} + \left(i + i\right)} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    11. count-2-rev N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\left(\alpha + \beta\right) + \color{blue}{2 \cdot i}} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    12. +-commutative N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\beta + \alpha\right)} + 2 \cdot i} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    13. lift-+.f64 N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\left(\beta + \alpha\right)} + 2 \cdot i} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    14. +-commutative N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{2 \cdot i + \left(\beta + \alpha\right)}} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    15. lift-fma.f64 99.7%

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\color{blue}{\mathsf{fma}\left(2, i, \beta + \alpha\right)}} \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    16. lift-+.f64 N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} \cdot \left(\color{blue}{\left(\alpha + \beta\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    17. +-commutative N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} \cdot \left(\color{blue}{\left(\beta + \alpha\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

    18. lift-+.f64 99.7%

        \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \frac{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} \cdot \left(\color{blue}{\left(\beta + \alpha\right)} + i\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - -1} \]

17. Applied rewrites 99.7%

    \[\leadsto \frac{\mathsf{fma}\left(\frac{i}{\left(\left(\alpha + \beta\right) + i\right) + i}, \left(\beta + \alpha\right) + i, \beta \cdot \frac{\alpha}{\left(\left(\alpha + \beta\right) + i\right) + i}\right)}{\left(\left(\left(\alpha + \beta\right) + i\right) + i\right) - 1} \cdot \color{blue}{\frac{\frac{i}{\mathsf{fma}\left(2, i, \beta + \alpha\right)} \cdot \left(\left(\beta + \alpha\right) + i\right)}{\mathsf{fma}\left(2, i, \beta + \alpha\right) - -1}} \]
18. Add Preprocessing

Reproduce

herbie shell --seed 2025192 
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/4"
  :precision binary64
  :pre (and (and (> alpha -1.0) (> beta -1.0)) (> i 1.0))
  (/ (/ (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i)))) (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i)))) (- (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i))) 1.0)))