powComplex, imaginary part

Percentage Accurate: 40.8% → 81.2%

Time: 53.9s

Alternatives: 9

Speedup: 2.0×

• 64.2% of points produce a very large (infinite) output. You may want to add a precondition.

Specification

Math

\[\begin{array}{l} t_0 := \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\\ e^{t\_0 \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(t\_0 \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (log (sqrt (+ (* x.re x.re) (* x.im x.im))))))
  (*
   (exp (- (* t_0 y.re) (* (atan2 x.im x.re) y.im)))
   (sin (+ (* t_0 y.im) (* (atan2 x.im x.re) y.re))))))

C

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	double t_0 = log(sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	return exp(((t_0 * y_46_re) - (atan2(x_46_im, x_46_re) * y_46_im))) * sin(((t_0 * y_46_im) + (atan2(x_46_im, x_46_re) * y_46_re)));
}

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(x_46re, x_46im, y_46re, y_46im)
use fmin_fmax_functions
    real(8), intent (in) :: x_46re
    real(8), intent (in) :: x_46im
    real(8), intent (in) :: y_46re
    real(8), intent (in) :: y_46im
    real(8) :: t_0
    t_0 = log(sqrt(((x_46re * x_46re) + (x_46im * x_46im))))
    code = exp(((t_0 * y_46re) - (atan2(x_46im, x_46re) * y_46im))) * sin(((t_0 * y_46im) + (atan2(x_46im, x_46re) * y_46re)))
end function

Java

public static double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	double t_0 = Math.log(Math.sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	return Math.exp(((t_0 * y_46_re) - (Math.atan2(x_46_im, x_46_re) * y_46_im))) * Math.sin(((t_0 * y_46_im) + (Math.atan2(x_46_im, x_46_re) * y_46_re)));
}

Python

def code(x_46_re, x_46_im, y_46_re, y_46_im):
	t_0 = math.log(math.sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))))
	return math.exp(((t_0 * y_46_re) - (math.atan2(x_46_im, x_46_re) * y_46_im))) * math.sin(((t_0 * y_46_im) + (math.atan2(x_46_im, x_46_re) * y_46_re)))

Julia

function code(x_46_re, x_46_im, y_46_re, y_46_im)
	t_0 = log(sqrt(Float64(Float64(x_46_re * x_46_re) + Float64(x_46_im * x_46_im))))
	return Float64(exp(Float64(Float64(t_0 * y_46_re) - Float64(atan(x_46_im, x_46_re) * y_46_im))) * sin(Float64(Float64(t_0 * y_46_im) + Float64(atan(x_46_im, x_46_re) * y_46_re))))
end

MATLAB

function tmp = code(x_46_re, x_46_im, y_46_re, y_46_im)
	t_0 = log(sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	tmp = exp(((t_0 * y_46_re) - (atan2(x_46_im, x_46_re) * y_46_im))) * sin(((t_0 * y_46_im) + (atan2(x_46_im, x_46_re) * y_46_re)));
end

Wolfram

code[x$46$re_, x$46$im_, y$46$re_, y$46$im_] := Block[{t$95$0 = N[Log[N[Sqrt[N[(N[(x$46$re * x$46$re), $MachinePrecision] + N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]}, N[(N[Exp[N[(N[(t$95$0 * y$46$re), $MachinePrecision] - N[(N[ArcTan[x$46$im / x$46$re], $MachinePrecision] * y$46$im), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(N[(t$95$0 * y$46$im), $MachinePrecision] + N[(N[ArcTan[x$46$im / x$46$re], $MachinePrecision] * y$46$re), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]

Initial Program: 40.8% accurate, 1.0× speedup

Math

\[\begin{array}{l} t_0 := \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\\ e^{t\_0 \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(t\_0 \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (log (sqrt (+ (* x.re x.re) (* x.im x.im))))))
  (*
   (exp (- (* t_0 y.re) (* (atan2 x.im x.re) y.im)))
   (sin (+ (* t_0 y.im) (* (atan2 x.im x.re) y.re))))))

C

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	double t_0 = log(sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	return exp(((t_0 * y_46_re) - (atan2(x_46_im, x_46_re) * y_46_im))) * sin(((t_0 * y_46_im) + (atan2(x_46_im, x_46_re) * y_46_re)));
}

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(x_46re, x_46im, y_46re, y_46im)
use fmin_fmax_functions
    real(8), intent (in) :: x_46re
    real(8), intent (in) :: x_46im
    real(8), intent (in) :: y_46re
    real(8), intent (in) :: y_46im
    real(8) :: t_0
    t_0 = log(sqrt(((x_46re * x_46re) + (x_46im * x_46im))))
    code = exp(((t_0 * y_46re) - (atan2(x_46im, x_46re) * y_46im))) * sin(((t_0 * y_46im) + (atan2(x_46im, x_46re) * y_46re)))
end function

Java

public static double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	double t_0 = Math.log(Math.sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	return Math.exp(((t_0 * y_46_re) - (Math.atan2(x_46_im, x_46_re) * y_46_im))) * Math.sin(((t_0 * y_46_im) + (Math.atan2(x_46_im, x_46_re) * y_46_re)));
}

Python

def code(x_46_re, x_46_im, y_46_re, y_46_im):
	t_0 = math.log(math.sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))))
	return math.exp(((t_0 * y_46_re) - (math.atan2(x_46_im, x_46_re) * y_46_im))) * math.sin(((t_0 * y_46_im) + (math.atan2(x_46_im, x_46_re) * y_46_re)))

Julia

function code(x_46_re, x_46_im, y_46_re, y_46_im)
	t_0 = log(sqrt(Float64(Float64(x_46_re * x_46_re) + Float64(x_46_im * x_46_im))))
	return Float64(exp(Float64(Float64(t_0 * y_46_re) - Float64(atan(x_46_im, x_46_re) * y_46_im))) * sin(Float64(Float64(t_0 * y_46_im) + Float64(atan(x_46_im, x_46_re) * y_46_re))))
end

MATLAB

function tmp = code(x_46_re, x_46_im, y_46_re, y_46_im)
	t_0 = log(sqrt(((x_46_re * x_46_re) + (x_46_im * x_46_im))));
	tmp = exp(((t_0 * y_46_re) - (atan2(x_46_im, x_46_re) * y_46_im))) * sin(((t_0 * y_46_im) + (atan2(x_46_im, x_46_re) * y_46_re)));
end

Wolfram

code[x$46$re_, x$46$im_, y$46$re_, y$46$im_] := Block[{t$95$0 = N[Log[N[Sqrt[N[(N[(x$46$re * x$46$re), $MachinePrecision] + N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], $MachinePrecision]}, N[(N[Exp[N[(N[(t$95$0 * y$46$re), $MachinePrecision] - N[(N[ArcTan[x$46$im / x$46$re], $MachinePrecision] * y$46$im), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[Sin[N[(N[(t$95$0 * y$46$im), $MachinePrecision] + N[(N[ArcTan[x$46$im / x$46$re], $MachinePrecision] * y$46$re), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]

Alternative 1: 81.2% accurate, 1.4× speedup

Math

\[\begin{array}{l} t_0 := y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\\ \mathbf{if}\;y.im \leq 409999999999999990472932154957878370114535304606251784249590698051943254078174365087551489442461857594998784:\\ \;\;\;\;\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{e^{t\_0 - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(\pi - y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - t\_0}\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (* y.im (atan2 x.im x.re))))
  (if (<=
       y.im
       409999999999999990472932154957878370114535304606251784249590698051943254078174365087551489442461857594998784)
    (/
     (sin
      (+
       (* (atan2 x.im x.re) y.re)
       (184-logsqrtz0z0z1z1z2 x.im x.re y.im)))
     (exp (- t_0 (184-logsqrtz0z0z1z1z2 x.im x.re y.re))))
    (*
     (sin (- PI (* y.re (atan2 x.im x.re))))
     (exp (- (184-logsqrtz0z0z1z1z2 x.im x.re y.re) t_0))))))

Derivation

1. Split input into 2 regimes

2. if y.im < 4.0999999999999999e107

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lift-exp.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      4. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      5. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\mathsf{neg}\left(\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re\right)\right)}} \]

      6. exp-neg N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{\frac{1}{e^{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re}}} \]

      7. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\color{blue}{\mathsf{neg}\left(\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)\right)}}} \]

      8. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\mathsf{neg}\left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)}\right)}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}} \]

   if 4.0999999999999999e107 < y.im

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lower-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

      1. lift-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. *-lft-identity N/A

         \[\leadsto \sin \left(1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. metadata-eval N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-*.f64 N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. *-commutative N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-*.f64 N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. *-commutative N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. distribute-lft-neg-out N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      17. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      18. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      19. mul-1-neg N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      20. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      21. distribute-lft-neg-out N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re\right)\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      22. lift-atan2.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re\right)\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      23. lift-neg.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      24. lift-atan2.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      25. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   8. Applied rewrites 56.0%

      \[\leadsto \sin \left(\pi - y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 2: 81.2% accurate, 1.5× speedup

Math

\[\begin{array}{l} t_0 := e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}\\ \mathbf{if}\;y.im \leq 409999999999999990472932154957878370114535304606251784249590698051943254078174365087551489442461857594998784:\\ \;\;\;\;\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;\sin \left(\pi - y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot t\_0\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0
        (exp
         (-
          (184-logsqrtz0z0z1z1z2 x.im x.re y.re)
          (* y.im (atan2 x.im x.re))))))
  (if (<=
       y.im
       409999999999999990472932154957878370114535304606251784249590698051943254078174365087551489442461857594998784)
    (*
     (sin
      (+
       (* (atan2 x.im x.re) y.re)
       (184-logsqrtz0z0z1z1z2 x.im x.re y.im)))
     t_0)
    (* (sin (- PI (* y.re (atan2 x.im x.re)))) t_0))))

Derivation

1. Split input into 2 regimes

2. if y.im < 4.0999999999999999e107

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   if 4.0999999999999999e107 < y.im

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lower-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

      1. lift-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. *-lft-identity N/A

         \[\leadsto \sin \left(1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. metadata-eval N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-*.f64 N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. *-commutative N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-*.f64 N/A

         \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. *-commutative N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(\mathsf{neg}\left(-1\right)\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. distribute-lft-neg-out N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      17. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      18. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(-1 \cdot \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      19. mul-1-neg N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      20. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right)\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      21. distribute-lft-neg-out N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re\right)\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      22. lift-atan2.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(y.re\right)\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      23. lift-neg.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      24. lift-atan2.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      25. lift-*.f64 N/A

          \[\leadsto \sin \left(\mathsf{neg}\left(\left(-y.re\right) \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   8. Applied rewrites 56.0%

      \[\leadsto \sin \left(\pi - y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 80.5% accurate, 1.4× speedup

Math

\[\begin{array}{l} t_0 := y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\\ \mathbf{if}\;y.re \leq \frac{-1684996666696915}{3369993333393829974333376885877453834204643052817571560137951281152}:\\ \;\;\;\;\frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{t\_0 - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}\\ \mathbf{elif}\;y.re \leq \frac{1224979098644775}{36028797018963968}:\\ \;\;\;\;\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{e^{-t\_0}}}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - t\_0}\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (* y.im (atan2 x.im x.re))))
  (if (<=
       y.re
       -1684996666696915/3369993333393829974333376885877453834204643052817571560137951281152)
    (/
     (sin (* y.re (atan2 x.im x.re)))
     (exp (- t_0 (184-logsqrtz0z0z1z1z2 x.im x.re y.re))))
    (if (<= y.re 1224979098644775/36028797018963968)
      (/
       (sin
        (+
         (* (atan2 x.im x.re) y.re)
         (184-logsqrtz0z0z1z1z2 x.im x.re y.im)))
       (/ 1 (exp (- t_0))))
      (*
       (sin (* 1 (184-logsqrtz0z0z1z1z2 x.re x.im y.im)))
       (exp (- (184-logsqrtz0z0z1z1z2 x.im x.re y.re) t_0)))))))

Derivation

1. Split input into 3 regimes

2. if y.re < -5e-52

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lift-exp.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      4. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      5. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\mathsf{neg}\left(\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re\right)\right)}} \]

      6. exp-neg N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{\frac{1}{e^{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re}}} \]

      7. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\color{blue}{\mathsf{neg}\left(\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)\right)}}} \]

      8. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\mathsf{neg}\left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)}\right)}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \frac{\color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

      2. lower-*.f64 N/A

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \frac{\color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

   if -5e-52 < y.re < 0.034000000000000002

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lift-exp.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      4. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      5. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\mathsf{neg}\left(\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re\right)\right)}} \]

      6. exp-neg N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{\frac{1}{e^{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re}}} \]

      7. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\color{blue}{\mathsf{neg}\left(\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)\right)}}} \]

      8. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\mathsf{neg}\left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)}\right)}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}} \]

   5. Applied rewrites 80.8%

      \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\color{blue}{\frac{1}{e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}}} \]

   6. Taylor expanded in y.re around 0

      \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{\color{blue}{e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}}} \]
   7. Step-by-step derivation

      1. lower-exp.f64 N/A

         \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}} \]

      2. lower-neg.f64 N/A

         \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}} \]

      3. lower-*.f64 N/A

         \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}} \]

      4. lower-atan2.f64 53.2%

         \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}} \]

   8. Applied rewrites 53.2%

      \[\leadsto \frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{\frac{1}{\color{blue}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}}} \]

   if 0.034000000000000002 < y.re

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
   4. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-184-logsqrtz0z0z1z1z2 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. +-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-+.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. lift-sqrt.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-log.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. *-commutative N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. lift-*.f64 N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. +-commutative N/A

          \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. sum-to-mult N/A

          \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-log.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. Applied rewrites 72.9%

      \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

   8. Applied rewrites 70.8%

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 4: 80.5% accurate, 1.5× speedup

Math

\[\begin{array}{l} t_0 := y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\\ \mathbf{if}\;y.re \leq \frac{-1684996666696915}{3369993333393829974333376885877453834204643052817571560137951281152}:\\ \;\;\;\;\frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{t\_0 - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}\\ \mathbf{elif}\;y.re \leq \frac{1224979098644775}{36028797018963968}:\\ \;\;\;\;\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-t\_0}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - t\_0}\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (* y.im (atan2 x.im x.re))))
  (if (<=
       y.re
       -1684996666696915/3369993333393829974333376885877453834204643052817571560137951281152)
    (/
     (sin (* y.re (atan2 x.im x.re)))
     (exp (- t_0 (184-logsqrtz0z0z1z1z2 x.im x.re y.re))))
    (if (<= y.re 1224979098644775/36028797018963968)
      (*
       (sin
        (+
         (* (atan2 x.im x.re) y.re)
         (184-logsqrtz0z0z1z1z2 x.im x.re y.im)))
       (exp (- t_0)))
      (*
       (sin (* 1 (184-logsqrtz0z0z1z1z2 x.re x.im y.im)))
       (exp (- (184-logsqrtz0z0z1z1z2 x.im x.re y.re) t_0)))))))

Derivation

1. Split input into 3 regimes

2. if y.re < -5e-52

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lift-exp.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      4. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      5. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\color{blue}{\mathsf{neg}\left(\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re\right)\right)}} \]

      6. exp-neg N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \color{blue}{\frac{1}{e^{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.im - \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re}}} \]

      7. sub-negate-rev N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\color{blue}{\mathsf{neg}\left(\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)\right)}}} \]

      8. lift--.f64 N/A

         \[\leadsto \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot \frac{1}{e^{\mathsf{neg}\left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im\right)}\right)}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\frac{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \frac{\color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

      2. lower-*.f64 N/A

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \frac{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \frac{\color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right)}} \]

   if -5e-52 < y.re < 0.034000000000000002

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot \color{blue}{e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}} \]
   5. Step-by-step derivation

      1. lower-exp.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \]

      2. lower-neg.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lower-atan2.f64 53.2%

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 53.2%

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot \color{blue}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   if 0.034000000000000002 < y.re

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
   4. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-184-logsqrtz0z0z1z1z2 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. +-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-+.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. lift-sqrt.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-log.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. *-commutative N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. lift-*.f64 N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. +-commutative N/A

          \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. sum-to-mult N/A

          \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-log.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. Applied rewrites 72.9%

      \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

   8. Applied rewrites 70.8%

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 5: 80.5% accurate, 1.5× speedup

Math

\[\begin{array}{l} t_0 := y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\\ t_1 := e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - t\_0}\\ \mathbf{if}\;y.re \leq \frac{-1684996666696915}{3369993333393829974333376885877453834204643052817571560137951281152}:\\ \;\;\;\;\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot t\_1\\ \mathbf{elif}\;y.re \leq \frac{1224979098644775}{36028797018963968}:\\ \;\;\;\;\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-t\_0}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot t\_1\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (* y.im (atan2 x.im x.re)))
       (t_1 (exp (- (184-logsqrtz0z0z1z1z2 x.im x.re y.re) t_0))))
  (if (<=
       y.re
       -1684996666696915/3369993333393829974333376885877453834204643052817571560137951281152)
    (* (sin (* y.re (atan2 x.im x.re))) t_1)
    (if (<= y.re 1224979098644775/36028797018963968)
      (*
       (sin
        (+
         (* (atan2 x.im x.re) y.re)
         (184-logsqrtz0z0z1z1z2 x.im x.re y.im)))
       (exp (- t_0)))
      (* (sin (* 1 (184-logsqrtz0z0z1z1z2 x.re x.im y.im))) t_1)))))

Derivation

1. Split input into 3 regimes

2. if y.re < -5e-52

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lower-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   if -5e-52 < y.re < 0.034000000000000002

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot \color{blue}{e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}} \]
   5. Step-by-step derivation

      1. lower-exp.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \]

      2. lower-neg.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lower-atan2.f64 53.2%

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 53.2%

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot \color{blue}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   if 0.034000000000000002 < y.re

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
   4. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-184-logsqrtz0z0z1z1z2 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. +-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-+.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. lift-sqrt.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-log.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. *-commutative N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. lift-*.f64 N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. +-commutative N/A

          \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. sum-to-mult N/A

          \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-log.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. Applied rewrites 72.9%

      \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

   8. Applied rewrites 70.8%

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 6: 70.8% accurate, 1.5× speedup

Math

\[\begin{array}{l} t_0 := y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\\ \mathbf{if}\;x.re \leq \frac{-8036314553897005}{10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376}:\\ \;\;\;\;\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - t\_0}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.re\right) - t\_0}\\ \end{array} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (let* ((t_0 (* y.im (atan2 x.im x.re))))
  (if (<=
       x.re
       -8036314553897005/10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376)
    (*
     (sin (* y.re (atan2 x.im x.re)))
     (exp (- (184-logsqrtz0z0z1z1z2 x.im x.re y.re) t_0)))
    (*
     (sin (* (184-logsqrtz0z0z1z1z2 x.re x.im 1) y.im))
     (exp (- (184-logsqrtz0z0z1z1z2 x.re x.im y.re) t_0))))))

Derivation

1. Split input into 2 regimes

2. if x.re < -7.5000000000000001e-286

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   4. Taylor expanded in y.im around 0

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   5. Step-by-step derivation

      1. lower-sin.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lower-*.f64 N/A

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. lower-atan2.f64 64.4%

         \[\leadsto \sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Applied rewrites 64.4%

      \[\leadsto \color{blue}{\sin \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   if -7.5000000000000001e-286 < x.re

   1. Initial program 40.8%

      \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
   2. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

      2. *-commutative N/A

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

      3. lower-*.f64 40.8%

         \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. Applied rewrites 80.8%

      \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
   4. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-184-logsqrtz0z0z1z1z2 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. *-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. lift-*.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. +-commutative N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-+.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      8. lift-sqrt.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      9. lift-log.f64 N/A

         \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      10. *-commutative N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      11. lift-*.f64 N/A

          \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      12. +-commutative N/A

          \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      13. sum-to-mult N/A

          \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      14. lift-*.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      15. *-commutative N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      16. lift-log.f64 N/A

          \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. Applied rewrites 72.9%

      \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. Taylor expanded in y.re around 0

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   7. Step-by-step derivation

   8. Applied rewrites 70.8%

      \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \sin \color{blue}{\left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      2. lift-184-logsqrtz0z0z1z1z2 N/A

         \[\leadsto \sin \left(1 \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      3. associate-*r* N/A

         \[\leadsto \sin \color{blue}{\left(\left(1 \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right) \cdot y.im\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      4. lower-*.f64 N/A

         \[\leadsto \sin \color{blue}{\left(\left(1 \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right) \cdot y.im\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      5. *-commutative N/A

         \[\leadsto \sin \left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot 1\right)} \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      6. lower-184-logsqrtz0z0z1z1z2 70.7%

         \[\leadsto \sin \left(\color{blue}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right)} \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

      7. lift-exp.f64 N/A

         \[\leadsto \sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot \color{blue}{e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

   10. Applied rewrites 70.7%

       \[\leadsto \color{blue}{\sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 70.7% accurate, 1.9× speedup

Math

\[\sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (*
 (sin (* (184-logsqrtz0z0z1z1z2 x.re x.im 1) y.im))
 (exp
  (-
   (184-logsqrtz0z0z1z1z2 x.re x.im y.re)
   (* y.im (atan2 x.im x.re))))))

Derivation

1. Initial program 40.8%

   \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
2. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

   2. *-commutative N/A

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. lower-*.f64 40.8%

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

3. Applied rewrites 80.8%

   \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
4. Step-by-step derivation

   1. lift-+.f64 N/A

      \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   2. lift-184-logsqrtz0z0z1z1z2 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   3. *-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   4. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. +-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   7. lift-+.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   8. lift-sqrt.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   9. lift-log.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   10. *-commutative N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   11. lift-*.f64 N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   12. +-commutative N/A

       \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   13. sum-to-mult N/A

       \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   14. lift-*.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   15. *-commutative N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   16. lift-log.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

5. Applied rewrites 72.9%

   \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

6. Taylor expanded in y.re around 0

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
7. Step-by-step derivation

8. Applied rewrites 70.8%

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
9. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \sin \color{blue}{\left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   2. lift-184-logsqrtz0z0z1z1z2 N/A

      \[\leadsto \sin \left(1 \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   3. associate-*r* N/A

      \[\leadsto \sin \color{blue}{\left(\left(1 \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right) \cdot y.im\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   4. lower-*.f64 N/A

      \[\leadsto \sin \color{blue}{\left(\left(1 \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right) \cdot y.im\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. *-commutative N/A

      \[\leadsto \sin \left(\color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot 1\right)} \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. lower-184-logsqrtz0z0z1z1z2 70.7%

      \[\leadsto \sin \left(\color{blue}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right)} \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   7. lift-exp.f64 N/A

      \[\leadsto \sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot \color{blue}{e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]

10. Applied rewrites 70.7%

    \[\leadsto \color{blue}{\sin \left(\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, 1\right) \cdot y.im\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
11. Add Preprocessing

Alternative 8: 70.0% accurate, 1.9× speedup

Math

\[\sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (*
 (sin (* 1 (184-logsqrtz0z0z1z1z2 x.re x.im y.im)))
 (exp
  (-
   (184-logsqrtz0z0z1z1z2 x.im x.re y.re)
   (* y.im (atan2 x.im x.re))))))

Derivation

1. Initial program 40.8%

   \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
2. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

   2. *-commutative N/A

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. lower-*.f64 40.8%

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

3. Applied rewrites 80.8%

   \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
4. Step-by-step derivation

   1. lift-+.f64 N/A

      \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   2. lift-184-logsqrtz0z0z1z1z2 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   3. *-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   4. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. +-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   7. lift-+.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   8. lift-sqrt.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   9. lift-log.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   10. *-commutative N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   11. lift-*.f64 N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   12. +-commutative N/A

       \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   13. sum-to-mult N/A

       \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   14. lift-*.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   15. *-commutative N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   16. lift-log.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

5. Applied rewrites 72.9%

   \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

6. Taylor expanded in y.re around 0

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
7. Step-by-step derivation

8. Applied rewrites 70.8%

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
9. Add Preprocessing

Alternative 9: 43.6% accurate, 2.0× speedup

Math

\[\sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

FPCore

(FPCore (x.re x.im y.re y.im)
  :precision binary64
  (*
 (sin (* 1 (184-logsqrtz0z0z1z1z2 x.re x.im y.im)))
 (exp (- (* y.im (atan2 x.im x.re))))))

Derivation

1. Initial program 40.8%

   \[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \]
2. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \]

   2. *-commutative N/A

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

   3. lower-*.f64 40.8%

      \[\leadsto \color{blue}{\sin \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right) \cdot e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im}} \]

3. Applied rewrites 80.8%

   \[\leadsto \color{blue}{\sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
4. Step-by-step derivation

   1. lift-+.f64 N/A

      \[\leadsto \sin \color{blue}{\left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   2. lift-184-logsqrtz0z0z1z1z2 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   3. *-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{y.im \cdot \log \left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   4. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.im \cdot x.im} + x.re \cdot x.re}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   5. lift-*.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{x.im \cdot x.im + \color{blue}{x.re \cdot x.re}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   6. +-commutative N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   7. lift-+.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \left(\sqrt{\color{blue}{x.re \cdot x.re + x.im \cdot x.im}}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   8. lift-sqrt.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \log \color{blue}{\left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   9. lift-log.f64 N/A

      \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   10. *-commutative N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   11. lift-*.f64 N/A

       \[\leadsto \sin \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re + \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   12. +-commutative N/A

       \[\leadsto \sin \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   13. sum-to-mult N/A

       \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   14. lift-*.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   15. *-commutative N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \color{blue}{\left(y.im \cdot \log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)\right)}\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

   16. lift-log.f64 N/A

       \[\leadsto \sin \left(\left(1 + \frac{\tan^{-1}_* \frac{x.im}{x.re} \cdot y.re}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im}\right) \cdot \left(y.im \cdot \color{blue}{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right)}\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

5. Applied rewrites 72.9%

   \[\leadsto \sin \color{blue}{\left(\left(1 + \frac{y.re \cdot \tan^{-1}_* \frac{x.im}{x.re}}{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)}\right) \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right)} \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

6. Taylor expanded in y.re around 0

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]
7. Step-by-step derivation

8. Applied rewrites 70.8%

   \[\leadsto \sin \left(\color{blue}{1} \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{184\_logsqrtz0z0z1z1z2}\left(x.im, x.re, y.re\right) - y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

9. Taylor expanded in y.re around 0

   \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot \color{blue}{e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}} \]
10. Step-by-step derivation

    1. lower-exp.f64 N/A

       \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{\mathsf{neg}\left(y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)} \]

    2. lower-neg.f64 N/A

       \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

    3. lower-*.f64 N/A

       \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

    4. lower-atan2.f64 43.6%

       \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}} \]

11. Applied rewrites 43.6%

    \[\leadsto \sin \left(1 \cdot \mathsf{184\_logsqrtz0z0z1z1z2}\left(x.re, x.im, y.im\right)\right) \cdot \color{blue}{e^{-y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}} \]
12. Add Preprocessing

Reproduce

herbie shell --seed 2025271 -o generate:evaluate
(FPCore (x.re x.im y.re y.im)
  :name "powComplex, imaginary part"
  :precision binary64
  (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))))