tan-example (used to crash)

Percentage Accurate: 79.7% → 99.7%

Time: 9.2s

Alternatives: 10

Speedup: 1.0×

Specification

\[\left(\left(\left(x = 0 \lor 0.5884142 \leq x \land x \leq 505.5909\right) \land \left(-1.796658 \cdot 10^{+308} \leq y \land y \leq -9.425585 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \leq y \land y \leq 1.751224 \cdot 10^{+308}\right)\right) \land \left(-1.776707 \cdot 10^{+308} \leq z \land z \leq -8.599796 \cdot 10^{-310} \lor 3.293145 \cdot 10^{-311} \leq z \land z \leq 1.725154 \cdot 10^{+308}\right)\right) \land \left(-1.796658 \cdot 10^{+308} \leq a \land a \leq -9.425585 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \leq a \land a \leq 1.751224 \cdot 10^{+308}\right)\]

Math

\[x + \left(\tan \left(y + z\right) - \tan a\right) \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (+ x (- (tan (+ y z)) (tan a))))

C

double code(double x, double y, double z, double a) {
	return x + (tan((y + z)) - tan(a));
}

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, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    code = x + (tan((y + z)) - tan(a))
end function

Java

public static double code(double x, double y, double z, double a) {
	return x + (Math.tan((y + z)) - Math.tan(a));
}

Python

def code(x, y, z, a):
	return x + (math.tan((y + z)) - math.tan(a))

Julia

function code(x, y, z, a)
	return Float64(x + Float64(tan(Float64(y + z)) - tan(a)))
end

MATLAB

function tmp = code(x, y, z, a)
	tmp = x + (tan((y + z)) - tan(a));
end

Wolfram

code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Initial Program: 79.7% accurate, 1.0× speedup

Math

\[x + \left(\tan \left(y + z\right) - \tan a\right) \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (+ x (- (tan (+ y z)) (tan a))))

C

double code(double x, double y, double z, double a) {
	return x + (tan((y + z)) - tan(a));
}

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, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    code = x + (tan((y + z)) - tan(a))
end function

Java

public static double code(double x, double y, double z, double a) {
	return x + (Math.tan((y + z)) - Math.tan(a));
}

Python

def code(x, y, z, a):
	return x + (math.tan((y + z)) - math.tan(a))

Julia

function code(x, y, z, a)
	return Float64(x + Float64(tan(Float64(y + z)) - tan(a)))
end

MATLAB

function tmp = code(x, y, z, a)
	tmp = x + (tan((y + z)) - tan(a));
end

Wolfram

code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Alternative 1: 99.7% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := \tan \left(\mathsf{max}\left(y, z\right)\right)\\ t_1 := \sin \left(\mathsf{min}\left(y, z\right)\right)\\ t_2 := \cos \left(\mathsf{min}\left(y, z\right)\right)\\ x + \left(\left(\frac{t\_1}{t\_2 \cdot \left(1 - \frac{t\_1 \cdot \sin \left(\mathsf{max}\left(y, z\right)\right)}{t\_2 \cdot \cos \left(\mathsf{max}\left(y, z\right)\right)}\right)} + \frac{t\_0}{1 - t\_0 \cdot \tan \left(\mathsf{min}\left(y, z\right)\right)}\right) - \tan a\right) \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0 (tan (fmax y z)))
       (t_1 (sin (fmin y z)))
       (t_2 (cos (fmin y z))))
  (+
   x
   (-
    (+
     (/
      t_1
      (*
       t_2
       (- 1.0 (/ (* t_1 (sin (fmax y z))) (* t_2 (cos (fmax y z)))))))
     (/ t_0 (- 1.0 (* t_0 (tan (fmin y z))))))
    (tan a)))))

C

double code(double x, double y, double z, double a) {
	double t_0 = tan(fmax(y, z));
	double t_1 = sin(fmin(y, z));
	double t_2 = cos(fmin(y, z));
	return x + (((t_1 / (t_2 * (1.0 - ((t_1 * sin(fmax(y, z))) / (t_2 * cos(fmax(y, z))))))) + (t_0 / (1.0 - (t_0 * tan(fmin(y, z)))))) - tan(a));
}

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, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: t_2
    t_0 = tan(fmax(y, z))
    t_1 = sin(fmin(y, z))
    t_2 = cos(fmin(y, z))
    code = x + (((t_1 / (t_2 * (1.0d0 - ((t_1 * sin(fmax(y, z))) / (t_2 * cos(fmax(y, z))))))) + (t_0 / (1.0d0 - (t_0 * tan(fmin(y, z)))))) - tan(a))
end function

Java

public static double code(double x, double y, double z, double a) {
	double t_0 = Math.tan(fmax(y, z));
	double t_1 = Math.sin(fmin(y, z));
	double t_2 = Math.cos(fmin(y, z));
	return x + (((t_1 / (t_2 * (1.0 - ((t_1 * Math.sin(fmax(y, z))) / (t_2 * Math.cos(fmax(y, z))))))) + (t_0 / (1.0 - (t_0 * Math.tan(fmin(y, z)))))) - Math.tan(a));
}

Python

def code(x, y, z, a):
	t_0 = math.tan(fmax(y, z))
	t_1 = math.sin(fmin(y, z))
	t_2 = math.cos(fmin(y, z))
	return x + (((t_1 / (t_2 * (1.0 - ((t_1 * math.sin(fmax(y, z))) / (t_2 * math.cos(fmax(y, z))))))) + (t_0 / (1.0 - (t_0 * math.tan(fmin(y, z)))))) - math.tan(a))

Julia

function code(x, y, z, a)
	t_0 = tan(fmax(y, z))
	t_1 = sin(fmin(y, z))
	t_2 = cos(fmin(y, z))
	return Float64(x + Float64(Float64(Float64(t_1 / Float64(t_2 * Float64(1.0 - Float64(Float64(t_1 * sin(fmax(y, z))) / Float64(t_2 * cos(fmax(y, z))))))) + Float64(t_0 / Float64(1.0 - Float64(t_0 * tan(fmin(y, z)))))) - tan(a)))
end

MATLAB

function tmp = code(x, y, z, a)
	t_0 = tan(max(y, z));
	t_1 = sin(min(y, z));
	t_2 = cos(min(y, z));
	tmp = x + (((t_1 / (t_2 * (1.0 - ((t_1 * sin(max(y, z))) / (t_2 * cos(max(y, z))))))) + (t_0 / (1.0 - (t_0 * tan(min(y, z)))))) - tan(a));
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[Tan[N[Max[y, z], $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[Sin[N[Min[y, z], $MachinePrecision]], $MachinePrecision]}, Block[{t$95$2 = N[Cos[N[Min[y, z], $MachinePrecision]], $MachinePrecision]}, N[(x + N[(N[(N[(t$95$1 / N[(t$95$2 * N[(1.0 - N[(N[(t$95$1 * N[Sin[N[Max[y, z], $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(t$95$2 * N[Cos[N[Max[y, z], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t$95$0 / N[(1.0 - N[(t$95$0 * N[Tan[N[Min[y, z], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]

Derivation

1. Initial program 79.7%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
2. Step-by-step derivation

   1. lift-tan.f64 N/A

      \[\leadsto x + \left(\color{blue}{\tan \left(y + z\right)} - \tan a\right) \]

   2. tan-quot N/A

      \[\leadsto x + \left(\color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} - \tan a\right) \]

   3. lift-+.f64 N/A

      \[\leadsto x + \left(\frac{\sin \color{blue}{\left(y + z\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

   4. +-commutative N/A

      \[\leadsto x + \left(\frac{\sin \color{blue}{\left(z + y\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

   5. sin-sum N/A

      \[\leadsto x + \left(\frac{\color{blue}{\sin z \cdot \cos y + \cos z \cdot \sin y}}{\cos \left(y + z\right)} - \tan a\right) \]

   6. div-add N/A

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

   7. *-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\color{blue}{\sin y \cdot \cos z}}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   8. lower-+.f64 N/A

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

   9. lower-/.f64 N/A

      \[\leadsto x + \left(\left(\color{blue}{\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   10. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z \cdot \cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   11. lower-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z} \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   12. lower-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \color{blue}{\cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   13. lower-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   14. lift-+.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   15. +-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   16. lower-+.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   17. lower-/.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \color{blue}{\frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}}\right) - \tan a\right) \]

3. Applied rewrites 80.2%

   \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right)} - \tan a\right) \]
4. Step-by-step derivation

   1. lift-cos.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(z + y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   2. lift-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   3. +-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   4. cos-sum N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos y \cdot \cos z - \sin y \cdot \sin z}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   5. sub-to-mult N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   6. lower-unsound-*.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   7. lower-unsound--.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   8. lower-unsound-/.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \color{blue}{\frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   9. lift-sin.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\color{blue}{\sin y} \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   10. lift-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \color{blue}{\sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   11. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\color{blue}{\sin y \cdot \sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   12. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y} \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   13. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \color{blue}{\cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   14. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   15. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   16. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\color{blue}{\cos y} \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   17. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos y \cdot \color{blue}{\cos z}\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   18. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   19. lower-*.f64 81.0%

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

5. Applied rewrites 81.0%

   \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]
6. Step-by-step derivation

   1. lift-cos.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\cos \left(z + y\right)}}\right) - \tan a\right) \]

   2. lift-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\cos \color{blue}{\left(z + y\right)}}\right) - \tan a\right) \]

   3. +-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\cos \color{blue}{\left(y + z\right)}}\right) - \tan a\right) \]

   4. cos-sum N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\cos y \cdot \cos z - \sin y \cdot \sin z}}\right) - \tan a\right) \]

   5. sub-to-mult N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}}\right) - \tan a\right) \]

   6. lower-unsound-*.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}}\right) - \tan a\right) \]

   7. lower-unsound--.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   8. lower-unsound-/.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \color{blue}{\frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   9. lift-sin.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\color{blue}{\sin y} \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   10. lift-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \color{blue}{\sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   11. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\color{blue}{\sin y \cdot \sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   12. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y} \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   13. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \color{blue}{\cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   14. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   15. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   16. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\color{blue}{\cos y} \cdot \cos z\right)}\right) - \tan a\right) \]

   17. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos y \cdot \color{blue}{\cos z}\right)}\right) - \tan a\right) \]

   18. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

   19. lower-*.f64 99.7%

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

7. Applied rewrites 99.7%

   \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

8. Taylor expanded in y around inf

   \[\leadsto x + \left(\color{blue}{\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}\right)} - \tan a\right) \]
9. Step-by-step derivation

   1. lower-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \color{blue}{\frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}}\right) - \tan a\right) \]

10. Applied rewrites 99.7%

    \[\leadsto x + \left(\color{blue}{\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}\right)} - \tan a\right) \]
11. Step-by-step derivation

    1. lift-/.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\color{blue}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}}\right) - \tan a\right) \]

    2. lift-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\cos z \cdot \color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}}\right) - \tan a\right) \]

    3. associate-/r* N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\frac{\sin z}{\cos z}}{\color{blue}{1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}}\right) - \tan a\right) \]

    4. lower-/.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\frac{\sin z}{\cos z}}{\color{blue}{1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}}\right) - \tan a\right) \]

    5. lift-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\frac{\sin z}{\cos z}}{1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) - \tan a\right) \]

    6. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\frac{\sin z}{\cos z}}{1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) - \tan a\right) \]

    7. quot-tan N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{\color{blue}{1} - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) - \tan a\right) \]

    8. lower-tan.f64 99.7%

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{\color{blue}{1} - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) - \tan a\right) \]

    9. lift-/.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y \cdot \cos z}}}\right) - \tan a\right) \]

    10. lift-*.f64 N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y} \cdot \cos z}}\right) - \tan a\right) \]

    11. *-commutative N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z \cdot \sin y}{\color{blue}{\cos y} \cdot \cos z}}\right) - \tan a\right) \]

    12. lift-*.f64 N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z \cdot \sin y}{\cos y \cdot \color{blue}{\cos z}}}\right) - \tan a\right) \]

    13. *-commutative N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z \cdot \sin y}{\cos z \cdot \color{blue}{\cos y}}}\right) - \tan a\right) \]

    14. times-frac N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z}{\cos z} \cdot \color{blue}{\frac{\sin y}{\cos y}}}\right) - \tan a\right) \]

    15. lift-/.f64 N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z}{\cos z} \cdot \frac{\sin y}{\color{blue}{\cos y}}}\right) - \tan a\right) \]

    16. lower-*.f64 N/A

        \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{1 - \frac{\sin z}{\cos z} \cdot \color{blue}{\frac{\sin y}{\cos y}}}\right) - \tan a\right) \]

12. Applied rewrites 99.7%

    \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\tan z}{\color{blue}{1 - \tan z \cdot \tan y}}\right) - \tan a\right) \]
13. Add Preprocessing

Alternative 2: 99.7% accurate, 0.4× speedup

Math

\[x - \left(\tan a - \frac{\tan z + \tan y}{1 - \tan z \cdot \tan y}\right) \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (- x (- (tan a) (/ (+ (tan z) (tan y)) (- 1.0 (* (tan z) (tan y)))))))

C

double code(double x, double y, double z, double a) {
	return x - (tan(a) - ((tan(z) + tan(y)) / (1.0 - (tan(z) * tan(y)))));
}

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, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    code = x - (tan(a) - ((tan(z) + tan(y)) / (1.0d0 - (tan(z) * tan(y)))))
end function

Java

public static double code(double x, double y, double z, double a) {
	return x - (Math.tan(a) - ((Math.tan(z) + Math.tan(y)) / (1.0 - (Math.tan(z) * Math.tan(y)))));
}

Python

def code(x, y, z, a):
	return x - (math.tan(a) - ((math.tan(z) + math.tan(y)) / (1.0 - (math.tan(z) * math.tan(y)))))

Julia

function code(x, y, z, a)
	return Float64(x - Float64(tan(a) - Float64(Float64(tan(z) + tan(y)) / Float64(1.0 - Float64(tan(z) * tan(y))))))
end

MATLAB

function tmp = code(x, y, z, a)
	tmp = x - (tan(a) - ((tan(z) + tan(y)) / (1.0 - (tan(z) * tan(y)))));
end

Wolfram

code[x_, y_, z_, a_] := N[(x - N[(N[Tan[a], $MachinePrecision] - N[(N[(N[Tan[z], $MachinePrecision] + N[Tan[y], $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[Tan[z], $MachinePrecision] * N[Tan[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 79.7%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
2. Step-by-step derivation

   1. lift-tan.f64 N/A

      \[\leadsto x + \left(\color{blue}{\tan \left(y + z\right)} - \tan a\right) \]

   2. tan-quot N/A

      \[\leadsto x + \left(\color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} - \tan a\right) \]

   3. lift-+.f64 N/A

      \[\leadsto x + \left(\frac{\sin \color{blue}{\left(y + z\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

   4. +-commutative N/A

      \[\leadsto x + \left(\frac{\sin \color{blue}{\left(z + y\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

   5. sin-sum N/A

      \[\leadsto x + \left(\frac{\color{blue}{\sin z \cdot \cos y + \cos z \cdot \sin y}}{\cos \left(y + z\right)} - \tan a\right) \]

   6. div-add N/A

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

   7. *-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\color{blue}{\sin y \cdot \cos z}}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   8. lower-+.f64 N/A

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

   9. lower-/.f64 N/A

      \[\leadsto x + \left(\left(\color{blue}{\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   10. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z \cdot \cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   11. lower-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z} \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   12. lower-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \color{blue}{\cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   13. lower-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   14. lift-+.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   15. +-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   16. lower-+.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

   17. lower-/.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \color{blue}{\frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}}\right) - \tan a\right) \]

3. Applied rewrites 80.2%

   \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right)} - \tan a\right) \]
4. Step-by-step derivation

   1. lift-cos.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(z + y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   2. lift-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   3. +-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   4. cos-sum N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos y \cdot \cos z - \sin y \cdot \sin z}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   5. sub-to-mult N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   6. lower-unsound-*.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   7. lower-unsound--.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   8. lower-unsound-/.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \color{blue}{\frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   9. lift-sin.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\color{blue}{\sin y} \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   10. lift-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \color{blue}{\sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   11. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\color{blue}{\sin y \cdot \sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   12. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y} \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   13. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \color{blue}{\cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   14. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   15. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   16. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\color{blue}{\cos y} \cdot \cos z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   17. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos y \cdot \color{blue}{\cos z}\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   18. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

   19. lower-*.f64 81.0%

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]

5. Applied rewrites 81.0%

   \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)}} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right) - \tan a\right) \]
6. Step-by-step derivation

   1. lift-cos.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\cos \left(z + y\right)}}\right) - \tan a\right) \]

   2. lift-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\cos \color{blue}{\left(z + y\right)}}\right) - \tan a\right) \]

   3. +-commutative N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\cos \color{blue}{\left(y + z\right)}}\right) - \tan a\right) \]

   4. cos-sum N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\cos y \cdot \cos z - \sin y \cdot \sin z}}\right) - \tan a\right) \]

   5. sub-to-mult N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}}\right) - \tan a\right) \]

   6. lower-unsound-*.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}}\right) - \tan a\right) \]

   7. lower-unsound--.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   8. lower-unsound-/.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \color{blue}{\frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   9. lift-sin.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\color{blue}{\sin y} \cdot \sin z}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   10. lift-sin.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \color{blue}{\sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   11. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\color{blue}{\sin y \cdot \sin z}}{\cos y \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   12. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos y} \cdot \cos z}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   13. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \color{blue}{\cos z}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   14. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   15. lower-*.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\color{blue}{\cos z \cdot \cos y}}\right) \cdot \left(\cos y \cdot \cos z\right)}\right) - \tan a\right) \]

   16. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\color{blue}{\cos y} \cdot \cos z\right)}\right) - \tan a\right) \]

   17. lift-cos.f64 N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos y \cdot \color{blue}{\cos z}\right)}\right) - \tan a\right) \]

   18. *-commutative N/A

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

   19. lower-*.f64 99.7%

       \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \color{blue}{\left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

7. Applied rewrites 99.7%

   \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)} + \frac{\cos z \cdot \sin y}{\color{blue}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \left(\cos z \cdot \cos y\right)}}\right) - \tan a\right) \]

8. Taylor expanded in y around inf

   \[\leadsto x + \left(\color{blue}{\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}\right)} - \tan a\right) \]
9. Step-by-step derivation

   1. lower-+.f64 N/A

      \[\leadsto x + \left(\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \color{blue}{\frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}}\right) - \tan a\right) \]

10. Applied rewrites 99.7%

    \[\leadsto x + \left(\color{blue}{\left(\frac{\sin y}{\cos y \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)} + \frac{\sin z}{\cos z \cdot \left(1 - \frac{\sin y \cdot \sin z}{\cos y \cdot \cos z}\right)}\right)} - \tan a\right) \]

12. Applied rewrites 99.7%

    \[\leadsto \color{blue}{x - \left(\tan a - \frac{\tan z + \tan y}{1 - \tan z \cdot \tan y}\right)} \]
13. Add Preprocessing

Alternative 3: 79.6% accurate, 0.9× speedup

Math

\[\begin{array}{l} \mathbf{if}\;\mathsf{min}\left(y, z\right) + \mathsf{max}\left(y, z\right) \leq -5 \cdot 10^{-13}:\\ \;\;\;\;x - \left(\tan a - \tan \left(\mathsf{min}\left(y, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(\tan \left(\mathsf{max}\left(y, z\right)\right) - \tan a\right)\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (if (<= (+ (fmin y z) (fmax y z)) -5e-13)
  (- x (- (tan a) (tan (fmin y z))))
  (+ x (- (tan (fmax y z)) (tan a)))))

C

double code(double x, double y, double z, double a) {
	double tmp;
	if ((fmin(y, z) + fmax(y, z)) <= -5e-13) {
		tmp = x - (tan(a) - tan(fmin(y, z)));
	} else {
		tmp = x + (tan(fmax(y, z)) - tan(a));
	}
	return tmp;
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

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

real(8) function code(x, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    real(8) :: tmp
    if ((fmin(y, z) + fmax(y, z)) <= (-5d-13)) then
        tmp = x - (tan(a) - tan(fmin(y, z)))
    else
        tmp = x + (tan(fmax(y, z)) - tan(a))
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double a) {
	double tmp;
	if ((fmin(y, z) + fmax(y, z)) <= -5e-13) {
		tmp = x - (Math.tan(a) - Math.tan(fmin(y, z)));
	} else {
		tmp = x + (Math.tan(fmax(y, z)) - Math.tan(a));
	}
	return tmp;
}

Python

def code(x, y, z, a):
	tmp = 0
	if (fmin(y, z) + fmax(y, z)) <= -5e-13:
		tmp = x - (math.tan(a) - math.tan(fmin(y, z)))
	else:
		tmp = x + (math.tan(fmax(y, z)) - math.tan(a))
	return tmp

Julia

function code(x, y, z, a)
	tmp = 0.0
	if (Float64(fmin(y, z) + fmax(y, z)) <= -5e-13)
		tmp = Float64(x - Float64(tan(a) - tan(fmin(y, z))));
	else
		tmp = Float64(x + Float64(tan(fmax(y, z)) - tan(a)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, a)
	tmp = 0.0;
	if ((min(y, z) + max(y, z)) <= -5e-13)
		tmp = x - (tan(a) - tan(min(y, z)));
	else
		tmp = x + (tan(max(y, z)) - tan(a));
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, a_] := If[LessEqual[N[(N[Min[y, z], $MachinePrecision] + N[Max[y, z], $MachinePrecision]), $MachinePrecision], -5e-13], N[(x - N[(N[Tan[a], $MachinePrecision] - N[Tan[N[Min[y, z], $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[(N[Tan[N[Max[y, z], $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (+.f64 y z) < -4.9999999999999999e-13

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in z around 0

      \[\leadsto x + \left(\color{blue}{\frac{\sin y}{\cos y}} - \tan a\right) \]
   3. Step-by-step derivation

      1. lower-/.f64 N/A

         \[\leadsto x + \left(\frac{\sin y}{\color{blue}{\cos y}} - \tan a\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto x + \left(\frac{\sin y}{\cos \color{blue}{y}} - \tan a\right) \]

      3. lower-cos.f64 59.9%

         \[\leadsto x + \left(\frac{\sin y}{\cos y} - \tan a\right) \]

   4. Applied rewrites 59.9%

      \[\leadsto x + \left(\color{blue}{\frac{\sin y}{\cos y}} - \tan a\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto \color{blue}{x + \left(\frac{\sin y}{\cos y} - \tan a\right)} \]

      2. add-flip N/A

         \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\left(\frac{\sin y}{\cos y} - \tan a\right)\right)\right)} \]

      3. lower--.f64 N/A

         \[\leadsto \color{blue}{x - \left(\mathsf{neg}\left(\left(\frac{\sin y}{\cos y} - \tan a\right)\right)\right)} \]

      4. lift--.f64 N/A

         \[\leadsto x - \left(\mathsf{neg}\left(\color{blue}{\left(\frac{\sin y}{\cos y} - \tan a\right)}\right)\right) \]

      5. sub-negate-rev N/A

         \[\leadsto x - \color{blue}{\left(\tan a - \frac{\sin y}{\cos y}\right)} \]

      6. lower--.f64 59.9%

         \[\leadsto x - \color{blue}{\left(\tan a - \frac{\sin y}{\cos y}\right)} \]

      7. lift-/.f64 N/A

         \[\leadsto x - \left(\tan a - \frac{\sin y}{\color{blue}{\cos y}}\right) \]

      8. lift-sin.f64 N/A

         \[\leadsto x - \left(\tan a - \frac{\sin y}{\cos \color{blue}{y}}\right) \]

      9. lift-cos.f64 N/A

         \[\leadsto x - \left(\tan a - \frac{\sin y}{\cos y}\right) \]

      10. quot-tan N/A

          \[\leadsto x - \left(\tan a - \tan y\right) \]

      11. lower-tan.f64 59.9%

          \[\leadsto x - \left(\tan a - \tan y\right) \]

   6. Applied rewrites 59.9%

      \[\leadsto \color{blue}{x - \left(\tan a - \tan y\right)} \]

   if -4.9999999999999999e-13 < (+.f64 y z)

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in y around 0

      \[\leadsto x + \left(\tan \color{blue}{z} - \tan a\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 60.6%

      \[\leadsto x + \left(\tan \color{blue}{z} - \tan a\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 69.7% accurate, 0.8× speedup

Math

\[\begin{array}{l} t_0 := \mathsf{min}\left(y, z\right) + \mathsf{max}\left(y, z\right)\\ \mathbf{if}\;\mathsf{min}\left(y, z\right) \leq -116:\\ \;\;\;\;x + \frac{\sin t\_0}{\cos t\_0}\\ \mathbf{else}:\\ \;\;\;\;x + \left(\tan \left(\mathsf{max}\left(y, z\right)\right) - \tan a\right)\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0 (+ (fmin y z) (fmax y z))))
  (if (<= (fmin y z) -116.0)
    (+ x (/ (sin t_0) (cos t_0)))
    (+ x (- (tan (fmax y z)) (tan a))))))

C

double code(double x, double y, double z, double a) {
	double t_0 = fmin(y, z) + fmax(y, z);
	double tmp;
	if (fmin(y, z) <= -116.0) {
		tmp = x + (sin(t_0) / cos(t_0));
	} else {
		tmp = x + (tan(fmax(y, z)) - tan(a));
	}
	return tmp;
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

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

real(8) function code(x, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    real(8) :: t_0
    real(8) :: tmp
    t_0 = fmin(y, z) + fmax(y, z)
    if (fmin(y, z) <= (-116.0d0)) then
        tmp = x + (sin(t_0) / cos(t_0))
    else
        tmp = x + (tan(fmax(y, z)) - tan(a))
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double a) {
	double t_0 = fmin(y, z) + fmax(y, z);
	double tmp;
	if (fmin(y, z) <= -116.0) {
		tmp = x + (Math.sin(t_0) / Math.cos(t_0));
	} else {
		tmp = x + (Math.tan(fmax(y, z)) - Math.tan(a));
	}
	return tmp;
}

Python

def code(x, y, z, a):
	t_0 = fmin(y, z) + fmax(y, z)
	tmp = 0
	if fmin(y, z) <= -116.0:
		tmp = x + (math.sin(t_0) / math.cos(t_0))
	else:
		tmp = x + (math.tan(fmax(y, z)) - math.tan(a))
	return tmp

Julia

function code(x, y, z, a)
	t_0 = Float64(fmin(y, z) + fmax(y, z))
	tmp = 0.0
	if (fmin(y, z) <= -116.0)
		tmp = Float64(x + Float64(sin(t_0) / cos(t_0)));
	else
		tmp = Float64(x + Float64(tan(fmax(y, z)) - tan(a)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, a)
	t_0 = min(y, z) + max(y, z);
	tmp = 0.0;
	if (min(y, z) <= -116.0)
		tmp = x + (sin(t_0) / cos(t_0));
	else
		tmp = x + (tan(max(y, z)) - tan(a));
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[(N[Min[y, z], $MachinePrecision] + N[Max[y, z], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[Min[y, z], $MachinePrecision], -116.0], N[(x + N[(N[Sin[t$95$0], $MachinePrecision] / N[Cos[t$95$0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[(N[Tan[N[Max[y, z], $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if y < -116

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in a around 0

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

      4. lower-pow.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

   4. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

      3. lift-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      4. lift-pow.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      5. unpow2 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

      6. associate-*r* N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

      8. lower-*.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   6. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 31.4%

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   10. Taylor expanded in a around 0

       \[\leadsto \color{blue}{x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]
   11. Step-by-step derivation

       1. lower-+.f64 N/A

          \[\leadsto x + \color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]

       2. lower-/.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\color{blue}{\cos \left(y + z\right)}} \]

       3. lower-sin.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \color{blue}{\left(y + z\right)}} \]

       4. lower-+.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(\color{blue}{y} + z\right)} \]

       5. lower-cos.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)} \]

       6. lower-+.f64 50.8%

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)} \]

   12. Applied rewrites 50.8%

       \[\leadsto \color{blue}{x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]

   if -116 < y

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in y around 0

      \[\leadsto x + \left(\tan \color{blue}{z} - \tan a\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 60.6%

      \[\leadsto x + \left(\tan \color{blue}{z} - \tan a\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 59.8% accurate, 0.4× speedup

Math

\[\begin{array}{l} t_0 := \mathsf{min}\left(y, z\right) + \mathsf{max}\left(y, z\right)\\ t_1 := \tan t\_0\\ t_2 := x + \frac{\sin t\_0}{\cos t\_0}\\ \mathbf{if}\;t\_1 \leq -0.01:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 4 \cdot 10^{-13}:\\ \;\;\;\;x + \left(\left(\mathsf{max}\left(y, z\right) + \mathsf{min}\left(y, z\right) \cdot \left(1 + \mathsf{min}\left(y, z\right) \cdot \left(\mathsf{max}\left(y, z\right) + 0.3333333333333333 \cdot \mathsf{min}\left(y, z\right)\right)\right)\right) - \tan a\right)\\ \mathbf{else}:\\ \;\;\;\;t\_2\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0 (+ (fmin y z) (fmax y z)))
       (t_1 (tan t_0))
       (t_2 (+ x (/ (sin t_0) (cos t_0)))))
  (if (<= t_1 -0.01)
    t_2
    (if (<= t_1 4e-13)
      (+
       x
       (-
        (+
         (fmax y z)
         (*
          (fmin y z)
          (+
           1.0
           (*
            (fmin y z)
            (+ (fmax y z) (* 0.3333333333333333 (fmin y z)))))))
        (tan a)))
      t_2))))

C

double code(double x, double y, double z, double a) {
	double t_0 = fmin(y, z) + fmax(y, z);
	double t_1 = tan(t_0);
	double t_2 = x + (sin(t_0) / cos(t_0));
	double tmp;
	if (t_1 <= -0.01) {
		tmp = t_2;
	} else if (t_1 <= 4e-13) {
		tmp = x + ((fmax(y, z) + (fmin(y, z) * (1.0 + (fmin(y, z) * (fmax(y, z) + (0.3333333333333333 * fmin(y, z))))))) - tan(a));
	} else {
		tmp = t_2;
	}
	return tmp;
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

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

real(8) function code(x, y, z, a)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: a
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: tmp
    t_0 = fmin(y, z) + fmax(y, z)
    t_1 = tan(t_0)
    t_2 = x + (sin(t_0) / cos(t_0))
    if (t_1 <= (-0.01d0)) then
        tmp = t_2
    else if (t_1 <= 4d-13) then
        tmp = x + ((fmax(y, z) + (fmin(y, z) * (1.0d0 + (fmin(y, z) * (fmax(y, z) + (0.3333333333333333d0 * fmin(y, z))))))) - tan(a))
    else
        tmp = t_2
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double a) {
	double t_0 = fmin(y, z) + fmax(y, z);
	double t_1 = Math.tan(t_0);
	double t_2 = x + (Math.sin(t_0) / Math.cos(t_0));
	double tmp;
	if (t_1 <= -0.01) {
		tmp = t_2;
	} else if (t_1 <= 4e-13) {
		tmp = x + ((fmax(y, z) + (fmin(y, z) * (1.0 + (fmin(y, z) * (fmax(y, z) + (0.3333333333333333 * fmin(y, z))))))) - Math.tan(a));
	} else {
		tmp = t_2;
	}
	return tmp;
}

Python

def code(x, y, z, a):
	t_0 = fmin(y, z) + fmax(y, z)
	t_1 = math.tan(t_0)
	t_2 = x + (math.sin(t_0) / math.cos(t_0))
	tmp = 0
	if t_1 <= -0.01:
		tmp = t_2
	elif t_1 <= 4e-13:
		tmp = x + ((fmax(y, z) + (fmin(y, z) * (1.0 + (fmin(y, z) * (fmax(y, z) + (0.3333333333333333 * fmin(y, z))))))) - math.tan(a))
	else:
		tmp = t_2
	return tmp

Julia

function code(x, y, z, a)
	t_0 = Float64(fmin(y, z) + fmax(y, z))
	t_1 = tan(t_0)
	t_2 = Float64(x + Float64(sin(t_0) / cos(t_0)))
	tmp = 0.0
	if (t_1 <= -0.01)
		tmp = t_2;
	elseif (t_1 <= 4e-13)
		tmp = Float64(x + Float64(Float64(fmax(y, z) + Float64(fmin(y, z) * Float64(1.0 + Float64(fmin(y, z) * Float64(fmax(y, z) + Float64(0.3333333333333333 * fmin(y, z))))))) - tan(a)));
	else
		tmp = t_2;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, a)
	t_0 = min(y, z) + max(y, z);
	t_1 = tan(t_0);
	t_2 = x + (sin(t_0) / cos(t_0));
	tmp = 0.0;
	if (t_1 <= -0.01)
		tmp = t_2;
	elseif (t_1 <= 4e-13)
		tmp = x + ((max(y, z) + (min(y, z) * (1.0 + (min(y, z) * (max(y, z) + (0.3333333333333333 * min(y, z))))))) - tan(a));
	else
		tmp = t_2;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[(N[Min[y, z], $MachinePrecision] + N[Max[y, z], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[Tan[t$95$0], $MachinePrecision]}, Block[{t$95$2 = N[(x + N[(N[Sin[t$95$0], $MachinePrecision] / N[Cos[t$95$0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -0.01], t$95$2, If[LessEqual[t$95$1, 4e-13], N[(x + N[(N[(N[Max[y, z], $MachinePrecision] + N[(N[Min[y, z], $MachinePrecision] * N[(1.0 + N[(N[Min[y, z], $MachinePrecision] * N[(N[Max[y, z], $MachinePrecision] + N[(0.3333333333333333 * N[Min[y, z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$2]]]]]

Derivation

1. Split input into 2 regimes

2. if (tan.f64 (+.f64 y z)) < -0.01 or 4.0000000000000001e-13 < (tan.f64 (+.f64 y z))

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in a around 0

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

      4. lower-pow.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

   4. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

      3. lift-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      4. lift-pow.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      5. unpow2 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

      6. associate-*r* N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

      8. lower-*.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   6. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 31.4%

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   10. Taylor expanded in a around 0

       \[\leadsto \color{blue}{x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]
   11. Step-by-step derivation

       1. lower-+.f64 N/A

          \[\leadsto x + \color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]

       2. lower-/.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\color{blue}{\cos \left(y + z\right)}} \]

       3. lower-sin.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \color{blue}{\left(y + z\right)}} \]

       4. lower-+.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(\color{blue}{y} + z\right)} \]

       5. lower-cos.f64 N/A

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)} \]

       6. lower-+.f64 50.8%

          \[\leadsto x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)} \]

   12. Applied rewrites 50.8%

       \[\leadsto \color{blue}{x + \frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} \]

   if -0.01 < (tan.f64 (+.f64 y z)) < 4.0000000000000001e-13

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. lift-tan.f64 N/A

         \[\leadsto x + \left(\color{blue}{\tan \left(y + z\right)} - \tan a\right) \]

      2. tan-quot N/A

         \[\leadsto x + \left(\color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} - \tan a\right) \]

      3. lift-+.f64 N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(y + z\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      4. +-commutative N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(z + y\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      5. sin-sum N/A

         \[\leadsto x + \left(\frac{\color{blue}{\sin z \cdot \cos y + \cos z \cdot \sin y}}{\cos \left(y + z\right)} - \tan a\right) \]

      6. div-add N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      7. *-commutative N/A

         \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\color{blue}{\sin y \cdot \cos z}}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      8. lower-+.f64 N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\left(\color{blue}{\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      10. lower-*.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z \cdot \cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z} \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      12. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \color{blue}{\cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      13. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      14. lift-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      15. +-commutative N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      16. lower-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      17. lower-/.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \color{blue}{\frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}}\right) - \tan a\right) \]

   3. Applied rewrites 80.2%

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right)} - \tan a\right) \]

   4. Taylor expanded in z around 0

      \[\leadsto x + \left(\color{blue}{\left(z \cdot \left(1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}\right) + \frac{\sin y}{\cos y}\right)} - \tan a\right) \]
   5. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, \color{blue}{1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      2. lower--.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - \color{blue}{-1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \color{blue}{\frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      4. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{\color{blue}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\color{blue}{\cos y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      6. lower-sin.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos \color{blue}{y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      7. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{\color{blue}{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      8. lower-cos.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      10. lower-sin.f64 N/A

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      11. lower-cos.f64 50.6%

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

   6. Applied rewrites 50.6%

      \[\leadsto x + \left(\color{blue}{\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right)} - \tan a\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot \left(z + \frac{1}{3} \cdot y\right)\right)}\right) - \tan a\right) \]
   8. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \color{blue}{\left(1 + y \cdot \left(z + \frac{1}{3} \cdot y\right)\right)}\right) - \tan a\right) \]

      2. lower-*.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + \color{blue}{y \cdot \left(z + \frac{1}{3} \cdot y\right)}\right)\right) - \tan a\right) \]

      3. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \color{blue}{\left(z + \frac{1}{3} \cdot y\right)}\right)\right) - \tan a\right) \]

      4. lower-*.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \left(z + \color{blue}{\frac{1}{3} \cdot y}\right)\right)\right) - \tan a\right) \]

      5. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \left(z + \frac{1}{3} \cdot \color{blue}{y}\right)\right)\right) - \tan a\right) \]

      6. lower-*.f64 26.2%

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \left(z + 0.3333333333333333 \cdot y\right)\right)\right) - \tan a\right) \]

   9. Applied rewrites 26.2%

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot \left(z + 0.3333333333333333 \cdot y\right)\right)}\right) - \tan a\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 55.2% accurate, 1.0× speedup

Math

\[\begin{array}{l} t_0 := x + \left(\mathsf{min}\left(y, z\right) \cdot \left(1 + 0.3333333333333333 \cdot {\left(\mathsf{min}\left(y, z\right)\right)}^{2}\right) - \tan a\right)\\ \mathbf{if}\;a \leq -0.015:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;a \leq 3.05:\\ \;\;\;\;x + \left(\tan \left(\mathsf{min}\left(y, z\right) + \mathsf{max}\left(y, z\right)\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0
        (+
         x
         (-
          (*
           (fmin y z)
           (+ 1.0 (* 0.3333333333333333 (pow (fmin y z) 2.0))))
          (tan a)))))
  (if (<= a -0.015)
    t_0
    (if (<= a 3.05)
      (+
       x
       (-
        (tan (+ (fmin y z) (fmax y z)))
        (* a (fma (* 0.3333333333333333 a) a 1.0))))
      t_0))))

C

double code(double x, double y, double z, double a) {
	double t_0 = x + ((fmin(y, z) * (1.0 + (0.3333333333333333 * pow(fmin(y, z), 2.0)))) - tan(a));
	double tmp;
	if (a <= -0.015) {
		tmp = t_0;
	} else if (a <= 3.05) {
		tmp = x + (tan((fmin(y, z) + fmax(y, z))) - (a * fma((0.3333333333333333 * a), a, 1.0)));
	} else {
		tmp = t_0;
	}
	return tmp;
}

Julia

function code(x, y, z, a)
	t_0 = Float64(x + Float64(Float64(fmin(y, z) * Float64(1.0 + Float64(0.3333333333333333 * (fmin(y, z) ^ 2.0)))) - tan(a)))
	tmp = 0.0
	if (a <= -0.015)
		tmp = t_0;
	elseif (a <= 3.05)
		tmp = Float64(x + Float64(tan(Float64(fmin(y, z) + fmax(y, z))) - Float64(a * fma(Float64(0.3333333333333333 * a), a, 1.0))));
	else
		tmp = t_0;
	end
	return tmp
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[(x + N[(N[(N[Min[y, z], $MachinePrecision] * N[(1.0 + N[(0.3333333333333333 * N[Power[N[Min[y, z], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[a, -0.015], t$95$0, If[LessEqual[a, 3.05], N[(x + N[(N[Tan[N[(N[Min[y, z], $MachinePrecision] + N[Max[y, z], $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - N[(a * N[(N[(0.3333333333333333 * a), $MachinePrecision] * a + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0]]]

Derivation

1. Split input into 2 regimes

2. if a < -0.014999999999999999 or 3.0499999999999998 < a

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in z around 0

      \[\leadsto x + \left(\color{blue}{\frac{\sin y}{\cos y}} - \tan a\right) \]
   3. Step-by-step derivation

      1. lower-/.f64 N/A

         \[\leadsto x + \left(\frac{\sin y}{\color{blue}{\cos y}} - \tan a\right) \]

      2. lower-sin.f64 N/A

         \[\leadsto x + \left(\frac{\sin y}{\cos \color{blue}{y}} - \tan a\right) \]

      3. lower-cos.f64 59.9%

         \[\leadsto x + \left(\frac{\sin y}{\cos y} - \tan a\right) \]

   4. Applied rewrites 59.9%

      \[\leadsto x + \left(\color{blue}{\frac{\sin y}{\cos y}} - \tan a\right) \]

   5. Taylor expanded in y around 0

      \[\leadsto x + \left(y \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {y}^{2}\right)} - \tan a\right) \]
   6. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(y \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {y}^{2}}\right) - \tan a\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(y \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{y}^{2}}\right) - \tan a\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(y \cdot \left(1 + \frac{1}{3} \cdot {y}^{\color{blue}{2}}\right) - \tan a\right) \]

      4. lower-pow.f64 31.3%

         \[\leadsto x + \left(y \cdot \left(1 + 0.3333333333333333 \cdot {y}^{2}\right) - \tan a\right) \]

   7. Applied rewrites 31.3%

      \[\leadsto x + \left(y \cdot \color{blue}{\left(1 + 0.3333333333333333 \cdot {y}^{2}\right)} - \tan a\right) \]

   if -0.014999999999999999 < a < 3.0499999999999998

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in a around 0

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

      4. lower-pow.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

   4. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

      3. lift-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      4. lift-pow.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      5. unpow2 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

      6. associate-*r* N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

      8. lower-*.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   6. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 53.0% accurate, 0.6× speedup

Math

\[\begin{array}{l} t_0 := x + \left(\left(\mathsf{max}\left(y, z\right) + \mathsf{min}\left(y, z\right) \cdot \left(1 + \mathsf{min}\left(y, z\right) \cdot \mathsf{max}\left(y, z\right)\right)\right) - \tan a\right)\\ \mathbf{if}\;\tan a \leq -0.01:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;\tan a \leq 2 \cdot 10^{-5}:\\ \;\;\;\;x + \left(\tan \left(\mathsf{min}\left(y, z\right) + \mathsf{max}\left(y, z\right)\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0
        (+
         x
         (-
          (+
           (fmax y z)
           (* (fmin y z) (+ 1.0 (* (fmin y z) (fmax y z)))))
          (tan a)))))
  (if (<= (tan a) -0.01)
    t_0
    (if (<= (tan a) 2e-5)
      (+
       x
       (-
        (tan (+ (fmin y z) (fmax y z)))
        (* a (fma (* 0.3333333333333333 a) a 1.0))))
      t_0))))

C

double code(double x, double y, double z, double a) {
	double t_0 = x + ((fmax(y, z) + (fmin(y, z) * (1.0 + (fmin(y, z) * fmax(y, z))))) - tan(a));
	double tmp;
	if (tan(a) <= -0.01) {
		tmp = t_0;
	} else if (tan(a) <= 2e-5) {
		tmp = x + (tan((fmin(y, z) + fmax(y, z))) - (a * fma((0.3333333333333333 * a), a, 1.0)));
	} else {
		tmp = t_0;
	}
	return tmp;
}

Julia

function code(x, y, z, a)
	t_0 = Float64(x + Float64(Float64(fmax(y, z) + Float64(fmin(y, z) * Float64(1.0 + Float64(fmin(y, z) * fmax(y, z))))) - tan(a)))
	tmp = 0.0
	if (tan(a) <= -0.01)
		tmp = t_0;
	elseif (tan(a) <= 2e-5)
		tmp = Float64(x + Float64(tan(Float64(fmin(y, z) + fmax(y, z))) - Float64(a * fma(Float64(0.3333333333333333 * a), a, 1.0))));
	else
		tmp = t_0;
	end
	return tmp
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[(x + N[(N[(N[Max[y, z], $MachinePrecision] + N[(N[Min[y, z], $MachinePrecision] * N[(1.0 + N[(N[Min[y, z], $MachinePrecision] * N[Max[y, z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[Tan[a], $MachinePrecision], -0.01], t$95$0, If[LessEqual[N[Tan[a], $MachinePrecision], 2e-5], N[(x + N[(N[Tan[N[(N[Min[y, z], $MachinePrecision] + N[Max[y, z], $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - N[(a * N[(N[(0.3333333333333333 * a), $MachinePrecision] * a + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0]]]

Derivation

1. Split input into 2 regimes

2. if (tan.f64 a) < -0.01 or 2.0000000000000002e-5 < (tan.f64 a)

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. lift-tan.f64 N/A

         \[\leadsto x + \left(\color{blue}{\tan \left(y + z\right)} - \tan a\right) \]

      2. tan-quot N/A

         \[\leadsto x + \left(\color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} - \tan a\right) \]

      3. lift-+.f64 N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(y + z\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      4. +-commutative N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(z + y\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      5. sin-sum N/A

         \[\leadsto x + \left(\frac{\color{blue}{\sin z \cdot \cos y + \cos z \cdot \sin y}}{\cos \left(y + z\right)} - \tan a\right) \]

      6. div-add N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      7. *-commutative N/A

         \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\color{blue}{\sin y \cdot \cos z}}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      8. lower-+.f64 N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\left(\color{blue}{\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      10. lower-*.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z \cdot \cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z} \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      12. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \color{blue}{\cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      13. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      14. lift-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      15. +-commutative N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      16. lower-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      17. lower-/.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \color{blue}{\frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}}\right) - \tan a\right) \]

   3. Applied rewrites 80.2%

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right)} - \tan a\right) \]

   4. Taylor expanded in z around 0

      \[\leadsto x + \left(\color{blue}{\left(z \cdot \left(1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}\right) + \frac{\sin y}{\cos y}\right)} - \tan a\right) \]
   5. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, \color{blue}{1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      2. lower--.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - \color{blue}{-1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \color{blue}{\frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      4. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{\color{blue}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\color{blue}{\cos y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      6. lower-sin.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos \color{blue}{y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      7. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{\color{blue}{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      8. lower-cos.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      10. lower-sin.f64 N/A

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      11. lower-cos.f64 50.6%

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

   6. Applied rewrites 50.6%

      \[\leadsto x + \left(\color{blue}{\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right)} - \tan a\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot z\right)}\right) - \tan a\right) \]
   8. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \color{blue}{\left(1 + y \cdot z\right)}\right) - \tan a\right) \]

      2. lower-*.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + \color{blue}{y \cdot z}\right)\right) - \tan a\right) \]

      3. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \color{blue}{z}\right)\right) - \tan a\right) \]

      4. lower-*.f64 26.4%

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot z\right)\right) - \tan a\right) \]

   9. Applied rewrites 26.4%

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot z\right)}\right) - \tan a\right) \]

   if -0.01 < (tan.f64 a) < 2.0000000000000002e-5

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in a around 0

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

      4. lower-pow.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

   4. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

      3. lift-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      4. lift-pow.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      5. unpow2 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

      6. associate-*r* N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

      8. lower-*.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   6. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 8: 43.2% accurate, 0.6× speedup

Math

\[\begin{array}{l} t_0 := x + \left(\left(\mathsf{max}\left(y, z\right) + \mathsf{min}\left(y, z\right) \cdot \left(1 + \mathsf{min}\left(y, z\right) \cdot \mathsf{max}\left(y, z\right)\right)\right) - \tan a\right)\\ \mathbf{if}\;\tan a \leq -0.01:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;\tan a \leq 10^{-8}:\\ \;\;\;\;x + \left(\tan \left(\mathsf{max}\left(y, z\right)\right) - a \cdot \mathsf{fma}\left(0.3333333333333333, a \cdot a, 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (let* ((t_0
        (+
         x
         (-
          (+
           (fmax y z)
           (* (fmin y z) (+ 1.0 (* (fmin y z) (fmax y z)))))
          (tan a)))))
  (if (<= (tan a) -0.01)
    t_0
    (if (<= (tan a) 1e-8)
      (+
       x
       (-
        (tan (fmax y z))
        (* a (fma 0.3333333333333333 (* a a) 1.0))))
      t_0))))

C

double code(double x, double y, double z, double a) {
	double t_0 = x + ((fmax(y, z) + (fmin(y, z) * (1.0 + (fmin(y, z) * fmax(y, z))))) - tan(a));
	double tmp;
	if (tan(a) <= -0.01) {
		tmp = t_0;
	} else if (tan(a) <= 1e-8) {
		tmp = x + (tan(fmax(y, z)) - (a * fma(0.3333333333333333, (a * a), 1.0)));
	} else {
		tmp = t_0;
	}
	return tmp;
}

Julia

function code(x, y, z, a)
	t_0 = Float64(x + Float64(Float64(fmax(y, z) + Float64(fmin(y, z) * Float64(1.0 + Float64(fmin(y, z) * fmax(y, z))))) - tan(a)))
	tmp = 0.0
	if (tan(a) <= -0.01)
		tmp = t_0;
	elseif (tan(a) <= 1e-8)
		tmp = Float64(x + Float64(tan(fmax(y, z)) - Float64(a * fma(0.3333333333333333, Float64(a * a), 1.0))));
	else
		tmp = t_0;
	end
	return tmp
end

Wolfram

code[x_, y_, z_, a_] := Block[{t$95$0 = N[(x + N[(N[(N[Max[y, z], $MachinePrecision] + N[(N[Min[y, z], $MachinePrecision] * N[(1.0 + N[(N[Min[y, z], $MachinePrecision] * N[Max[y, z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[Tan[a], $MachinePrecision], -0.01], t$95$0, If[LessEqual[N[Tan[a], $MachinePrecision], 1e-8], N[(x + N[(N[Tan[N[Max[y, z], $MachinePrecision]], $MachinePrecision] - N[(a * N[(0.3333333333333333 * N[(a * a), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0]]]

Derivation

1. Split input into 2 regimes

2. if (tan.f64 a) < -0.01 or 1e-8 < (tan.f64 a)

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. lift-tan.f64 N/A

         \[\leadsto x + \left(\color{blue}{\tan \left(y + z\right)} - \tan a\right) \]

      2. tan-quot N/A

         \[\leadsto x + \left(\color{blue}{\frac{\sin \left(y + z\right)}{\cos \left(y + z\right)}} - \tan a\right) \]

      3. lift-+.f64 N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(y + z\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      4. +-commutative N/A

         \[\leadsto x + \left(\frac{\sin \color{blue}{\left(z + y\right)}}{\cos \left(y + z\right)} - \tan a\right) \]

      5. sin-sum N/A

         \[\leadsto x + \left(\frac{\color{blue}{\sin z \cdot \cos y + \cos z \cdot \sin y}}{\cos \left(y + z\right)} - \tan a\right) \]

      6. div-add N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\cos z \cdot \sin y}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      7. *-commutative N/A

         \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\color{blue}{\sin y \cdot \cos z}}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      8. lower-+.f64 N/A

         \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right)} - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\left(\color{blue}{\frac{\sin z \cdot \cos y}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      10. lower-*.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z \cdot \cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      11. lower-sin.f64 N/A

          \[\leadsto x + \left(\left(\frac{\color{blue}{\sin z} \cdot \cos y}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      12. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \color{blue}{\cos y}}{\cos \left(y + z\right)} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      13. lower-cos.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\color{blue}{\cos \left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      14. lift-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(y + z\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      15. +-commutative N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      16. lower-+.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \color{blue}{\left(z + y\right)}} + \frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}\right) - \tan a\right) \]

      17. lower-/.f64 N/A

          \[\leadsto x + \left(\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \color{blue}{\frac{\sin y \cdot \cos z}{\cos \left(y + z\right)}}\right) - \tan a\right) \]

   3. Applied rewrites 80.2%

      \[\leadsto x + \left(\color{blue}{\left(\frac{\sin z \cdot \cos y}{\cos \left(z + y\right)} + \frac{\cos z \cdot \sin y}{\cos \left(z + y\right)}\right)} - \tan a\right) \]

   4. Taylor expanded in z around 0

      \[\leadsto x + \left(\color{blue}{\left(z \cdot \left(1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}\right) + \frac{\sin y}{\cos y}\right)} - \tan a\right) \]
   5. Step-by-step derivation

      1. lower-fma.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, \color{blue}{1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      2. lower--.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - \color{blue}{-1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \color{blue}{\frac{{\sin y}^{2}}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      4. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{\color{blue}{{\cos y}^{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      5. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\color{blue}{\cos y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      6. lower-sin.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos \color{blue}{y}}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      7. lower-pow.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{\color{blue}{2}}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      8. lower-cos.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      10. lower-sin.f64 N/A

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

      11. lower-cos.f64 50.6%

          \[\leadsto x + \left(\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right) - \tan a\right) \]

   6. Applied rewrites 50.6%

      \[\leadsto x + \left(\color{blue}{\mathsf{fma}\left(z, 1 - -1 \cdot \frac{{\sin y}^{2}}{{\cos y}^{2}}, \frac{\sin y}{\cos y}\right)} - \tan a\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot z\right)}\right) - \tan a\right) \]
   8. Step-by-step derivation

      1. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \color{blue}{\left(1 + y \cdot z\right)}\right) - \tan a\right) \]

      2. lower-*.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + \color{blue}{y \cdot z}\right)\right) - \tan a\right) \]

      3. lower-+.f64 N/A

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot \color{blue}{z}\right)\right) - \tan a\right) \]

      4. lower-*.f64 26.4%

         \[\leadsto x + \left(\left(z + y \cdot \left(1 + y \cdot z\right)\right) - \tan a\right) \]

   9. Applied rewrites 26.4%

      \[\leadsto x + \left(\left(z + \color{blue}{y \cdot \left(1 + y \cdot z\right)}\right) - \tan a\right) \]

   if -0.01 < (tan.f64 a) < 1e-8

   1. Initial program 79.7%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

   2. Taylor expanded in a around 0

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
   3. Step-by-step derivation

      1. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

      2. lower-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      3. lower-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

      4. lower-pow.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

   4. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
   5. Step-by-step derivation

      1. lift-+.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

      3. lift-*.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      4. lift-pow.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

      5. unpow2 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

      6. associate-*r* N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

      7. lower-fma.f64 N/A

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

      8. lower-*.f64 41.1%

         \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

   6. Applied rewrites 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]

   7. Taylor expanded in y around 0

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 31.4%

      \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
   10. Step-by-step derivation

       1. lift-fma.f64 N/A

          \[\leadsto x + \left(\tan z - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + \color{blue}{1}\right)\right) \]

       2. lift-*.f64 N/A

          \[\leadsto x + \left(\tan z - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

       3. associate-*l* N/A

          \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

       4. lower-*.f32 N/A

          \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

       5. lower-unsound-*.f32 N/A

          \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

       6. lower-fma.f64 N/A

          \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(\frac{1}{3}, \color{blue}{a \cdot a}, 1\right)\right) \]

       7. lower-unsound-*.f64 31.4%

          \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(0.3333333333333333, a \cdot \color{blue}{a}, 1\right)\right) \]

   11. Applied rewrites 31.4%

       \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(0.3333333333333333, \color{blue}{a \cdot a}, 1\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 9: 31.3% accurate, 1.4× speedup

Math

\[x + \left(\tan \left(\mathsf{max}\left(y, z\right)\right) - a \cdot \mathsf{fma}\left(0.3333333333333333, a \cdot a, 1\right)\right) \]

FPCore

(FPCore (x y z a)
  :precision binary64
  (+ x (- (tan (fmax y z)) (* a (fma 0.3333333333333333 (* a a) 1.0)))))

C

double code(double x, double y, double z, double a) {
	return x + (tan(fmax(y, z)) - (a * fma(0.3333333333333333, (a * a), 1.0)));
}

Julia

function code(x, y, z, a)
	return Float64(x + Float64(tan(fmax(y, z)) - Float64(a * fma(0.3333333333333333, Float64(a * a), 1.0))))
end

Wolfram

code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[Max[y, z], $MachinePrecision]], $MachinePrecision] - N[(a * N[(0.3333333333333333 * N[(a * a), $MachinePrecision] + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 79.7%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

2. Taylor expanded in a around 0

   \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]
3. Step-by-step derivation

   1. lower-*.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {a}^{2}\right)}\right) \]

   2. lower-+.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

   3. lower-*.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{a}^{2}}\right)\right) \]

   4. lower-pow.f64 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{\color{blue}{2}}\right)\right) \]

4. Applied rewrites 41.1%

   \[\leadsto x + \left(\tan \left(y + z\right) - \color{blue}{a \cdot \left(1 + 0.3333333333333333 \cdot {a}^{2}\right)}\right) \]
5. Step-by-step derivation

   1. lift-+.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {a}^{2}}\right)\right) \]

   2. +-commutative N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + \color{blue}{1}\right)\right) \]

   3. lift-*.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

   4. lift-pow.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot {a}^{2} + 1\right)\right) \]

   5. unpow2 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

   6. associate-*r* N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

   7. lower-fma.f64 N/A

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(\frac{1}{3} \cdot a, \color{blue}{a}, 1\right)\right) \]

   8. lower-*.f64 41.1%

      \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]

6. Applied rewrites 41.1%

   \[\leadsto x + \left(\tan \left(y + z\right) - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, \color{blue}{a}, 1\right)\right) \]

7. Taylor expanded in y around 0

   \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
8. Step-by-step derivation

9. Applied rewrites 31.4%

   \[\leadsto x + \left(\tan \color{blue}{z} - a \cdot \mathsf{fma}\left(0.3333333333333333 \cdot a, a, 1\right)\right) \]
10. Step-by-step derivation

    1. lift-fma.f64 N/A

       \[\leadsto x + \left(\tan z - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + \color{blue}{1}\right)\right) \]

    2. lift-*.f64 N/A

       \[\leadsto x + \left(\tan z - a \cdot \left(\left(\frac{1}{3} \cdot a\right) \cdot a + 1\right)\right) \]

    3. associate-*l* N/A

       \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

    4. lower-*.f32 N/A

       \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

    5. lower-unsound-*.f32 N/A

       \[\leadsto x + \left(\tan z - a \cdot \left(\frac{1}{3} \cdot \left(a \cdot a\right) + 1\right)\right) \]

    6. lower-fma.f64 N/A

       \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(\frac{1}{3}, \color{blue}{a \cdot a}, 1\right)\right) \]

    7. lower-unsound-*.f64 31.4%

       \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(0.3333333333333333, a \cdot \color{blue}{a}, 1\right)\right) \]

11. Applied rewrites 31.4%

    \[\leadsto x + \left(\tan z - a \cdot \mathsf{fma}\left(0.3333333333333333, \color{blue}{a \cdot a}, 1\right)\right) \]
12. Add Preprocessing

Reproduce

herbie shell --seed 2025210 
(FPCore (x y z a)
  :name "tan-example (used to crash)"
  :precision binary64
  :pre (and (and (and (or (== x 0.0) (and (<= 0.5884142 x) (<= x 505.5909))) (or (and (<= -1.796658e+308 y) (<= y -9.425585e-310)) (and (<= 1.284938e-309 y) (<= y 1.751224e+308)))) (or (and (<= -1.776707e+308 z) (<= z -8.599796e-310)) (and (<= 3.293145e-311 z) (<= z 1.725154e+308)))) (or (and (<= -1.796658e+308 a) (<= a -9.425585e-310)) (and (<= 1.284938e-309 a) (<= a 1.751224e+308))))
  (+ x (- (tan (+ y z)) (tan a))))