(tan (* (PI) (* x 2)))

Percentage Accurate: 52.8% → 93.4%
Time: 55.2s
Alternatives: 9
Speedup: 1.0×

Specification

?
\[\begin{array}{l} \\ \tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \end{array} \]
(FPCore (x) :precision binary64 (tan (* (PI) (* x 2.0))))
\begin{array}{l}

\\
\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right)
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 9 alternatives:

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

Initial Program: 52.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \end{array} \]
(FPCore (x) :precision binary64 (tan (* (PI) (* x 2.0))))
\begin{array}{l}

\\
\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right)
\end{array}

Alternative 1: 93.4% accurate, 0.4× speedup?

\[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\sin \left(2 \cdot x\_m\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(1.6253968253968254, x\_m \cdot x\_m, -4.266666666666667\right), x\_m \cdot x\_m, 5.333333333333333\right), x\_m \cdot x\_m, -2\right) \cdot x\_m}\\ \end{array} \end{array} \]
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (/ (sin (* (+ x_m x_m) (PI))) (cos (* (* 2.0 x_m) (PI))))
    (/
     (* (pow (sin (* 2.0 x_m)) 2.0) (PI))
     (-
      (*
       (fma
        (fma
         (fma 1.6253968253968254 (* x_m x_m) -4.266666666666667)
         (* x_m x_m)
         5.333333333333333)
        (* x_m x_m)
        -2.0)
       x_m))))))
\begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{{\sin \left(2 \cdot x\_m\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(1.6253968253968254, x\_m \cdot x\_m, -4.266666666666667\right), x\_m \cdot x\_m, 5.333333333333333\right), x\_m \cdot x\_m, -2\right) \cdot x\_m}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (*.f64 x #s(literal 2 binary64)) < 5e9

    1. Initial program 64.0%

      \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
    2. Add Preprocessing

    3. Taylor expanded in x around inf

      \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
    4. Step-by-step derivation

      1. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

      2. *-commutativeN/A

        \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      3. associate-*r*N/A

        \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      4. lower-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      5. associate-*r*N/A

        \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      6. *-commutativeN/A

        \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      7. associate-*r*N/A

        \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      8. lower-*.f64N/A

        \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      9. lower-*.f64N/A

        \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      10. lower-PI.f64N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

      11. *-commutativeN/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

      12. associate-*r*N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

      13. lower-cos.f64N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

      14. associate-*r*N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

      15. *-commutativeN/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

      16. associate-*r*N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

      17. lower-*.f64N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

      18. lower-*.f64N/A

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

      19. lower-PI.f6464.0

        \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

    5. Applied rewrites64.0%

      \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]
    6. Step-by-step derivation

      1. Applied rewrites64.0%

        \[\leadsto \frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(\color{blue}{2} \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)} \]

      if 5e9 < (*.f64 x #s(literal 2 binary64))

      1. Initial program 3.1%

        \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
      2. Add Preprocessing

      4. Applied rewrites3.1%

        \[\leadsto \color{blue}{\frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\sin \left(2 \cdot x\right) \cdot \left(-\cos \left(x + x\right)\right)}} \]

      5. Taylor expanded in x around 0

        \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{x \cdot \left({x}^{2} \cdot \left(\frac{16}{3} + {x}^{2} \cdot \left(\frac{512}{315} \cdot {x}^{2} - \frac{64}{15}\right)\right) - 2\right)}} \]
      6. Step-by-step derivation

        1. *-commutativeN/A

          \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left({x}^{2} \cdot \left(\frac{16}{3} + {x}^{2} \cdot \left(\frac{512}{315} \cdot {x}^{2} - \frac{64}{15}\right)\right) - 2\right) \cdot x}} \]

        2. lower-*.f64N/A

          \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left({x}^{2} \cdot \left(\frac{16}{3} + {x}^{2} \cdot \left(\frac{512}{315} \cdot {x}^{2} - \frac{64}{15}\right)\right) - 2\right) \cdot x}} \]

      7. Applied rewrites88.1%

        \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(1.6253968253968254, x \cdot x, -4.266666666666667\right), x \cdot x, 5.333333333333333\right), x \cdot x, -2\right) \cdot x}} \]
    7. Recombined 2 regimes into one program.

    8. Final simplification69.1%

      \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\sin \left(2 \cdot x\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(1.6253968253968254, x \cdot x, -4.266666666666667\right), x \cdot x, 5.333333333333333\right), x \cdot x, -2\right) \cdot x}\\ \end{array} \]
    9. Add Preprocessing

    Alternative 2: 84.9% accurate, 0.3× speedup?

    \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;{\tan \left({\left(2 \cdot x\_m\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\ \end{array} \end{array} \]
    x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (/ (sin (* (+ x_m x_m) (PI))) (cos (* (* 2.0 x_m) (PI))))
    (pow (tan (pow (* 2.0 x_m) -1.0)) (PI)))))
    \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;{\tan \left({\left(2 \cdot x\_m\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\


\end{array}
\end{array}
    Derivation
    1. Split input into 2 regimes

    2. if (*.f64 x #s(literal 2 binary64)) < 5e9

      1. Initial program 64.0%

        \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
      2. Add Preprocessing

      3. Taylor expanded in x around inf

        \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
      4. Step-by-step derivation

        1. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

        2. *-commutativeN/A

          \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        3. associate-*r*N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        4. lower-sin.f64N/A

          \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        5. associate-*r*N/A

          \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        6. *-commutativeN/A

          \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        7. associate-*r*N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        8. lower-*.f64N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        9. lower-*.f64N/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        10. lower-PI.f64N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

        11. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

        12. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

        13. lower-cos.f64N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

        14. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

        15. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

        16. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

        17. lower-*.f64N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

        18. lower-*.f64N/A

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

        19. lower-PI.f6464.0

          \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

      5. Applied rewrites64.0%

        \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]
      6. Step-by-step derivation

        1. Applied rewrites64.0%

          \[\leadsto \frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(\color{blue}{2} \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)} \]

        if 5e9 < (*.f64 x #s(literal 2 binary64))

        1. Initial program 3.1%

          \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
        2. Add Preprocessing

        4. Applied rewrites1.9%

          \[\leadsto \color{blue}{{\tan \left(2 \cdot x\right)}^{\mathsf{PI}\left(\right)}} \]
        5. Step-by-step derivation

          1. lift-*.f64N/A

            \[\leadsto {\tan \color{blue}{\left(2 \cdot x\right)}}^{\mathsf{PI}\left(\right)} \]

          2. count-2N/A

            \[\leadsto {\tan \color{blue}{\left(x + x\right)}}^{\mathsf{PI}\left(\right)} \]

          3. flip-+N/A

            \[\leadsto {\tan \color{blue}{\left(\frac{x \cdot x - x \cdot x}{x - x}\right)}}^{\mathsf{PI}\left(\right)} \]

          4. clear-numN/A

            \[\leadsto {\tan \color{blue}{\left(\frac{1}{\frac{x - x}{x \cdot x - x \cdot x}}\right)}}^{\mathsf{PI}\left(\right)} \]

          5. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{\color{blue}{0}}{x \cdot x - x \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          6. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{\color{blue}{x \cdot x - x \cdot x}}{x \cdot x - x \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          7. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{x \cdot x - x \cdot x}{\color{blue}{0}}}\right)}^{\mathsf{PI}\left(\right)} \]

          8. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{x \cdot x - x \cdot x}{\color{blue}{x - x}}}\right)}^{\mathsf{PI}\left(\right)} \]

          9. flip-+N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{x + x}}\right)}^{\mathsf{PI}\left(\right)} \]

          10. count-2N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{2 \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          11. lift-*.f64N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{2 \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          12. lower-/.f6465.6

            \[\leadsto {\tan \color{blue}{\left(\frac{1}{2 \cdot x}\right)}}^{\mathsf{PI}\left(\right)} \]

        6. Applied rewrites65.6%

          \[\leadsto {\tan \color{blue}{\left(\frac{1}{2 \cdot x}\right)}}^{\mathsf{PI}\left(\right)} \]
      7. Recombined 2 regimes into one program.

      8. Final simplification64.4%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;{\tan \left({\left(2 \cdot x\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\ \end{array} \]
      9. Add Preprocessing

      Alternative 3: 84.9% accurate, 0.3× speedup?

      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\tan \left(\mathsf{PI}\left(\right) \cdot \left(x\_m \cdot 2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{\tan \left({\left(2 \cdot x\_m\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\ \end{array} \end{array} \]
      x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (tan (* (PI) (* x_m 2.0)))
    (pow (tan (pow (* 2.0 x_m) -1.0)) (PI)))))
      \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\tan \left(\mathsf{PI}\left(\right) \cdot \left(x\_m \cdot 2\right)\right)\\

\mathbf{else}:\\
\;\;\;\;{\tan \left({\left(2 \cdot x\_m\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\


\end{array}
\end{array}
      Derivation
      1. Split input into 2 regimes

      2. if (*.f64 x #s(literal 2 binary64)) < 5e9

        1. Initial program 64.0%

          \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
        2. Add Preprocessing

        if 5e9 < (*.f64 x #s(literal 2 binary64))

        1. Initial program 3.1%

          \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
        2. Add Preprocessing

        4. Applied rewrites1.9%

          \[\leadsto \color{blue}{{\tan \left(2 \cdot x\right)}^{\mathsf{PI}\left(\right)}} \]
        5. Step-by-step derivation

          1. lift-*.f64N/A

            \[\leadsto {\tan \color{blue}{\left(2 \cdot x\right)}}^{\mathsf{PI}\left(\right)} \]

          2. count-2N/A

            \[\leadsto {\tan \color{blue}{\left(x + x\right)}}^{\mathsf{PI}\left(\right)} \]

          3. flip-+N/A

            \[\leadsto {\tan \color{blue}{\left(\frac{x \cdot x - x \cdot x}{x - x}\right)}}^{\mathsf{PI}\left(\right)} \]

          4. clear-numN/A

            \[\leadsto {\tan \color{blue}{\left(\frac{1}{\frac{x - x}{x \cdot x - x \cdot x}}\right)}}^{\mathsf{PI}\left(\right)} \]

          5. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{\color{blue}{0}}{x \cdot x - x \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          6. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{\color{blue}{x \cdot x - x \cdot x}}{x \cdot x - x \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          7. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{x \cdot x - x \cdot x}{\color{blue}{0}}}\right)}^{\mathsf{PI}\left(\right)} \]

          8. +-inversesN/A

            \[\leadsto {\tan \left(\frac{1}{\frac{x \cdot x - x \cdot x}{\color{blue}{x - x}}}\right)}^{\mathsf{PI}\left(\right)} \]

          9. flip-+N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{x + x}}\right)}^{\mathsf{PI}\left(\right)} \]

          10. count-2N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{2 \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          11. lift-*.f64N/A

            \[\leadsto {\tan \left(\frac{1}{\color{blue}{2 \cdot x}}\right)}^{\mathsf{PI}\left(\right)} \]

          12. lower-/.f6465.6

            \[\leadsto {\tan \color{blue}{\left(\frac{1}{2 \cdot x}\right)}}^{\mathsf{PI}\left(\right)} \]

        6. Applied rewrites65.6%

          \[\leadsto {\tan \color{blue}{\left(\frac{1}{2 \cdot x}\right)}}^{\mathsf{PI}\left(\right)} \]
      3. Recombined 2 regimes into one program.

      4. Final simplification64.4%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot 2 \leq 5000000000:\\ \;\;\;\;\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{\tan \left({\left(2 \cdot x\right)}^{-1}\right)}^{\mathsf{PI}\left(\right)}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 4: 92.2% accurate, 0.4× speedup?

      \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.08888888888888889, x\_m \cdot x\_m, 0.6666666666666666\right), x\_m \cdot x\_m, -2\right), x\_m \cdot x\_m, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\_m\right)\\ \end{array} \end{array} \]
      x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (/ (sin (* (+ x_m x_m) (PI))) (cos (* (* 2.0 x_m) (PI))))
    (*
     (/
      (pow
       (fma
        (fma
         (fma -0.08888888888888889 (* x_m x_m) 0.6666666666666666)
         (* x_m x_m)
         -2.0)
        (* x_m x_m)
        1.0)
       -1.0)
      (PI))
     (sin (* 2.0 x_m))))))
      \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.08888888888888889, x\_m \cdot x\_m, 0.6666666666666666\right), x\_m \cdot x\_m, -2\right), x\_m \cdot x\_m, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\_m\right)\\


\end{array}
\end{array}
      Derivation
      1. Split input into 2 regimes

      2. if (*.f64 x #s(literal 2 binary64)) < 5e9

        1. Initial program 64.0%

          \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
        2. Add Preprocessing

        3. Taylor expanded in x around inf

          \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
        4. Step-by-step derivation

          1. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

          2. *-commutativeN/A

            \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          3. associate-*r*N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          4. lower-sin.f64N/A

            \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          5. associate-*r*N/A

            \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          6. *-commutativeN/A

            \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          7. associate-*r*N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          8. lower-*.f64N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          9. lower-*.f64N/A

            \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          10. lower-PI.f64N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

          11. *-commutativeN/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

          12. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

          13. lower-cos.f64N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

          14. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

          15. *-commutativeN/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

          16. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

          17. lower-*.f64N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

          18. lower-*.f64N/A

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

          19. lower-PI.f6464.0

            \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

        5. Applied rewrites64.0%

          \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]
        6. Step-by-step derivation

          1. Applied rewrites64.0%

            \[\leadsto \frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(\color{blue}{2} \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)} \]

          if 5e9 < (*.f64 x #s(literal 2 binary64))

          1. Initial program 3.1%

            \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
          2. Add Preprocessing

          4. Applied rewrites3.1%

            \[\leadsto \color{blue}{\frac{{\cos \left(x + x\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right)} \]

          5. Taylor expanded in x around 0

            \[\leadsto \frac{{\color{blue}{\left(1 + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) - 2\right)\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]
          6. Step-by-step derivation

            1. +-commutativeN/A

              \[\leadsto \frac{{\color{blue}{\left({x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) - 2\right) + 1\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            2. *-commutativeN/A

              \[\leadsto \frac{{\left(\color{blue}{\left({x}^{2} \cdot \left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) - 2\right) \cdot {x}^{2}} + 1\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            3. lower-fma.f64N/A

              \[\leadsto \frac{{\color{blue}{\left(\mathsf{fma}\left({x}^{2} \cdot \left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) - 2, {x}^{2}, 1\right)\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            4. sub-negN/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\color{blue}{{x}^{2} \cdot \left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) + \left(\mathsf{neg}\left(2\right)\right)}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            5. *-commutativeN/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\color{blue}{\left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) \cdot {x}^{2}} + \left(\mathsf{neg}\left(2\right)\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            6. metadata-evalN/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}\right) \cdot {x}^{2} + \color{blue}{-2}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            7. lower-fma.f64N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{2}{3} + \frac{-4}{45} \cdot {x}^{2}, {x}^{2}, -2\right)}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            8. +-commutativeN/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\frac{-4}{45} \cdot {x}^{2} + \frac{2}{3}}, {x}^{2}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            9. lower-fma.f64N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-4}{45}, {x}^{2}, \frac{2}{3}\right)}, {x}^{2}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            10. unpow2N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-4}{45}, \color{blue}{x \cdot x}, \frac{2}{3}\right), {x}^{2}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            11. lower-*.f64N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-4}{45}, \color{blue}{x \cdot x}, \frac{2}{3}\right), {x}^{2}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            12. unpow2N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-4}{45}, x \cdot x, \frac{2}{3}\right), \color{blue}{x \cdot x}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            13. lower-*.f64N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-4}{45}, x \cdot x, \frac{2}{3}\right), \color{blue}{x \cdot x}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            14. unpow2N/A

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{-4}{45}, x \cdot x, \frac{2}{3}\right), x \cdot x, -2\right), \color{blue}{x \cdot x}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

            15. lower-*.f6482.7

              \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.08888888888888889, x \cdot x, 0.6666666666666666\right), x \cdot x, -2\right), \color{blue}{x \cdot x}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

          7. Applied rewrites82.7%

            \[\leadsto \frac{{\color{blue}{\left(\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-0.08888888888888889, x \cdot x, 0.6666666666666666\right), x \cdot x, -2\right), x \cdot x, 1\right)\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]
        7. Recombined 2 regimes into one program.
        8. Add Preprocessing

        Alternative 5: 90.6% accurate, 0.4× speedup?

        \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\sin \left(2 \cdot x\_m\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(-4.266666666666667, x\_m \cdot x\_m, 5.333333333333333\right), x\_m \cdot x\_m, -2\right) \cdot x\_m}\\ \end{array} \end{array} \]
        x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (/ (sin (* (+ x_m x_m) (PI))) (cos (* (* 2.0 x_m) (PI))))
    (/
     (* (pow (sin (* 2.0 x_m)) 2.0) (PI))
     (-
      (*
       (fma
        (fma -4.266666666666667 (* x_m x_m) 5.333333333333333)
        (* x_m x_m)
        -2.0)
       x_m))))))
        \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{{\sin \left(2 \cdot x\_m\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(-4.266666666666667, x\_m \cdot x\_m, 5.333333333333333\right), x\_m \cdot x\_m, -2\right) \cdot x\_m}\\


\end{array}
\end{array}
        Derivation
        1. Split input into 2 regimes

        2. if (*.f64 x #s(literal 2 binary64)) < 5e9

          1. Initial program 64.0%

            \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
          2. Add Preprocessing

          3. Taylor expanded in x around inf

            \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
          4. Step-by-step derivation

            1. lower-/.f64N/A

              \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

            2. *-commutativeN/A

              \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            3. associate-*r*N/A

              \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            4. lower-sin.f64N/A

              \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            5. associate-*r*N/A

              \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            6. *-commutativeN/A

              \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            7. associate-*r*N/A

              \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            8. lower-*.f64N/A

              \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            9. lower-*.f64N/A

              \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            10. lower-PI.f64N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

            11. *-commutativeN/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

            12. associate-*r*N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

            13. lower-cos.f64N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

            14. associate-*r*N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

            15. *-commutativeN/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

            16. associate-*r*N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

            17. lower-*.f64N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

            18. lower-*.f64N/A

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

            19. lower-PI.f6464.0

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

          5. Applied rewrites64.0%

            \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]
          6. Step-by-step derivation

            1. Applied rewrites64.0%

              \[\leadsto \frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(\color{blue}{2} \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)} \]

            if 5e9 < (*.f64 x #s(literal 2 binary64))

            1. Initial program 3.1%

              \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
            2. Add Preprocessing

            4. Applied rewrites3.1%

              \[\leadsto \color{blue}{\frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\sin \left(2 \cdot x\right) \cdot \left(-\cos \left(x + x\right)\right)}} \]

            5. Taylor expanded in x around 0

              \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{x \cdot \left({x}^{2} \cdot \left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) - 2\right)}} \]
            6. Step-by-step derivation

              1. *-commutativeN/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left({x}^{2} \cdot \left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) - 2\right) \cdot x}} \]

              2. lower-*.f64N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left({x}^{2} \cdot \left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) - 2\right) \cdot x}} \]

              3. sub-negN/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\left({x}^{2} \cdot \left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) + \left(\mathsf{neg}\left(2\right)\right)\right)} \cdot x} \]

              4. *-commutativeN/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\left(\color{blue}{\left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) \cdot {x}^{2}} + \left(\mathsf{neg}\left(2\right)\right)\right) \cdot x} \]

              5. metadata-evalN/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\left(\left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}\right) \cdot {x}^{2} + \color{blue}{-2}\right) \cdot x} \]

              6. lower-fma.f64N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\mathsf{fma}\left(\frac{16}{3} + \frac{-64}{15} \cdot {x}^{2}, {x}^{2}, -2\right)} \cdot x} \]

              7. +-commutativeN/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\color{blue}{\frac{-64}{15} \cdot {x}^{2} + \frac{16}{3}}, {x}^{2}, -2\right) \cdot x} \]

              8. lower-fma.f64N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{-64}{15}, {x}^{2}, \frac{16}{3}\right)}, {x}^{2}, -2\right) \cdot x} \]

              9. unpow2N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-64}{15}, \color{blue}{x \cdot x}, \frac{16}{3}\right), {x}^{2}, -2\right) \cdot x} \]

              10. lower-*.f64N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-64}{15}, \color{blue}{x \cdot x}, \frac{16}{3}\right), {x}^{2}, -2\right) \cdot x} \]

              11. unpow2N/A

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{fma}\left(\frac{-64}{15}, x \cdot x, \frac{16}{3}\right), \color{blue}{x \cdot x}, -2\right) \cdot x} \]

              12. lower-*.f6480.8

                \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\mathsf{fma}\left(\mathsf{fma}\left(-4.266666666666667, x \cdot x, 5.333333333333333\right), \color{blue}{x \cdot x}, -2\right) \cdot x} \]

            7. Applied rewrites80.8%

              \[\leadsto \frac{\left(-{\sin \left(2 \cdot x\right)}^{2}\right) \cdot \mathsf{PI}\left(\right)}{\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-4.266666666666667, x \cdot x, 5.333333333333333\right), x \cdot x, -2\right) \cdot x}} \]
          7. Recombined 2 regimes into one program.

          8. Final simplification67.6%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\sin \left(2 \cdot x\right)}^{2} \cdot \mathsf{PI}\left(\right)}{-\mathsf{fma}\left(\mathsf{fma}\left(-4.266666666666667, x \cdot x, 5.333333333333333\right), x \cdot x, -2\right) \cdot x}\\ \end{array} \]
          9. Add Preprocessing

          Alternative 6: 88.5% accurate, 0.4× speedup?

          \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \begin{array}{l} \mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\ \;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.6666666666666666, x\_m \cdot x\_m, -2\right), x\_m \cdot x\_m, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\_m\right)\\ \end{array} \end{array} \]
          x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (if (<= (* x_m 2.0) 5000000000.0)
    (/ (sin (* (+ x_m x_m) (PI))) (cos (* (* 2.0 x_m) (PI))))
    (*
     (/
      (pow
       (fma (fma 0.6666666666666666 (* x_m x_m) -2.0) (* x_m x_m) 1.0)
       -1.0)
      (PI))
     (sin (* 2.0 x_m))))))
          \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \begin{array}{l}
\mathbf{if}\;x\_m \cdot 2 \leq 5000000000:\\
\;\;\;\;\frac{\sin \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.6666666666666666, x\_m \cdot x\_m, -2\right), x\_m \cdot x\_m, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\_m\right)\\


\end{array}
\end{array}
          Derivation
          1. Split input into 2 regimes

          2. if (*.f64 x #s(literal 2 binary64)) < 5e9

            1. Initial program 64.0%

              \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
            2. Add Preprocessing

            3. Taylor expanded in x around inf

              \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
            4. Step-by-step derivation

              1. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

              2. *-commutativeN/A

                \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              3. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              4. lower-sin.f64N/A

                \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              5. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              6. *-commutativeN/A

                \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              7. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              8. lower-*.f64N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              9. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              10. lower-PI.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              11. *-commutativeN/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

              12. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

              13. lower-cos.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

              14. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

              15. *-commutativeN/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

              16. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

              17. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

              18. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

              19. lower-PI.f6464.0

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

            5. Applied rewrites64.0%

              \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]
            6. Step-by-step derivation

              1. Applied rewrites64.0%

                \[\leadsto \frac{\sin \left(\left(x + x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(\color{blue}{2} \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)} \]

              if 5e9 < (*.f64 x #s(literal 2 binary64))

              1. Initial program 3.1%

                \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
              2. Add Preprocessing

              4. Applied rewrites3.1%

                \[\leadsto \color{blue}{\frac{{\cos \left(x + x\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right)} \]

              5. Taylor expanded in x around 0

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

                1. +-commutativeN/A

                  \[\leadsto \frac{{\color{blue}{\left({x}^{2} \cdot \left(\frac{2}{3} \cdot {x}^{2} - 2\right) + 1\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                2. *-commutativeN/A

                  \[\leadsto \frac{{\left(\color{blue}{\left(\frac{2}{3} \cdot {x}^{2} - 2\right) \cdot {x}^{2}} + 1\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                3. lower-fma.f64N/A

                  \[\leadsto \frac{{\color{blue}{\left(\mathsf{fma}\left(\frac{2}{3} \cdot {x}^{2} - 2, {x}^{2}, 1\right)\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                4. sub-negN/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\color{blue}{\frac{2}{3} \cdot {x}^{2} + \left(\mathsf{neg}\left(2\right)\right)}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                5. metadata-evalN/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\frac{2}{3} \cdot {x}^{2} + \color{blue}{-2}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                6. lower-fma.f64N/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(\frac{2}{3}, {x}^{2}, -2\right)}, {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                7. unpow2N/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{2}{3}, \color{blue}{x \cdot x}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                8. lower-*.f64N/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{2}{3}, \color{blue}{x \cdot x}, -2\right), {x}^{2}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                9. unpow2N/A

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(\frac{2}{3}, x \cdot x, -2\right), \color{blue}{x \cdot x}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

                10. lower-*.f6475.6

                  \[\leadsto \frac{{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.6666666666666666, x \cdot x, -2\right), \color{blue}{x \cdot x}, 1\right)\right)}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]

              7. Applied rewrites75.6%

                \[\leadsto \frac{{\color{blue}{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.6666666666666666, x \cdot x, -2\right), x \cdot x, 1\right)\right)}}^{-1}}{\mathsf{PI}\left(\right)} \cdot \sin \left(2 \cdot x\right) \]
            7. Recombined 2 regimes into one program.
            8. Add Preprocessing

            Alternative 7: 75.7% accurate, 0.8× speedup?

            \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \frac{\sin \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\mathsf{fma}\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -2, x\_m \cdot x\_m, 1\right)} \end{array} \]
            x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m)
 :precision binary64
 (*
  x_s
  (/ (sin (* (* 2.0 x_m) (PI))) (fma (* (* (PI) (PI)) -2.0) (* x_m x_m) 1.0))))
            \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \frac{\sin \left(\left(2 \cdot x\_m\right) \cdot \mathsf{PI}\left(\right)\right)}{\mathsf{fma}\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -2, x\_m \cdot x\_m, 1\right)}
\end{array}
            Derivation

            1. Initial program 51.2%

              \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
            2. Add Preprocessing

            3. Taylor expanded in x around inf

              \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]
            4. Step-by-step derivation

              1. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\sin \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

              2. *-commutativeN/A

                \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              3. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              4. lower-sin.f64N/A

                \[\leadsto \frac{\color{blue}{\sin \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              5. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              6. *-commutativeN/A

                \[\leadsto \frac{\sin \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              7. associate-*r*N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              8. lower-*.f64N/A

                \[\leadsto \frac{\sin \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              9. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              10. lower-PI.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}{\cos \left(2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)} \]

              11. *-commutativeN/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot x\right)}\right)} \]

              12. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

              13. lower-cos.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\cos \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot x\right)}} \]

              14. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}} \]

              15. *-commutativeN/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(2 \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)} \]

              16. associate-*r*N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

              17. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \color{blue}{\left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

              18. lower-*.f64N/A

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)} \]

              19. lower-PI.f6451.2

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]

            5. Applied rewrites51.2%

              \[\leadsto \color{blue}{\frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\cos \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}} \]

            6. Taylor expanded in x around 0

              \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{1 + \color{blue}{-2 \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}} \]
            7. Step-by-step derivation

              1. Applied rewrites71.9%

                \[\leadsto \frac{\sin \left(\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\mathsf{fma}\left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -2, \color{blue}{x \cdot x}, 1\right)} \]
              2. Add Preprocessing

              Alternative 8: 52.8% accurate, 1.0× speedup?

              \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \tan \left(\mathsf{PI}\left(\right) \cdot \left(x\_m \cdot 2\right)\right) \end{array} \]
              x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m) :precision binary64 (* x_s (tan (* (PI) (* x_m 2.0)))))
              \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \tan \left(\mathsf{PI}\left(\right) \cdot \left(x\_m \cdot 2\right)\right)
\end{array}
              Derivation

              1. Initial program 51.2%

                \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
              2. Add Preprocessing
              3. Add Preprocessing

              Alternative 9: 50.6% accurate, 12.3× speedup?

              \[\begin{array}{l} x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ x\_s \cdot \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right) \end{array} \]
              x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
(FPCore (x_s x_m) :precision binary64 (* x_s (* (+ x_m x_m) (PI))))
              \begin{array}{l}
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)

\\
x\_s \cdot \left(\left(x\_m + x\_m\right) \cdot \mathsf{PI}\left(\right)\right)
\end{array}
              Derivation

              1. Initial program 51.2%

                \[\tan \left(\mathsf{PI}\left(\right) \cdot \left(x \cdot 2\right)\right) \]
              2. Add Preprocessing

              3. Taylor expanded in x around 0

                \[\leadsto \color{blue}{2 \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)} \]
              4. Step-by-step derivation

                1. associate-*r*N/A

                  \[\leadsto \color{blue}{\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)} \]

                2. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)} \]

                3. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(2 \cdot x\right)} \cdot \mathsf{PI}\left(\right) \]

                4. lower-PI.f6449.6

                  \[\leadsto \left(2 \cdot x\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} \]

              5. Applied rewrites49.6%

                \[\leadsto \color{blue}{\left(2 \cdot x\right) \cdot \mathsf{PI}\left(\right)} \]
              6. Step-by-step derivation

                1. Applied rewrites49.6%

                  \[\leadsto \left(x + x\right) \cdot \mathsf{PI}\left(\right) \]
                2. Add Preprocessing

                Reproduce

                ?
                herbie shell --seed 1 
(FPCore (x)
  :name "(tan (* (PI) (* x 2)))"
  :precision binary64
  (tan (* (PI) (* x 2.0))))