Lanczos kernel

Percentage Accurate: 98.0% → 97.8%
Time: 7.6s
Alternatives: 13
Speedup: N/A×

Specification

?
\[\left(10^{-5} \leq x \land x \leq 1\right) \land \left(1 \leq tau \land tau \leq 5\right)\]
\[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ \frac{\sin t\_2}{t\_2} \cdot \frac{\sin t\_1}{t\_1} \end{array} \end{array} \]
(FPCore (x tau)
 :precision binary32
 (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)))
   (* (/ (sin t_2) t_2) (/ (sin t_1) t_1))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := x \cdot \mathsf{PI}\left(\right)\\
t_2 := t\_1 \cdot tau\\
\frac{\sin t\_2}{t\_2} \cdot \frac{\sin t\_1}{t\_1}
\end{array}
\end{array}

Sampling outcomes in binary32 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 13 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: 98.0% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ \frac{\sin t\_2}{t\_2} \cdot \frac{\sin t\_1}{t\_1} \end{array} \end{array} \]
(FPCore (x tau)
 :precision binary32
 (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)))
   (* (/ (sin t_2) t_2) (/ (sin t_1) t_1))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := x \cdot \mathsf{PI}\left(\right)\\
t_2 := t\_1 \cdot tau\\
\frac{\sin t\_2}{t\_2} \cdot \frac{\sin t\_1}{t\_1}
\end{array}
\end{array}

Alternative 1: 97.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ \frac{\sin t\_2 \cdot \sin t\_1}{t\_1 \cdot t\_2} \end{array} \end{array} \]
(FPCore (x tau)
 :precision binary32
 (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)))
   (/ (* (sin t_2) (sin t_1)) (* t_1 t_2))))
\begin{array}{l}

\\
\begin{array}{l}
t_1 := x \cdot \mathsf{PI}\left(\right)\\
t_2 := t\_1 \cdot tau\\
\frac{\sin t\_2 \cdot \sin t\_1}{t\_1 \cdot t\_2}
\end{array}
\end{array}
Derivation
  1. Initial program 97.5%

    \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
    2. lift-/.f32N/A

      \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
    3. associate-*l/N/A

      \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
    4. lower-/.f32N/A

      \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
  4. Applied rewrites97.5%

    \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
  5. Applied rewrites81.5%

    \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
  6. Step-by-step derivation
    1. Applied rewrites97.6%

      \[\leadsto \frac{\color{blue}{\sin \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
    2. Final simplification97.6%

      \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
    3. Add Preprocessing

    Alternative 2: 97.2% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ \mathbf{if}\;x \leq 0.023000000044703484:\\ \;\;\;\;\frac{\sin t\_2}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(tau \cdot \mathsf{PI}\left(\right), x, \mathsf{PI}\left(\right)\right)\right) \cdot \sin t\_1}{t\_1 \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\ \end{array} \end{array} \]
    (FPCore (x tau)
     :precision binary32
     (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)))
       (if (<= x 0.023000000044703484)
         (*
          (/ (sin t_2) t_2)
          (fma (* (* -0.16666666666666666 x) x) (* (PI) (PI)) 1.0))
         (/
          (* (sin (fma (* tau (PI)) x (PI))) (sin t_1))
          (* t_1 (* (* (- x) (PI)) tau))))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := x \cdot \mathsf{PI}\left(\right)\\
    t_2 := t\_1 \cdot tau\\
    \mathbf{if}\;x \leq 0.023000000044703484:\\
    \;\;\;\;\frac{\sin t\_2}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(tau \cdot \mathsf{PI}\left(\right), x, \mathsf{PI}\left(\right)\right)\right) \cdot \sin t\_1}{t\_1 \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if x < 0.023

      1. Initial program 98.4%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
        2. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
        3. lower-fma.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
        4. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        5. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        7. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right)} \cdot x, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        10. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lower-PI.f3298.4

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
      5. Applied rewrites98.4%

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

      if 0.023 < x

      1. Initial program 96.0%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
        2. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        3. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
        4. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. Applied rewrites95.9%

        \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
      5. Applied rewrites93.3%

        \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
      6. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        3. add-log-expN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \color{blue}{\log \left(e^{\mathsf{PI}\left(\right)}\right)}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        4. log-pow-revN/A

          \[\leadsto \frac{\sin \color{blue}{\log \left({\left(e^{\mathsf{PI}\left(\right)}\right)}^{\left(\mathsf{fma}\left(x, tau, 1\right)\right)}\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        5. lift-fma.f32N/A

          \[\leadsto \frac{\sin \log \left({\left(e^{\mathsf{PI}\left(\right)}\right)}^{\color{blue}{\left(x \cdot tau + 1\right)}}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        6. lift-*.f32N/A

          \[\leadsto \frac{\sin \log \left({\left(e^{\mathsf{PI}\left(\right)}\right)}^{\left(\color{blue}{x \cdot tau} + 1\right)}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        7. pow-plus-revN/A

          \[\leadsto \frac{\sin \log \color{blue}{\left({\left(e^{\mathsf{PI}\left(\right)}\right)}^{\left(x \cdot tau\right)} \cdot e^{\mathsf{PI}\left(\right)}\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        8. sum-logN/A

          \[\leadsto \frac{\sin \color{blue}{\left(\log \left({\left(e^{\mathsf{PI}\left(\right)}\right)}^{\left(x \cdot tau\right)}\right) + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        9. log-pow-revN/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(x \cdot tau\right) \cdot \log \left(e^{\mathsf{PI}\left(\right)}\right)} + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        10. add-log-expN/A

          \[\leadsto \frac{\sin \left(\left(x \cdot tau\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        11. lift-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot tau\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        12. lift-*.f32N/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(x \cdot tau\right)} \cdot \mathsf{PI}\left(\right) + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        13. associate-*l*N/A

          \[\leadsto \frac{\sin \left(\color{blue}{x \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)} + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        14. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x} + \log \left(e^{\mathsf{PI}\left(\right)}\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        15. add-log-expN/A

          \[\leadsto \frac{\sin \left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x + \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        16. lift-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x + \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        17. lower-fma.f32N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\mathsf{fma}\left(tau \cdot \mathsf{PI}\left(\right), x, \mathsf{PI}\left(\right)\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        18. lower-*.f3293.9

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(\color{blue}{tau \cdot \mathsf{PI}\left(\right)}, x, \mathsf{PI}\left(\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
      7. Applied rewrites93.9%

        \[\leadsto \frac{\sin \color{blue}{\left(\mathsf{fma}\left(tau \cdot \mathsf{PI}\left(\right), x, \mathsf{PI}\left(\right)\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification96.7%

      \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.023000000044703484:\\ \;\;\;\;\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(tau \cdot \mathsf{PI}\left(\right), x, \mathsf{PI}\left(\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\ \end{array} \]
    5. Add Preprocessing

    Alternative 3: 96.9% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ t_3 := \sin t\_2\\ \mathbf{if}\;x \leq 0.03200000151991844:\\ \;\;\;\;\frac{t\_3}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, \mathsf{PI}\left(\right), \mathsf{PI}\left(\right)\right)\right) \cdot t\_3}{t\_1 \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\ \end{array} \end{array} \]
    (FPCore (x tau)
     :precision binary32
     (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)) (t_3 (sin t_2)))
       (if (<= x 0.03200000151991844)
         (* (/ t_3 t_2) (fma (* (* -0.16666666666666666 x) x) (* (PI) (PI)) 1.0))
         (/ (* (sin (fma x (PI) (PI))) t_3) (* t_1 (* (* (- x) (PI)) tau))))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := x \cdot \mathsf{PI}\left(\right)\\
    t_2 := t\_1 \cdot tau\\
    t_3 := \sin t\_2\\
    \mathbf{if}\;x \leq 0.03200000151991844:\\
    \;\;\;\;\frac{t\_3}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, \mathsf{PI}\left(\right), \mathsf{PI}\left(\right)\right)\right) \cdot t\_3}{t\_1 \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if x < 0.0320000015

      1. Initial program 98.4%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
        2. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
        3. lower-fma.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
        4. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        5. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        7. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right)} \cdot x, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        10. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lower-PI.f3298.1

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
      5. Applied rewrites98.1%

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

      if 0.0320000015 < x

      1. Initial program 95.8%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
        2. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        3. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
        4. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. Applied rewrites95.8%

        \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
      5. Applied rewrites94.0%

        \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, \mathsf{PI}\left(\right), \mathsf{PI}\left(\right)\right)\right) \cdot \sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification96.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.03200000151991844:\\ \;\;\;\;\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, \mathsf{PI}\left(\right), \mathsf{PI}\left(\right)\right)\right) \cdot \sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}\\ \end{array} \]
    5. Add Preprocessing

    Alternative 4: 97.1% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ t_2 := t\_1 \cdot tau\\ \mathbf{if}\;x \leq 0.03099999949336052:\\ \;\;\;\;\frac{\sin t\_2}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(-\sin t\_1\right)}{\left(t\_1 \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}\\ \end{array} \end{array} \]
    (FPCore (x tau)
     :precision binary32
     (let* ((t_1 (* x (PI))) (t_2 (* t_1 tau)))
       (if (<= x 0.03099999949336052)
         (*
          (/ (sin t_2) t_2)
          (fma (* (* -0.16666666666666666 x) x) (* (PI) (PI)) 1.0))
         (/
          (* (sin (* (fma x tau 1.0) (PI))) (- (sin t_1)))
          (* (* t_1 (* tau (PI))) x)))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := x \cdot \mathsf{PI}\left(\right)\\
    t_2 := t\_1 \cdot tau\\
    \mathbf{if}\;x \leq 0.03099999949336052:\\
    \;\;\;\;\frac{\sin t\_2}{t\_2} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(-\sin t\_1\right)}{\left(t\_1 \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if x < 0.0309999995

      1. Initial program 98.4%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
        2. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
        3. lower-fma.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
        4. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        5. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        7. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right)} \cdot x, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        10. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lower-PI.f3298.1

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
      5. Applied rewrites98.1%

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

      if 0.0309999995 < x

      1. Initial program 95.8%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
        2. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        3. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
        4. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. Applied rewrites95.8%

        \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
      5. Applied rewrites93.6%

        \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
      6. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
        2. lift-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)} \cdot tau\right)} \]
        4. associate-*l*N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(x \cdot \left(\mathsf{PI}\left(\right) \cdot tau\right)\right)}} \]
        5. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot tau\right) \cdot x\right)}} \]
        6. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\color{blue}{\left(tau \cdot \mathsf{PI}\left(\right)\right)} \cdot x\right)} \]
        7. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}} \]
        8. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}} \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot x} \]
        10. lower-*.f3293.9

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(tau \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot x} \]
      7. Applied rewrites93.9%

        \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification96.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.03099999949336052:\\ \;\;\;\;\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(-\sin \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{\left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot \left(tau \cdot \mathsf{PI}\left(\right)\right)\right) \cdot x}\\ \end{array} \]
    5. Add Preprocessing

    Alternative 5: 97.1% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\ t_2 := x \cdot \mathsf{PI}\left(\right)\\ t_3 := t\_2 \cdot tau\\ \mathbf{if}\;x \leq 0.03099999949336052:\\ \;\;\;\;\frac{\sin t\_3}{t\_3} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, t\_1, 1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin t\_2}{\left(-tau\right) \cdot \left(t\_1 \cdot \left(x \cdot x\right)\right)}\\ \end{array} \end{array} \]
    (FPCore (x tau)
     :precision binary32
     (let* ((t_1 (* (PI) (PI))) (t_2 (* x (PI))) (t_3 (* t_2 tau)))
       (if (<= x 0.03099999949336052)
         (* (/ (sin t_3) t_3) (fma (* (* -0.16666666666666666 x) x) t_1 1.0))
         (/
          (* (sin (* (fma x tau 1.0) (PI))) (sin t_2))
          (* (- tau) (* t_1 (* x x)))))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\
    t_2 := x \cdot \mathsf{PI}\left(\right)\\
    t_3 := t\_2 \cdot tau\\
    \mathbf{if}\;x \leq 0.03099999949336052:\\
    \;\;\;\;\frac{\sin t\_3}{t\_3} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, t\_1, 1\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin t\_2}{\left(-tau\right) \cdot \left(t\_1 \cdot \left(x \cdot x\right)\right)}\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if x < 0.0309999995

      1. Initial program 98.4%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
        2. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
        3. lower-fma.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
        4. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        5. associate-*r*N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        7. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right)} \cdot x, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
        10. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lower-PI.f3298.1

          \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
      5. Applied rewrites98.1%

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

      if 0.0309999995 < x

      1. Initial program 95.8%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
        2. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        3. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
        4. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. Applied rewrites95.8%

        \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
      5. Applied rewrites93.6%

        \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
      6. Taylor expanded in x around 0

        \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{-1 \cdot \left(tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)}} \]
      7. Step-by-step derivation
        1. mul-1-negN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\mathsf{neg}\left(tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)}} \]
        2. distribute-lft-neg-inN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\mathsf{neg}\left(tau\right)\right) \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}} \]
        3. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(\mathsf{neg}\left(tau\right)\right) \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}} \]
        4. lower-neg.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{\left(-tau\right)} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)} \]
        5. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \color{blue}{\left({\mathsf{PI}\left(\right)}^{2} \cdot {x}^{2}\right)}} \]
        6. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \color{blue}{\left({\mathsf{PI}\left(\right)}^{2} \cdot {x}^{2}\right)}} \]
        7. unpow2N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot {x}^{2}\right)} \]
        8. lower-*.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\color{blue}{\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot {x}^{2}\right)} \]
        9. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\left(\color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right)\right) \cdot {x}^{2}\right)} \]
        10. lower-PI.f32N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot {x}^{2}\right)} \]
        11. unpow2N/A

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]
        12. lower-*.f3293.8

          \[\leadsto \frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(-tau\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]
      8. Applied rewrites93.8%

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

    Alternative 6: 97.3% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ \frac{\sin \left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x\right) \cdot \sin t\_1}{t\_1 \cdot \left(t\_1 \cdot tau\right)} \end{array} \end{array} \]
    (FPCore (x tau)
     :precision binary32
     (let* ((t_1 (* x (PI))))
       (/ (* (sin (* (* tau (PI)) x)) (sin t_1)) (* t_1 (* t_1 tau)))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := x \cdot \mathsf{PI}\left(\right)\\
    \frac{\sin \left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x\right) \cdot \sin t\_1}{t\_1 \cdot \left(t\_1 \cdot tau\right)}
    \end{array}
    \end{array}
    
    Derivation
    1. Initial program 97.5%

      \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
      2. lift-/.f32N/A

        \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      3. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. lower-/.f32N/A

        \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
    4. Applied rewrites97.5%

      \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
    5. Applied rewrites81.5%

      \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
    6. Step-by-step derivation
      1. Applied rewrites97.6%

        \[\leadsto \frac{\color{blue}{\sin \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
      2. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        2. lift-*.f32N/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot tau\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        3. associate-*l*N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(-x\right) \cdot \left(\mathsf{PI}\left(\right) \cdot tau\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        4. *-commutativeN/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot tau\right) \cdot \left(-x\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        5. lower-*.f32N/A

          \[\leadsto \frac{\sin \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot tau\right) \cdot \left(-x\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        6. *-commutativeN/A

          \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(-x\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        7. lower-*.f3297.0

          \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot \mathsf{PI}\left(\right)\right)} \cdot \left(-x\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
      3. Applied rewrites97.0%

        \[\leadsto \frac{\sin \color{blue}{\left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot \left(-x\right)\right)} \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
      4. Final simplification97.0%

        \[\leadsto \frac{\sin \left(\left(tau \cdot \mathsf{PI}\left(\right)\right) \cdot x\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
      5. Add Preprocessing

      Alternative 7: 97.0% accurate, 1.0× speedup?

      \[\begin{array}{l} \\ \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(x \cdot x\right)\right)} \end{array} \]
      (FPCore (x tau)
       :precision binary32
       (/
        (* (sin (* (* tau x) (PI))) (sin (* (PI) x)))
        (* tau (* (* (PI) (PI)) (* x x)))))
      \begin{array}{l}
      
      \\
      \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(x \cdot x\right)\right)}
      \end{array}
      
      Derivation
      1. Initial program 97.5%

        \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}} \]
        2. lift-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        3. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
        4. lower-/.f32N/A

          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau}} \]
      4. Applied rewrites97.5%

        \[\leadsto \color{blue}{\frac{\frac{\sin \left(tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)\right)}{\mathsf{PI}\left(\right) \cdot x} \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\mathsf{PI}\left(\right) \cdot x\right)}} \]
      5. Applied rewrites81.5%

        \[\leadsto \color{blue}{\frac{\sin \left(\mathsf{fma}\left(x, tau, 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}} \]
      6. Step-by-step derivation
        1. Applied rewrites97.6%

          \[\leadsto \frac{\color{blue}{\sin \left(\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}}{\left(\left(-x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)} \]
        2. Taylor expanded in x around inf

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

            \[\leadsto \color{blue}{\mathsf{neg}\left(\frac{\sin \left(-1 \cdot \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)}\right)} \]
          2. distribute-neg-frac2N/A

            \[\leadsto \color{blue}{\frac{\sin \left(-1 \cdot \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\mathsf{neg}\left(tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)}} \]
          3. mul-1-negN/A

            \[\leadsto \frac{\sin \left(-1 \cdot \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{\color{blue}{-1 \cdot \left(tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)}} \]
          4. lower-/.f32N/A

            \[\leadsto \color{blue}{\frac{\sin \left(-1 \cdot \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{-1 \cdot \left(tau \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)}} \]
        4. Applied rewrites96.9%

          \[\leadsto \color{blue}{\frac{\sin \left(\left(\left(-tau\right) \cdot x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{\left(-tau\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(x \cdot x\right)\right)}} \]
        5. Final simplification96.9%

          \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot x\right)}{tau \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot \left(x \cdot x\right)\right)} \]
        6. Add Preprocessing

        Alternative 8: 85.8% accurate, 1.6× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\\ \frac{\sin t\_1}{t\_1} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right) \end{array} \end{array} \]
        (FPCore (x tau)
         :precision binary32
         (let* ((t_1 (* (* x (PI)) tau)))
           (*
            (/ (sin t_1) t_1)
            (fma (* (* -0.16666666666666666 x) x) (* (PI) (PI)) 1.0))))
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_1 := \left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\\
        \frac{\sin t\_1}{t\_1} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)
        \end{array}
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
          2. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
          3. lower-fma.f32N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
          4. unpow2N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          5. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          6. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right) \cdot x}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          7. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\left(\frac{-1}{6} \cdot x\right)} \cdot x, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          8. unpow2N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          9. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          10. lower-PI.f32N/A

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
          11. lower-PI.f3280.9

            \[\leadsto \frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
        5. Applied rewrites80.9%

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

        Alternative 9: 85.2% accurate, 1.6× speedup?

        \[\begin{array}{l} \\ \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right) \end{array} \]
        (FPCore (x tau)
         :precision binary32
         (*
          (/ (sin (* (* tau x) (PI))) (* (* x (PI)) tau))
          (fma (* -0.16666666666666666 (* x x)) (* (PI) (PI)) 1.0)))
        \begin{array}{l}
        
        \\
        \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f32N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          2. *-commutativeN/A

            \[\leadsto \frac{\sin \color{blue}{\left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          3. lift-*.f32N/A

            \[\leadsto \frac{\sin \left(tau \cdot \color{blue}{\left(x \cdot \mathsf{PI}\left(\right)\right)}\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          4. associate-*r*N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          5. lower-*.f32N/A

            \[\leadsto \frac{\sin \color{blue}{\left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          6. lower-*.f3297.1

            \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot x\right)} \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        4. Applied rewrites97.1%

          \[\leadsto \frac{\sin \color{blue}{\left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        5. Taylor expanded in x around 0

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

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
          2. associate-*r*N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
          3. lower-fma.f32N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
          4. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\color{blue}{\frac{-1}{6} \cdot {x}^{2}}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          5. unpow2N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          6. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          7. unpow2N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          8. lower-*.f32N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          9. lower-PI.f32N/A

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
          10. lower-PI.f3280.4

            \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \mathsf{PI}\left(\right)\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
        7. Applied rewrites80.4%

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

        Alternative 10: 80.1% accurate, 1.6× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot \mathsf{PI}\left(\right)\\ \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \frac{\sin t\_1}{t\_1} \end{array} \end{array} \]
        (FPCore (x tau)
         :precision binary32
         (let* ((t_1 (* x (PI))))
           (*
            (fma (* (* -0.16666666666666666 x) x) (* (* (* (PI) (PI)) tau) tau) 1.0)
            (/ (sin t_1) t_1))))
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_1 := x \cdot \mathsf{PI}\left(\right)\\
        \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \frac{\sin t\_1}{t\_1}
        \end{array}
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \color{blue}{\left(\frac{-1}{6} \cdot \left({tau}^{2} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right) + 1\right)} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          2. *-commutativeN/A

            \[\leadsto \left(\frac{-1}{6} \cdot \color{blue}{\left(\left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) \cdot {tau}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          3. associate-*r*N/A

            \[\leadsto \left(\color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right) \cdot {tau}^{2}} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          4. associate-*r*N/A

            \[\leadsto \left(\color{blue}{\left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}\right)} \cdot {tau}^{2} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          5. associate-*l*N/A

            \[\leadsto \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \left({\mathsf{PI}\left(\right)}^{2} \cdot {tau}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \color{blue}{\left({tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          7. lower-fma.f32N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}, 1\right)} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        5. Applied rewrites75.1%

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

        Alternative 11: 80.1% accurate, 4.4× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_1 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\ \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(t\_1 \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), t\_1, 1\right) \end{array} \end{array} \]
        (FPCore (x tau)
         :precision binary32
         (let* ((t_1 (* (PI) (PI))))
           (*
            (fma (* (* -0.16666666666666666 x) x) (* (* t_1 tau) tau) 1.0)
            (fma (* -0.16666666666666666 (* x x)) t_1 1.0))))
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_1 := \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\\
        \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(t\_1 \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), t\_1, 1\right)
        \end{array}
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \color{blue}{\left(\frac{-1}{6} \cdot \left({tau}^{2} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right) + 1\right)} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          2. *-commutativeN/A

            \[\leadsto \left(\frac{-1}{6} \cdot \color{blue}{\left(\left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) \cdot {tau}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          3. associate-*r*N/A

            \[\leadsto \left(\color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right) \cdot {tau}^{2}} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          4. associate-*r*N/A

            \[\leadsto \left(\color{blue}{\left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}\right)} \cdot {tau}^{2} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          5. associate-*l*N/A

            \[\leadsto \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \left({\mathsf{PI}\left(\right)}^{2} \cdot {tau}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          6. *-commutativeN/A

            \[\leadsto \left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \color{blue}{\left({tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)} + 1\right) \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
          7. lower-fma.f32N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}, 1\right)} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        5. Applied rewrites75.1%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right)} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        6. Taylor expanded in x around 0

          \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \color{blue}{\left(1 + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right)\right)} \]
        7. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \color{blue}{\left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1\right)} \]
          2. associate-*r*N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \left(\color{blue}{\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\mathsf{PI}\left(\right)}^{2}} + 1\right) \]
          3. lower-fma.f32N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot {x}^{2}, {\mathsf{PI}\left(\right)}^{2}, 1\right)} \]
          4. lower-*.f32N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\color{blue}{\frac{-1}{6} \cdot {x}^{2}}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          5. unpow2N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          6. lower-*.f32N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \color{blue}{\left(x \cdot x\right)}, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          7. unpow2N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          8. lower-*.f32N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)}, 1\right) \]
          9. lower-PI.f32N/A

            \[\leadsto \mathsf{fma}\left(\left(\frac{-1}{6} \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(\frac{-1}{6} \cdot \left(x \cdot x\right), \color{blue}{\mathsf{PI}\left(\right)} \cdot \mathsf{PI}\left(\right), 1\right) \]
          10. lower-PI.f3274.9

            \[\leadsto \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}, 1\right) \]
        8. Applied rewrites74.9%

          \[\leadsto \mathsf{fma}\left(\left(-0.16666666666666666 \cdot x\right) \cdot x, \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right) \cdot tau, 1\right) \cdot \color{blue}{\mathsf{fma}\left(-0.16666666666666666 \cdot \left(x \cdot x\right), \mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right), 1\right)} \]
        9. Add Preprocessing

        Alternative 12: 79.4% accurate, 7.8× speedup?

        \[\begin{array}{l} \\ \mathsf{fma}\left(\mathsf{fma}\left(tau, tau, 1\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -0.16666666666666666\right), x \cdot x, 1\right) \end{array} \]
        (FPCore (x tau)
         :precision binary32
         (fma
          (* (fma tau tau 1.0) (* (* (PI) (PI)) -0.16666666666666666))
          (* x x)
          1.0))
        \begin{array}{l}
        
        \\
        \mathsf{fma}\left(\mathsf{fma}\left(tau, tau, 1\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -0.16666666666666666\right), x \cdot x, 1\right)
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

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

            \[\leadsto \color{blue}{{x}^{2} \cdot \left(\frac{-1}{6} \cdot \left({tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \frac{-1}{6} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + 1} \]
          2. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\frac{-1}{6} \cdot \left({tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \frac{-1}{6} \cdot {\mathsf{PI}\left(\right)}^{2}\right) \cdot {x}^{2}} + 1 \]
          3. lower-fma.f32N/A

            \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{-1}{6} \cdot \left({tau}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \frac{-1}{6} \cdot {\mathsf{PI}\left(\right)}^{2}, {x}^{2}, 1\right)} \]
        5. Applied rewrites73.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(tau, tau, 1\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -0.16666666666666666\right), x \cdot x, 1\right)} \]
        6. Final simplification73.9%

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(tau, tau, 1\right) \cdot \left(\left(\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right)\right) \cdot -0.16666666666666666\right), x \cdot x, 1\right) \]
        7. Add Preprocessing

        Alternative 13: 64.5% accurate, 258.0× speedup?

        \[\begin{array}{l} \\ 1 \end{array} \]
        (FPCore (x tau) :precision binary32 1.0)
        float code(float x, float tau) {
        	return 1.0f;
        }
        
        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(4) function code(x, tau)
        use fmin_fmax_functions
            real(4), intent (in) :: x
            real(4), intent (in) :: tau
            code = 1.0e0
        end function
        
        function code(x, tau)
        	return Float32(1.0)
        end
        
        function tmp = code(x, tau)
        	tmp = single(1.0);
        end
        
        \begin{array}{l}
        
        \\
        1
        \end{array}
        
        Derivation
        1. Initial program 97.5%

          \[\frac{\sin \left(\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau\right)}{\left(x \cdot \mathsf{PI}\left(\right)\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \mathsf{PI}\left(\right)\right)}{x \cdot \mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \color{blue}{1} \]
        4. Step-by-step derivation
          1. Applied rewrites59.8%

            \[\leadsto \color{blue}{1} \]
          2. Final simplification59.8%

            \[\leadsto 1 \]
          3. Add Preprocessing

          Reproduce

          ?
          herbie shell --seed 2024364 
          (FPCore (x tau)
            :name "Lanczos kernel"
            :precision binary32
            :pre (and (and (<= 1e-5 x) (<= x 1.0)) (and (<= 1.0 tau) (<= tau 5.0)))
            (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))))