Lanczos kernel

Percentage Accurate: 98.0% → 98.0%
Time: 13.5s
Alternatives: 16
Speedup: 1.0×

Specification

?
\[\left(10^{-5} \leq x \land x \leq 1\right) \land \left(1 \leq tau \land tau \leq 5\right)\]
\[\begin{array}{l} t_1 := \left(x \cdot \pi\right) \cdot tau\\ \frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \end{array} \]
(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* x PI) tau)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))
float code(float x, float tau) {
	float t_1 = (x * ((float) M_PI)) * tau;
	return (sinf(t_1) / t_1) * (sinf((x * ((float) M_PI))) / (x * ((float) M_PI)));
}
function code(x, tau)
	t_1 = Float32(Float32(x * Float32(pi)) * tau)
	return Float32(Float32(sin(t_1) / t_1) * Float32(sin(Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
end
function tmp = code(x, tau)
	t_1 = (x * single(pi)) * tau;
	tmp = (sin(t_1) / t_1) * (sin((x * single(pi))) / (x * single(pi)));
end
\begin{array}{l}
t_1 := \left(x \cdot \pi\right) \cdot tau\\
\frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}
\end{array}

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 16 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} t_1 := \left(x \cdot \pi\right) \cdot tau\\ \frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \end{array} \]
(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* x PI) tau)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))
float code(float x, float tau) {
	float t_1 = (x * ((float) M_PI)) * tau;
	return (sinf(t_1) / t_1) * (sinf((x * ((float) M_PI))) / (x * ((float) M_PI)));
}
function code(x, tau)
	t_1 = Float32(Float32(x * Float32(pi)) * tau)
	return Float32(Float32(sin(t_1) / t_1) * Float32(sin(Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
end
function tmp = code(x, tau)
	t_1 = (x * single(pi)) * tau;
	tmp = (sin(t_1) / t_1) * (sin((x * single(pi))) / (x * single(pi)));
end
\begin{array}{l}
t_1 := \left(x \cdot \pi\right) \cdot tau\\
\frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}
\end{array}

Alternative 1: 98.0% accurate, 1.0× speedup?

\[\begin{array}{l} t_1 := \left(tau \cdot x\right) \cdot \pi\\ \frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \end{array} \]
(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* tau x) PI)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))
float code(float x, float tau) {
	float t_1 = (tau * x) * ((float) M_PI);
	return (sinf(t_1) / t_1) * (sinf((x * ((float) M_PI))) / (x * ((float) M_PI)));
}
function code(x, tau)
	t_1 = Float32(Float32(tau * x) * Float32(pi))
	return Float32(Float32(sin(t_1) / t_1) * Float32(sin(Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
end
function tmp = code(x, tau)
	t_1 = (tau * x) * single(pi);
	tmp = (sin(t_1) / t_1) * (sin((x * single(pi))) / (x * single(pi)));
end
\begin{array}{l}
t_1 := \left(tau \cdot x\right) \cdot \pi\\
\frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}
\end{array}
Derivation
  1. Initial program 98.0%

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

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

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

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

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

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

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

      \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot x\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    8. lower-*.f3297.4%

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

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

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

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

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

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

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

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

      \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right)}{\color{blue}{\left(tau \cdot x\right)} \cdot \pi} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    8. lower-*.f3298.0%

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

    \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right)}{\color{blue}{\left(tau \cdot x\right) \cdot \pi}} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
  6. Add Preprocessing

Alternative 2: 97.8% accurate, 1.0× speedup?

\[\begin{array}{l} t_1 := \left(-tau\right) \cdot \left(x \cdot \pi\right)\\ \frac{\sin t\_1 \cdot \sin \left(x \cdot \pi\right)}{t\_1 \cdot \left(x \cdot \pi\right)} \end{array} \]
(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (- tau) (* x PI))))
  (/ (* (sin t_1) (sin (* x PI))) (* t_1 (* x PI)))))
float code(float x, float tau) {
	float t_1 = -tau * (x * ((float) M_PI));
	return (sinf(t_1) * sinf((x * ((float) M_PI)))) / (t_1 * (x * ((float) M_PI)));
}
function code(x, tau)
	t_1 = Float32(Float32(-tau) * Float32(x * Float32(pi)))
	return Float32(Float32(sin(t_1) * sin(Float32(x * Float32(pi)))) / Float32(t_1 * Float32(x * Float32(pi))))
end
function tmp = code(x, tau)
	t_1 = -tau * (x * single(pi));
	tmp = (sin(t_1) * sin((x * single(pi)))) / (t_1 * (x * single(pi)));
end
\begin{array}{l}
t_1 := \left(-tau\right) \cdot \left(x \cdot \pi\right)\\
\frac{\sin t\_1 \cdot \sin \left(x \cdot \pi\right)}{t\_1 \cdot \left(x \cdot \pi\right)}
\end{array}
Derivation
  1. Initial program 98.0%

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

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

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

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

      \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}}{\left(x \cdot \pi\right) \cdot tau}} \]
  3. Applied rewrites97.8%

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

    \[\leadsto \color{blue}{\frac{\sin \left(\left(-tau\right) \cdot \left(x \cdot \pi\right)\right) \cdot \sin \left(x \cdot \pi\right)}{\left(\left(-tau\right) \cdot \left(x \cdot \pi\right)\right) \cdot \left(x \cdot \pi\right)}} \]
  5. Add Preprocessing

Alternative 3: 97.2% accurate, 1.0× speedup?

\[\frac{\sin \left(tau \cdot \left(\pi \cdot x\right)\right)}{\left(\left(\pi \cdot x\right) \cdot x\right) \cdot \left(tau \cdot \pi\right)} \cdot \sin \left(\pi \cdot x\right) \]
(FPCore (x tau)
  :precision binary32
  (*
 (/ (sin (* tau (* PI x))) (* (* (* PI x) x) (* tau PI)))
 (sin (* PI x))))
float code(float x, float tau) {
	return (sinf((tau * (((float) M_PI) * x))) / (((((float) M_PI) * x) * x) * (tau * ((float) M_PI)))) * sinf((((float) M_PI) * x));
}
function code(x, tau)
	return Float32(Float32(sin(Float32(tau * Float32(Float32(pi) * x))) / Float32(Float32(Float32(Float32(pi) * x) * x) * Float32(tau * Float32(pi)))) * sin(Float32(Float32(pi) * x)))
end
function tmp = code(x, tau)
	tmp = (sin((tau * (single(pi) * x))) / (((single(pi) * x) * x) * (tau * single(pi)))) * sin((single(pi) * x));
end
\frac{\sin \left(tau \cdot \left(\pi \cdot x\right)\right)}{\left(\left(\pi \cdot x\right) \cdot x\right) \cdot \left(tau \cdot \pi\right)} \cdot \sin \left(\pi \cdot x\right)
Derivation
  1. Initial program 98.0%

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

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

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

      \[\leadsto \color{blue}{\frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}} \cdot \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \]
    4. mult-flipN/A

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

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

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

      \[\leadsto \color{blue}{\left(\frac{1}{x \cdot \pi} \cdot \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau}\right) \cdot \sin \left(x \cdot \pi\right)} \]
  3. Applied rewrites97.2%

    \[\leadsto \color{blue}{\frac{\sin \left(tau \cdot \left(\pi \cdot x\right)\right)}{\left(\left(\pi \cdot x\right) \cdot x\right) \cdot \left(tau \cdot \pi\right)} \cdot \sin \left(\pi \cdot x\right)} \]
  4. Add Preprocessing

Alternative 4: 97.0% accurate, 1.0× speedup?

\[\sin \left(\pi \cdot \left(x \cdot tau\right)\right) \cdot \frac{\sin \left(\pi \cdot x\right)}{\left(\left(\pi \cdot tau\right) \cdot \pi\right) \cdot \left(x \cdot x\right)} \]
(FPCore (x tau)
  :precision binary32
  (*
 (sin (* PI (* x tau)))
 (/ (sin (* PI x)) (* (* (* PI tau) PI) (* x x)))))
float code(float x, float tau) {
	return sinf((((float) M_PI) * (x * tau))) * (sinf((((float) M_PI) * x)) / (((((float) M_PI) * tau) * ((float) M_PI)) * (x * x)));
}
function code(x, tau)
	return Float32(sin(Float32(Float32(pi) * Float32(x * tau))) * Float32(sin(Float32(Float32(pi) * x)) / Float32(Float32(Float32(Float32(pi) * tau) * Float32(pi)) * Float32(x * x))))
end
function tmp = code(x, tau)
	tmp = sin((single(pi) * (x * tau))) * (sin((single(pi) * x)) / (((single(pi) * tau) * single(pi)) * (x * x)));
end
\sin \left(\pi \cdot \left(x \cdot tau\right)\right) \cdot \frac{\sin \left(\pi \cdot x\right)}{\left(\left(\pi \cdot tau\right) \cdot \pi\right) \cdot \left(x \cdot x\right)}
Derivation
  1. Initial program 98.0%

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

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

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

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

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

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

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

      \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot x\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    8. lower-*.f3297.4%

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

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

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

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

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

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

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

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

      \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right)}{\color{blue}{\left(tau \cdot x\right)} \cdot \pi} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    8. lower-*.f3298.0%

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

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

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

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

      \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right)}{\left(tau \cdot x\right) \cdot \pi} \cdot \color{blue}{\frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}} \]
    4. frac-timesN/A

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

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

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

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

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

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

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

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

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

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

      \[\leadsto \sin \left(\pi \cdot \left(x \cdot tau\right)\right) \cdot \frac{\sin \left(x \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot \color{blue}{\left(\left(tau \cdot x\right) \cdot \pi\right)}} \]
  7. Applied rewrites97.0%

    \[\leadsto \color{blue}{\sin \left(\pi \cdot \left(x \cdot tau\right)\right) \cdot \frac{\sin \left(\pi \cdot x\right)}{\left(\left(\pi \cdot tau\right) \cdot \pi\right) \cdot \left(x \cdot x\right)}} \]
  8. Add Preprocessing

Alternative 5: 85.1% accurate, 1.2× speedup?

\[\begin{array}{l} t_1 := tau \cdot \left(x \cdot \pi\right)\\ \frac{\sin t\_1}{t\_1} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \end{array} \]
(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* tau (* x PI))))
  (*
   (/ (sin t_1) t_1)
   (/
    (*
     (+
      1.0
      (/
       (* (* x (* (* x x) -0.16666666666666666)) (* (* PI PI) PI))
       (* x PI)))
     (* x PI))
    (* x PI)))))
float code(float x, float tau) {
	float t_1 = tau * (x * ((float) M_PI));
	return (sinf(t_1) / t_1) * (((1.0f + (((x * ((x * x) * -0.16666666666666666f)) * ((((float) M_PI) * ((float) M_PI)) * ((float) M_PI))) / (x * ((float) M_PI)))) * (x * ((float) M_PI))) / (x * ((float) M_PI)));
}
function code(x, tau)
	t_1 = Float32(tau * Float32(x * Float32(pi)))
	return Float32(Float32(sin(t_1) / t_1) * Float32(Float32(Float32(Float32(1.0) + Float32(Float32(Float32(x * Float32(Float32(x * x) * Float32(-0.16666666666666666))) * Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi))) / Float32(x * Float32(pi)))) * Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
end
function tmp = code(x, tau)
	t_1 = tau * (x * single(pi));
	tmp = (sin(t_1) / t_1) * (((single(1.0) + (((x * ((x * x) * single(-0.16666666666666666))) * ((single(pi) * single(pi)) * single(pi))) / (x * single(pi)))) * (x * single(pi))) / (x * single(pi)));
end
\begin{array}{l}
t_1 := tau \cdot \left(x \cdot \pi\right)\\
\frac{\sin t\_1}{t\_1} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi}
\end{array}
Derivation
  1. Initial program 98.0%

    \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
  2. Taylor expanded in x around 0

    \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
  3. Step-by-step derivation
    1. Applied rewrites64.4%

      \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    2. Taylor expanded in x around 0

      \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
    3. Step-by-step derivation
      1. lower-*.f32N/A

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

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

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

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

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

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

        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
      8. lower-PI.f3264.6%

        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
    4. Applied rewrites64.6%

      \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
    5. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto 1 \cdot \frac{x \cdot \color{blue}{\left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
      2. lift-+.f32N/A

        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \color{blue}{\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)}\right)}{x \cdot \pi} \]
      3. distribute-lft-inN/A

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

        \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
      5. lift-*.f32N/A

        \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
      6. sum-to-multN/A

        \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
      7. lower-unsound-*.f32N/A

        \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
    6. Applied rewrites64.6%

      \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \color{blue}{\left(x \cdot \pi\right)}}{x \cdot \pi} \]
    7. Taylor expanded in x around inf

      \[\leadsto \color{blue}{\frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)}} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
    8. Step-by-step derivation
      1. lower-/.f32N/A

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

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

        \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
      4. lower-*.f32N/A

        \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)\right)}{tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
      5. lower-PI.f32N/A

        \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \mathsf{PI}\left(\right)\right)} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
      6. lower-*.f32N/A

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

        \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
      8. lower-PI.f3285.1%

        \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
    9. Applied rewrites85.1%

      \[\leadsto \color{blue}{\frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)}} \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
    10. Add Preprocessing

    Alternative 6: 71.1% accurate, 1.6× speedup?

    \[\begin{array}{l} t_1 := tau \cdot \left(x \cdot \pi\right)\\ \frac{\sin t\_1}{t\_1} \cdot \frac{x \cdot \pi}{x \cdot \pi} \end{array} \]
    (FPCore (x tau)
      :precision binary32
      (let* ((t_1 (* tau (* x PI))))
      (* (/ (sin t_1) t_1) (/ (* x PI) (* x PI)))))
    float code(float x, float tau) {
    	float t_1 = tau * (x * ((float) M_PI));
    	return (sinf(t_1) / t_1) * ((x * ((float) M_PI)) / (x * ((float) M_PI)));
    }
    
    function code(x, tau)
    	t_1 = Float32(tau * Float32(x * Float32(pi)))
    	return Float32(Float32(sin(t_1) / t_1) * Float32(Float32(x * Float32(pi)) / Float32(x * Float32(pi))))
    end
    
    function tmp = code(x, tau)
    	t_1 = tau * (x * single(pi));
    	tmp = (sin(t_1) / t_1) * ((x * single(pi)) / (x * single(pi)));
    end
    
    \begin{array}{l}
    t_1 := tau \cdot \left(x \cdot \pi\right)\\
    \frac{\sin t\_1}{t\_1} \cdot \frac{x \cdot \pi}{x \cdot \pi}
    \end{array}
    
    Derivation
    1. Initial program 98.0%

      \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    2. Taylor expanded in x around 0

      \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
    3. Step-by-step derivation
      1. Applied rewrites64.4%

        \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
      2. Taylor expanded in x around 0

        \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
      3. Step-by-step derivation
        1. lower-*.f32N/A

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

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

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

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

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

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

          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
        8. lower-PI.f3264.6%

          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
      4. Applied rewrites64.6%

        \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
      5. Taylor expanded in x around 0

        \[\leadsto 1 \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      6. Step-by-step derivation
        1. lower-PI.f3263.6%

          \[\leadsto 1 \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      7. Applied rewrites63.6%

        \[\leadsto 1 \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      8. Taylor expanded in x around inf

        \[\leadsto \color{blue}{\frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)}} \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      9. Step-by-step derivation
        1. lower-/.f32N/A

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

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

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

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

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

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

          \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
        8. lower-PI.f3271.1%

          \[\leadsto \frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)} \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      10. Applied rewrites71.1%

        \[\leadsto \color{blue}{\frac{\sin \left(tau \cdot \left(x \cdot \pi\right)\right)}{tau \cdot \left(x \cdot \pi\right)}} \cdot \frac{x \cdot \pi}{x \cdot \pi} \]
      11. Add Preprocessing

      Alternative 7: 71.1% accurate, 1.9× speedup?

      \[\begin{array}{l} t_1 := \pi \cdot \left(x \cdot tau\right)\\ \frac{1 \cdot \sin t\_1}{t\_1} \end{array} \]
      (FPCore (x tau)
        :precision binary32
        (let* ((t_1 (* PI (* x tau)))) (/ (* 1.0 (sin t_1)) t_1)))
      float code(float x, float tau) {
      	float t_1 = ((float) M_PI) * (x * tau);
      	return (1.0f * sinf(t_1)) / t_1;
      }
      
      function code(x, tau)
      	t_1 = Float32(Float32(pi) * Float32(x * tau))
      	return Float32(Float32(Float32(1.0) * sin(t_1)) / t_1)
      end
      
      function tmp = code(x, tau)
      	t_1 = single(pi) * (x * tau);
      	tmp = (single(1.0) * sin(t_1)) / t_1;
      end
      
      \begin{array}{l}
      t_1 := \pi \cdot \left(x \cdot tau\right)\\
      \frac{1 \cdot \sin t\_1}{t\_1}
      \end{array}
      
      Derivation
      1. Initial program 98.0%

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

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

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

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

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

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

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

          \[\leadsto \frac{\sin \left(\color{blue}{\left(tau \cdot x\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
        8. lower-*.f3297.4%

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

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

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

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

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

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

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

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

          \[\leadsto \frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right)}{\color{blue}{\left(tau \cdot x\right)} \cdot \pi} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
        8. lower-*.f3298.0%

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

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

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

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

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

          \[\leadsto \color{blue}{\frac{\sin \left(\left(tau \cdot x\right) \cdot \pi\right) \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}}{\left(tau \cdot x\right) \cdot \pi}} \]
      7. Applied rewrites97.9%

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

        \[\leadsto \frac{\color{blue}{1} \cdot \sin \left(\pi \cdot \left(x \cdot tau\right)\right)}{\pi \cdot \left(x \cdot tau\right)} \]
      9. Step-by-step derivation
        1. Applied rewrites71.1%

          \[\leadsto \frac{\color{blue}{1} \cdot \sin \left(\pi \cdot \left(x \cdot tau\right)\right)}{\pi \cdot \left(x \cdot tau\right)} \]
        2. Add Preprocessing

        Alternative 8: 64.6% accurate, 2.8× speedup?

        \[1 \cdot \frac{\frac{1}{\frac{x \cdot \pi}{x \cdot \left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right)}} \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
        (FPCore (x tau)
          :precision binary32
          (*
         1.0
         (/
          (*
           (/
            1.0
            (/
             (* x PI)
             (*
              x
              (- PI (* (* 0.16666666666666666 (* x x)) (* (* PI PI) PI))))))
           (* x PI))
          (* x PI))))
        float code(float x, float tau) {
        	return 1.0f * (((1.0f / ((x * ((float) M_PI)) / (x * (((float) M_PI) - ((0.16666666666666666f * (x * x)) * ((((float) M_PI) * ((float) M_PI)) * ((float) M_PI))))))) * (x * ((float) M_PI))) / (x * ((float) M_PI)));
        }
        
        function code(x, tau)
        	return Float32(Float32(1.0) * Float32(Float32(Float32(Float32(1.0) / Float32(Float32(x * Float32(pi)) / Float32(x * Float32(Float32(pi) - Float32(Float32(Float32(0.16666666666666666) * Float32(x * x)) * Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi))))))) * Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
        end
        
        function tmp = code(x, tau)
        	tmp = single(1.0) * (((single(1.0) / ((x * single(pi)) / (x * (single(pi) - ((single(0.16666666666666666) * (x * x)) * ((single(pi) * single(pi)) * single(pi))))))) * (x * single(pi))) / (x * single(pi)));
        end
        
        1 \cdot \frac{\frac{1}{\frac{x \cdot \pi}{x \cdot \left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right)}} \cdot \left(x \cdot \pi\right)}{x \cdot \pi}
        
        Derivation
        1. Initial program 98.0%

          \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
        2. Taylor expanded in x around 0

          \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
        3. Step-by-step derivation
          1. Applied rewrites64.4%

            \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
          2. Taylor expanded in x around 0

            \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
          3. Step-by-step derivation
            1. lower-*.f32N/A

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

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

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

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

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

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

              \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
            8. lower-PI.f3264.6%

              \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
          4. Applied rewrites64.6%

            \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
          5. Step-by-step derivation
            1. lift-*.f32N/A

              \[\leadsto 1 \cdot \frac{x \cdot \color{blue}{\left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
            2. lift-+.f32N/A

              \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \color{blue}{\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)}\right)}{x \cdot \pi} \]
            3. distribute-lft-inN/A

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

              \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
            5. lift-*.f32N/A

              \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
            6. sum-to-multN/A

              \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
            7. lower-unsound-*.f32N/A

              \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
          6. Applied rewrites64.6%

            \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \color{blue}{\left(x \cdot \pi\right)}}{x \cdot \pi} \]
          7. Applied rewrites64.6%

            \[\leadsto 1 \cdot \frac{\frac{1}{\frac{x \cdot \pi}{x \cdot \left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right)}} \cdot \left(\color{blue}{x} \cdot \pi\right)}{x \cdot \pi} \]
          8. Add Preprocessing

          Alternative 9: 64.6% accurate, 3.6× speedup?

          \[1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(-0.16666666666666666 \cdot x\right) \cdot x\right) \cdot \frac{\pi \cdot \pi}{x}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
          (FPCore (x tau)
            :precision binary32
            (*
           1.0
           (/
            (*
             (+ 1.0 (* x (* (* (* -0.16666666666666666 x) x) (/ (* PI PI) x))))
             (* x PI))
            (* x PI))))
          float code(float x, float tau) {
          	return 1.0f * (((1.0f + (x * (((-0.16666666666666666f * x) * x) * ((((float) M_PI) * ((float) M_PI)) / x)))) * (x * ((float) M_PI))) / (x * ((float) M_PI)));
          }
          
          function code(x, tau)
          	return Float32(Float32(1.0) * Float32(Float32(Float32(Float32(1.0) + Float32(x * Float32(Float32(Float32(Float32(-0.16666666666666666) * x) * x) * Float32(Float32(Float32(pi) * Float32(pi)) / x)))) * Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
          end
          
          function tmp = code(x, tau)
          	tmp = single(1.0) * (((single(1.0) + (x * (((single(-0.16666666666666666) * x) * x) * ((single(pi) * single(pi)) / x)))) * (x * single(pi))) / (x * single(pi)));
          end
          
          1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(-0.16666666666666666 \cdot x\right) \cdot x\right) \cdot \frac{\pi \cdot \pi}{x}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi}
          
          Derivation
          1. Initial program 98.0%

            \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
          2. Taylor expanded in x around 0

            \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
          3. Step-by-step derivation
            1. Applied rewrites64.4%

              \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
            2. Taylor expanded in x around 0

              \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
            3. Step-by-step derivation
              1. lower-*.f32N/A

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

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

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

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

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

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

                \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
              8. lower-PI.f3264.6%

                \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
            4. Applied rewrites64.6%

              \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
            5. Step-by-step derivation
              1. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{x \cdot \color{blue}{\left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
              2. lift-+.f32N/A

                \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \color{blue}{\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)}\right)}{x \cdot \pi} \]
              3. distribute-lft-inN/A

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

                \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
              5. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
              6. sum-to-multN/A

                \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
              7. lower-unsound-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
            6. Applied rewrites64.6%

              \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \color{blue}{\left(x \cdot \pi\right)}}{x \cdot \pi} \]
            7. Step-by-step derivation
              1. lift-/.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              2. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              3. associate-/l*N/A

                \[\leadsto 1 \cdot \frac{\left(1 + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              4. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              5. associate-*l*N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              6. lower-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              7. lower-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              8. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              9. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              10. associate-*l*N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(x \cdot \left(x \cdot \frac{-1}{6}\right)\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              11. *-commutativeN/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot \frac{-1}{6}\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              12. lower-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(x \cdot \frac{-1}{6}\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              13. *-commutativeN/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(\frac{-1}{6} \cdot x\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              14. lower-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(\frac{-1}{6} \cdot x\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              15. lift-*.f32N/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(\frac{-1}{6} \cdot x\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{x \cdot \pi}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
              16. *-commutativeN/A

                \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(\frac{-1}{6} \cdot x\right) \cdot x\right) \cdot \frac{\left(\pi \cdot \pi\right) \cdot \pi}{\pi \cdot x}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
            8. Applied rewrites64.6%

              \[\leadsto 1 \cdot \frac{\left(1 + x \cdot \left(\left(\left(-0.16666666666666666 \cdot x\right) \cdot x\right) \cdot \frac{\pi \cdot \pi}{x}\right)\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
            9. Add Preprocessing

            Alternative 10: 64.6% accurate, 3.9× speedup?

            \[\frac{1}{\frac{x \cdot \pi}{\left(\left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right) \cdot x\right) \cdot 1}} \]
            (FPCore (x tau)
              :precision binary32
              (/
             1.0
             (/
              (* x PI)
              (*
               (* (- PI (* (* 0.16666666666666666 (* x x)) (* (* PI PI) PI))) x)
               1.0))))
            float code(float x, float tau) {
            	return 1.0f / ((x * ((float) M_PI)) / (((((float) M_PI) - ((0.16666666666666666f * (x * x)) * ((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)))) * x) * 1.0f));
            }
            
            function code(x, tau)
            	return Float32(Float32(1.0) / Float32(Float32(x * Float32(pi)) / Float32(Float32(Float32(Float32(pi) - Float32(Float32(Float32(0.16666666666666666) * Float32(x * x)) * Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)))) * x) * Float32(1.0))))
            end
            
            function tmp = code(x, tau)
            	tmp = single(1.0) / ((x * single(pi)) / (((single(pi) - ((single(0.16666666666666666) * (x * x)) * ((single(pi) * single(pi)) * single(pi)))) * x) * single(1.0)));
            end
            
            \frac{1}{\frac{x \cdot \pi}{\left(\left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right) \cdot x\right) \cdot 1}}
            
            Derivation
            1. Initial program 98.0%

              \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
            2. Taylor expanded in x around 0

              \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
            3. Step-by-step derivation
              1. Applied rewrites64.4%

                \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
              2. Taylor expanded in x around 0

                \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
              3. Step-by-step derivation
                1. lower-*.f32N/A

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

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

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

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

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

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

                  \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
                8. lower-PI.f3264.6%

                  \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
              4. Applied rewrites64.6%

                \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
              5. Step-by-step derivation
                1. lift-*.f32N/A

                  \[\leadsto \color{blue}{1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi}} \]
                2. lift-/.f32N/A

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

                  \[\leadsto \color{blue}{\frac{1 \cdot \left(x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)\right)}{x \cdot \pi}} \]
                4. lift-*.f32N/A

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

                  \[\leadsto \frac{1 \cdot \left(x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)\right)}{\color{blue}{\pi \cdot x}} \]
                6. lift-*.f32N/A

                  \[\leadsto \frac{1 \cdot \left(x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)\right)}{\color{blue}{\pi \cdot x}} \]
                7. div-flipN/A

                  \[\leadsto \color{blue}{\frac{1}{\frac{\pi \cdot x}{1 \cdot \left(x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)\right)}}} \]
              6. Applied rewrites64.6%

                \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot \pi}{\left(\left(\pi - \left(0.16666666666666666 \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)\right) \cdot x\right) \cdot 1}}} \]
              7. Add Preprocessing

              Alternative 11: 64.6% accurate, 4.3× speedup?

              \[1 \cdot \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right) + x \cdot \pi}{x \cdot \pi} \]
              (FPCore (x tau)
                :precision binary32
                (*
               1.0
               (/
                (+
                 (* (* x (* (* x x) -0.16666666666666666)) (* (* PI PI) PI))
                 (* x PI))
                (* x PI))))
              float code(float x, float tau) {
              	return 1.0f * ((((x * ((x * x) * -0.16666666666666666f)) * ((((float) M_PI) * ((float) M_PI)) * ((float) M_PI))) + (x * ((float) M_PI))) / (x * ((float) M_PI)));
              }
              
              function code(x, tau)
              	return Float32(Float32(1.0) * Float32(Float32(Float32(Float32(x * Float32(Float32(x * x) * Float32(-0.16666666666666666))) * Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi))) + Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
              end
              
              function tmp = code(x, tau)
              	tmp = single(1.0) * ((((x * ((x * x) * single(-0.16666666666666666))) * ((single(pi) * single(pi)) * single(pi))) + (x * single(pi))) / (x * single(pi)));
              end
              
              1 \cdot \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right) + x \cdot \pi}{x \cdot \pi}
              
              Derivation
              1. Initial program 98.0%

                \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
              2. Taylor expanded in x around 0

                \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
              3. Step-by-step derivation
                1. Applied rewrites64.4%

                  \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                2. Taylor expanded in x around 0

                  \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                3. Step-by-step derivation
                  1. lower-*.f32N/A

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

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

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

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

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

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

                    \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
                  8. lower-PI.f3264.6%

                    \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                4. Applied rewrites64.6%

                  \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                5. Step-by-step derivation
                  1. lift-*.f32N/A

                    \[\leadsto 1 \cdot \frac{x \cdot \color{blue}{\left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                  2. lift-+.f32N/A

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

                    \[\leadsto 1 \cdot \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right) + \color{blue}{\pi}\right)}{x \cdot \pi} \]
                  4. distribute-lft-inN/A

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

                    \[\leadsto 1 \cdot \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right) + \pi \cdot \color{blue}{x}}{x \cdot \pi} \]
                  6. lift-*.f32N/A

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

                    \[\leadsto 1 \cdot \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right) + \color{blue}{\pi \cdot x}}{x \cdot \pi} \]
                6. Applied rewrites64.6%

                  \[\leadsto 1 \cdot \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right) + \color{blue}{x \cdot \pi}}{x \cdot \pi} \]
                7. Add Preprocessing

                Alternative 12: 64.6% accurate, 4.7× speedup?

                \[1 \cdot \frac{\pi \cdot \left(x + \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(-0.16666666666666666 \cdot \left(\pi \cdot \pi\right)\right)\right)}{x \cdot \pi} \]
                (FPCore (x tau)
                  :precision binary32
                  (*
                 1.0
                 (/
                  (* PI (+ x (* (* (* x x) x) (* -0.16666666666666666 (* PI PI)))))
                  (* x PI))))
                float code(float x, float tau) {
                	return 1.0f * ((((float) M_PI) * (x + (((x * x) * x) * (-0.16666666666666666f * (((float) M_PI) * ((float) M_PI)))))) / (x * ((float) M_PI)));
                }
                
                function code(x, tau)
                	return Float32(Float32(1.0) * Float32(Float32(Float32(pi) * Float32(x + Float32(Float32(Float32(x * x) * x) * Float32(Float32(-0.16666666666666666) * Float32(Float32(pi) * Float32(pi)))))) / Float32(x * Float32(pi))))
                end
                
                function tmp = code(x, tau)
                	tmp = single(1.0) * ((single(pi) * (x + (((x * x) * x) * (single(-0.16666666666666666) * (single(pi) * single(pi)))))) / (x * single(pi)));
                end
                
                1 \cdot \frac{\pi \cdot \left(x + \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(-0.16666666666666666 \cdot \left(\pi \cdot \pi\right)\right)\right)}{x \cdot \pi}
                
                Derivation
                1. Initial program 98.0%

                  \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                2. Taylor expanded in x around 0

                  \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                3. Step-by-step derivation
                  1. Applied rewrites64.4%

                    \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                  2. Taylor expanded in x around 0

                    \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                  3. Step-by-step derivation
                    1. lower-*.f32N/A

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

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

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

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

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

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

                      \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
                    8. lower-PI.f3264.6%

                      \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                  4. Applied rewrites64.6%

                    \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                  5. Step-by-step derivation
                    1. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \color{blue}{\left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                    2. lift-+.f32N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \color{blue}{\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)}\right)}{x \cdot \pi} \]
                    3. distribute-lft-inN/A

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

                      \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                    5. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{\pi \cdot x + \color{blue}{x} \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                    6. sum-to-multN/A

                      \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
                    7. lower-unsound-*.f32N/A

                      \[\leadsto 1 \cdot \frac{\left(1 + \frac{x \cdot \left(\frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{\pi \cdot x}\right) \cdot \color{blue}{\left(\pi \cdot x\right)}}{x \cdot \pi} \]
                  6. Applied rewrites64.6%

                    \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot -0.16666666666666666\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \color{blue}{\left(x \cdot \pi\right)}}{x \cdot \pi} \]
                  7. Step-by-step derivation
                    1. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \color{blue}{\left(x \cdot \pi\right)}}{x \cdot \pi} \]
                    2. lift-+.f32N/A

                      \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(\color{blue}{x} \cdot \pi\right)}{x \cdot \pi} \]
                    3. lift-/.f32N/A

                      \[\leadsto 1 \cdot \frac{\left(1 + \frac{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi}\right) \cdot \left(x \cdot \pi\right)}{x \cdot \pi} \]
                    4. sum-to-mult-revN/A

                      \[\leadsto 1 \cdot \frac{x \cdot \pi + \color{blue}{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}}{x \cdot \pi} \]
                    5. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \pi + \color{blue}{\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right)} \cdot \left(\left(\pi \cdot \pi\right) \cdot \pi\right)}{x \cdot \pi} \]
                    6. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \pi + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \color{blue}{\left(\left(\pi \cdot \pi\right) \cdot \pi\right)}}{x \cdot \pi} \]
                    7. lift-*.f32N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \pi + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\left(\pi \cdot \pi\right) \cdot \color{blue}{\pi}\right)}{x \cdot \pi} \]
                    8. associate-*r*N/A

                      \[\leadsto 1 \cdot \frac{x \cdot \pi + \left(\left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \color{blue}{\pi}}{x \cdot \pi} \]
                    9. distribute-rgt-outN/A

                      \[\leadsto 1 \cdot \frac{\pi \cdot \color{blue}{\left(x + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\pi \cdot \pi\right)\right)}}{x \cdot \pi} \]
                    10. lower-*.f32N/A

                      \[\leadsto 1 \cdot \frac{\pi \cdot \color{blue}{\left(x + \left(x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right) \cdot \left(\pi \cdot \pi\right)\right)}}{x \cdot \pi} \]
                  8. Applied rewrites64.6%

                    \[\leadsto 1 \cdot \frac{\pi \cdot \color{blue}{\left(x + \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(-0.16666666666666666 \cdot \left(\pi \cdot \pi\right)\right)\right)}}{x \cdot \pi} \]
                  9. Add Preprocessing

                  Alternative 13: 64.6% accurate, 4.7× speedup?

                  \[1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot -0.16666666666666666\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                  (FPCore (x tau)
                    :precision binary32
                    (*
                   1.0
                   (/
                    (* x (+ PI (* (* (* (* x x) -0.16666666666666666) (* PI PI)) PI)))
                    (* x PI))))
                  float code(float x, float tau) {
                  	return 1.0f * ((x * (((float) M_PI) + ((((x * x) * -0.16666666666666666f) * (((float) M_PI) * ((float) M_PI))) * ((float) M_PI)))) / (x * ((float) M_PI)));
                  }
                  
                  function code(x, tau)
                  	return Float32(Float32(1.0) * Float32(Float32(x * Float32(Float32(pi) + Float32(Float32(Float32(Float32(x * x) * Float32(-0.16666666666666666)) * Float32(Float32(pi) * Float32(pi))) * Float32(pi)))) / Float32(x * Float32(pi))))
                  end
                  
                  function tmp = code(x, tau)
                  	tmp = single(1.0) * ((x * (single(pi) + ((((x * x) * single(-0.16666666666666666)) * (single(pi) * single(pi))) * single(pi)))) / (x * single(pi)));
                  end
                  
                  1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot -0.16666666666666666\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi}
                  
                  Derivation
                  1. Initial program 98.0%

                    \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                  2. Taylor expanded in x around 0

                    \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                  3. Step-by-step derivation
                    1. Applied rewrites64.4%

                      \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                    2. Taylor expanded in x around 0

                      \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                    3. Step-by-step derivation
                      1. lower-*.f32N/A

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

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

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

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

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

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

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
                      8. lower-PI.f3264.6%

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                    4. Applied rewrites64.6%

                      \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                    5. Step-by-step derivation
                      1. lift-*.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \color{blue}{\left({x}^{2} \cdot {\pi}^{3}\right)}\right)}{x \cdot \pi} \]
                      2. lift-*.f32N/A

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

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \color{blue}{{\pi}^{3}}\right)}{x \cdot \pi} \]
                      4. lift-pow.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot {\pi}^{\color{blue}{3}}\right)}{x \cdot \pi} \]
                      5. unpow3N/A

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

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \color{blue}{\pi}\right)}{x \cdot \pi} \]
                      7. lower-*.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \color{blue}{\pi}\right)}{x \cdot \pi} \]
                      8. lower-*.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\frac{-1}{6} \cdot {x}^{2}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      9. *-commutativeN/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left({x}^{2} \cdot \frac{-1}{6}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      10. lower-*.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left({x}^{2} \cdot \frac{-1}{6}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      11. lift-pow.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left({x}^{2} \cdot \frac{-1}{6}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      12. unpow2N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      13. lower-*.f32N/A

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                      14. lower-*.f3264.6%

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot -0.16666666666666666\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \pi\right)}{x \cdot \pi} \]
                    6. Applied rewrites64.6%

                      \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(\left(\left(x \cdot x\right) \cdot -0.16666666666666666\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \color{blue}{\pi}\right)}{x \cdot \pi} \]
                    7. Add Preprocessing

                    Alternative 14: 64.6% accurate, 4.7× speedup?

                    \[1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot -0.16666666666666666\right)\right)}{x \cdot \pi} \]
                    (FPCore (x tau)
                      :precision binary32
                      (*
                     1.0
                     (/
                      (* x (+ PI (* (* x x) (* (* (* PI PI) PI) -0.16666666666666666))))
                      (* x PI))))
                    float code(float x, float tau) {
                    	return 1.0f * ((x * (((float) M_PI) + ((x * x) * (((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * -0.16666666666666666f)))) / (x * ((float) M_PI)));
                    }
                    
                    function code(x, tau)
                    	return Float32(Float32(1.0) * Float32(Float32(x * Float32(Float32(pi) + Float32(Float32(x * x) * Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * Float32(-0.16666666666666666))))) / Float32(x * Float32(pi))))
                    end
                    
                    function tmp = code(x, tau)
                    	tmp = single(1.0) * ((x * (single(pi) + ((x * x) * (((single(pi) * single(pi)) * single(pi)) * single(-0.16666666666666666))))) / (x * single(pi)));
                    end
                    
                    1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot -0.16666666666666666\right)\right)}{x \cdot \pi}
                    
                    Derivation
                    1. Initial program 98.0%

                      \[\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                    2. Taylor expanded in x around 0

                      \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                    3. Step-by-step derivation
                      1. Applied rewrites64.4%

                        \[\leadsto \color{blue}{1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]
                      2. Taylor expanded in x around 0

                        \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                      3. Step-by-step derivation
                        1. lower-*.f32N/A

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

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

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

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

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

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

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \frac{-1}{6} \cdot \left({x}^{2} \cdot {\mathsf{PI}\left(\right)}^{\color{blue}{3}}\right)\right)}{x \cdot \pi} \]
                        8. lower-PI.f3264.6%

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}{x \cdot \pi} \]
                      4. Applied rewrites64.6%

                        \[\leadsto 1 \cdot \frac{\color{blue}{x \cdot \left(\pi + -0.16666666666666666 \cdot \left({x}^{2} \cdot {\pi}^{3}\right)\right)}}{x \cdot \pi} \]
                      5. Step-by-step derivation
                        1. lift-*.f32N/A

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

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left({x}^{2} \cdot {\pi}^{3}\right) \cdot \color{blue}{\frac{-1}{6}}\right)}{x \cdot \pi} \]
                        3. lift-*.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left({x}^{2} \cdot {\pi}^{3}\right) \cdot \frac{-1}{6}\right)}{x \cdot \pi} \]
                        4. associate-*l*N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + {x}^{2} \cdot \color{blue}{\left({\pi}^{3} \cdot \frac{-1}{6}\right)}\right)}{x \cdot \pi} \]
                        5. lower-*.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + {x}^{2} \cdot \color{blue}{\left({\pi}^{3} \cdot \frac{-1}{6}\right)}\right)}{x \cdot \pi} \]
                        6. lift-pow.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + {x}^{2} \cdot \left(\color{blue}{{\pi}^{3}} \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        7. unpow2N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\color{blue}{{\pi}^{3}} \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        8. lower-*.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\color{blue}{{\pi}^{3}} \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        9. lower-*.f3264.6%

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left({\pi}^{3} \cdot \color{blue}{-0.16666666666666666}\right)\right)}{x \cdot \pi} \]
                        10. lift-pow.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left({\pi}^{3} \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        11. unpow3N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        12. lower-*.f32N/A

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot \frac{-1}{6}\right)\right)}{x \cdot \pi} \]
                        13. lower-*.f3264.6%

                          \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot -0.16666666666666666\right)\right)}{x \cdot \pi} \]
                      6. Applied rewrites64.6%

                        \[\leadsto 1 \cdot \frac{x \cdot \left(\pi + \left(x \cdot x\right) \cdot \color{blue}{\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot -0.16666666666666666\right)}\right)}{x \cdot \pi} \]
                      7. Add Preprocessing

                      Alternative 15: 63.6% accurate, 258.0× speedup?

                      \[1 \]
                      (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
                      
                      1
                      
                      Derivation
                      1. Initial program 98.0%

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

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

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

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

                          \[\leadsto \color{blue}{\frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right) \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi}}{\left(x \cdot \pi\right) \cdot tau}} \]
                      3. Applied rewrites97.8%

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

                        \[\leadsto \color{blue}{1} \]
                      5. Step-by-step derivation
                        1. Applied rewrites63.6%

                          \[\leadsto \color{blue}{1} \]
                        2. Add Preprocessing

                        Reproduce

                        ?
                        herbie shell --seed 2025258 
                        (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))))