Lanczos kernel

Percentage Accurate: 97.9% → 97.9%

Time: 16.8s

Alternatives: 6

Speedup: 1.0×

• unsoundness detected in the egraph

Specification

\[\left(10^{-5} \leq x \land x \leq 1\right) \land \left(1 \leq tau \land tau \leq 5\right)\]

Math

\[\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

(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* x PI) tau)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))

C

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)));
}

Julia

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

MATLAB

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

Initial Program: 97.9% accurate, 1.0× speedup

Math

\[\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

(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* x PI) tau)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))

C

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)));
}

Julia

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

MATLAB

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

Alternative 1: 97.9% accurate, 1.0× speedup

Math

\[\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

(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* tau x) PI)))
  (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))))

C

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)));
}

Julia

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

MATLAB

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

Derivation

1. Initial program 97.9%

   \[\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-*.f32 N/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-*.f32 N/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. *-commutative N/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-*.f32 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} \]

   7. *-commutative N/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-*.f32 97.3%

      \[\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 rewrites 97.3%

   \[\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-*.f32 N/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-*.f32 N/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. *-commutative N/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-*.f32 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} \]

   7. *-commutative N/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-*.f32 97.9%

      \[\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 rewrites 97.9%

   \[\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: 70.9% accurate, 1.7× speedup

Math

\[\begin{array}{l} t_1 := tau \cdot \left(\pi \cdot x\right)\\ \frac{1}{\frac{t\_1}{\sin t\_1}} \cdot 1 \end{array} \]

FPCore

(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* tau (* PI x)))) (* (/ 1.0 (/ t_1 (sin t_1))) 1.0)))

C

float code(float x, float tau) {
	float t_1 = tau * (((float) M_PI) * x);
	return (1.0f / (t_1 / sinf(t_1))) * 1.0f;
}

Julia

function code(x, tau)
	t_1 = Float32(tau * Float32(Float32(pi) * x))
	return Float32(Float32(Float32(1.0) / Float32(t_1 / sin(t_1))) * Float32(1.0))
end

MATLAB

function tmp = code(x, tau)
	t_1 = tau * (single(pi) * x);
	tmp = (single(1.0) / (t_1 / sin(t_1))) * single(1.0);
end

Derivation

1. Initial program 97.9%

   \[\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-/.f32 N/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. frac-2neg N/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\sin \left(\left(x \cdot \pi\right) \cdot tau\right)\right)}{\mathsf{neg}\left(\left(x \cdot \pi\right) \cdot tau\right)}} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   3. frac-2neg N/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)\right)}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)}} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   4. div-flip N/A

      \[\leadsto \color{blue}{\frac{1}{\frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)\right)}}} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   5. remove-double-neg N/A

      \[\leadsto \frac{1}{\frac{\color{blue}{\left(x \cdot \pi\right) \cdot tau}}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)\right)}} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   6. remove-double-neg N/A

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

   7. lower-/.f32 N/A

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

   8. lower-/.f32 97.7%

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

   9. lift-*.f32 N/A

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

   10. *-commutative N/A

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

   11. lower-*.f32 97.7%

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

   12. lift-*.f32 N/A

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

   13. *-commutative N/A

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

   14. lower-*.f32 97.7%

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

   15. lift-*.f32 N/A

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

   16. *-commutative N/A

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

   17. lower-*.f32 97.7%

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

   18. lift-*.f32 N/A

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

   19. *-commutative N/A

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

   20. lower-*.f32 97.7%

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

3. Applied rewrites 97.7%

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

4. Taylor expanded in x around 0

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

6. Applied rewrites 70.9%

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

Alternative 3: 69.8% accurate, 0.6× speedup

Math

\[\begin{array}{l} t_1 := \left(x \cdot \pi\right) \cdot tau\\ \mathbf{if}\;\frac{\sin t\_1}{t\_1} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \leq 0.9999949932098389:\\ \;\;\;\;\frac{\cos \left(\mathsf{fma}\left(tau, x, -0.5\right) \cdot \pi\right)}{t\_1} \cdot 1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{\pi \cdot x}{\sin \left(\pi \cdot x\right) \cdot 1}}\\ \end{array} \]

FPCore

(FPCore (x tau)
  :precision binary32
  (let* ((t_1 (* (* x PI) tau)))
  (if (<=
       (* (/ (sin t_1) t_1) (/ (sin (* x PI)) (* x PI)))
       0.9999949932098389)
    (* (/ (cos (* (fma tau x -0.5) PI)) t_1) 1.0)
    (/ 1.0 (/ (* PI x) (* (sin (* PI x)) 1.0))))))

C

float code(float x, float tau) {
	float t_1 = (x * ((float) M_PI)) * tau;
	float tmp;
	if (((sinf(t_1) / t_1) * (sinf((x * ((float) M_PI))) / (x * ((float) M_PI)))) <= 0.9999949932098389f) {
		tmp = (cosf((fmaf(tau, x, -0.5f) * ((float) M_PI))) / t_1) * 1.0f;
	} else {
		tmp = 1.0f / ((((float) M_PI) * x) / (sinf((((float) M_PI) * x)) * 1.0f));
	}
	return tmp;
}

Julia

function code(x, tau)
	t_1 = Float32(Float32(x * Float32(pi)) * tau)
	tmp = Float32(0.0)
	if (Float32(Float32(sin(t_1) / t_1) * Float32(sin(Float32(x * Float32(pi))) / Float32(x * Float32(pi)))) <= Float32(0.9999949932098389))
		tmp = Float32(Float32(cos(Float32(fma(tau, x, Float32(-0.5)) * Float32(pi))) / t_1) * Float32(1.0));
	else
		tmp = Float32(Float32(1.0) / Float32(Float32(Float32(pi) * x) / Float32(sin(Float32(Float32(pi) * x)) * Float32(1.0))));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if (*.f32 (/.f32 (sin.f32 (*.f32 (*.f32 x (PI.f32)) tau)) (*.f32 (*.f32 x (PI.f32)) tau)) (/.f32 (sin.f32 (*.f32 x (PI.f32))) (*.f32 x (PI.f32)))) < 0.999994993

   1. Initial program 97.9%

      \[\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. remove-double-neg N/A

         \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(\left(x \cdot \pi\right) \cdot tau\right)\right)\right)\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      2. lift-sin.f32 N/A

         \[\leadsto \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}\right)\right)\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      3. sin-neg-rev N/A

         \[\leadsto \frac{\mathsf{neg}\left(\color{blue}{\sin \left(\mathsf{neg}\left(\left(x \cdot \pi\right) \cdot tau\right)\right)}\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      4. cos-+PI/2-rev N/A

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

      5. lower-cos.f32 N/A

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

      6. lift-*.f32 N/A

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

      7. lift-*.f32 N/A

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

      8. *-commutative N/A

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

      9. associate-*l* N/A

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

      10. distribute-rgt-neg-in N/A

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

      11. lift-PI.f32 N/A

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

      12. mult-flip N/A

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

      13. metadata-eval N/A

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

      14. distribute-lft-out N/A

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

      15. lower-*.f32 N/A

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

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

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

      17. lower-fma.f32 N/A

          \[\leadsto \frac{\cos \left(\pi \cdot \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(x\right), tau, \frac{1}{2}\right)}\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      18. lower-neg.f32 83.0%

          \[\leadsto \frac{\cos \left(\pi \cdot \mathsf{fma}\left(\color{blue}{-x}, tau, 0.5\right)\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   3. Applied rewrites 83.0%

      \[\leadsto \frac{\color{blue}{\cos \left(\pi \cdot \mathsf{fma}\left(-x, tau, 0.5\right)\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-cos.f32 N/A

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

      2. cos-neg-rev N/A

         \[\leadsto \frac{\color{blue}{\cos \left(\mathsf{neg}\left(\pi \cdot \mathsf{fma}\left(-x, tau, \frac{1}{2}\right)\right)\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      3. lower-cos.f32 N/A

         \[\leadsto \frac{\color{blue}{\cos \left(\mathsf{neg}\left(\pi \cdot \mathsf{fma}\left(-x, tau, \frac{1}{2}\right)\right)\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      4. lift-*.f32 N/A

         \[\leadsto \frac{\cos \left(\mathsf{neg}\left(\color{blue}{\pi \cdot \mathsf{fma}\left(-x, tau, \frac{1}{2}\right)}\right)\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      5. *-commutative N/A

         \[\leadsto \frac{\cos \left(\mathsf{neg}\left(\color{blue}{\mathsf{fma}\left(-x, tau, \frac{1}{2}\right) \cdot \pi}\right)\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

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

         \[\leadsto \frac{\cos \color{blue}{\left(\left(\mathsf{neg}\left(\mathsf{fma}\left(-x, tau, \frac{1}{2}\right)\right)\right) \cdot \pi\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      7. lift-fma.f32 N/A

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

      8. lift-*.f32 N/A

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

      9. add-flip N/A

         \[\leadsto \frac{\cos \left(\left(\mathsf{neg}\left(\color{blue}{\left(\left(-x\right) \cdot tau - \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)}\right)\right) \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      10. sub-negate-rev N/A

          \[\leadsto \frac{\cos \left(\color{blue}{\left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - \left(-x\right) \cdot tau\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      11. lower-*.f32 N/A

          \[\leadsto \frac{\cos \color{blue}{\left(\left(\left(\mathsf{neg}\left(\frac{1}{2}\right)\right) - \left(-x\right) \cdot tau\right) \cdot \pi\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      12. sub-negate-rev N/A

          \[\leadsto \frac{\cos \left(\color{blue}{\left(\mathsf{neg}\left(\left(\left(-x\right) \cdot tau - \left(\mathsf{neg}\left(\frac{1}{2}\right)\right)\right)\right)\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      13. add-flip N/A

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

      14. distribute-neg-in N/A

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

      15. lift-*.f32 N/A

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

      16. lift-neg.f32 N/A

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

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

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

      18. remove-double-neg N/A

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

      19. *-commutative N/A

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

      20. lower-fma.f32 N/A

          \[\leadsto \frac{\cos \left(\color{blue}{\mathsf{fma}\left(tau, x, \mathsf{neg}\left(\frac{1}{2}\right)\right)} \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

      21. metadata-eval 83.0%

          \[\leadsto \frac{\cos \left(\mathsf{fma}\left(tau, x, \color{blue}{-0.5}\right) \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   5. Applied rewrites 83.0%

      \[\leadsto \frac{\color{blue}{\cos \left(\mathsf{fma}\left(tau, x, -0.5\right) \cdot \pi\right)}}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

   6. Taylor expanded in x around 0

      \[\leadsto \frac{\cos \left(\mathsf{fma}\left(tau, x, -0.5\right) \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \color{blue}{1} \]
   7. Step-by-step derivation

   8. Applied rewrites 60.7%

      \[\leadsto \frac{\cos \left(\mathsf{fma}\left(tau, x, -0.5\right) \cdot \pi\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \color{blue}{1} \]

   if 0.999994993 < (*.f32 (/.f32 (sin.f32 (*.f32 (*.f32 x (PI.f32)) tau)) (*.f32 (*.f32 x (PI.f32)) tau)) (/.f32 (sin.f32 (*.f32 x (PI.f32))) (*.f32 x (PI.f32))))

   1. Initial program 97.9%

      \[\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. remove-double-neg N/A

         \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(x \cdot \pi\right)\right)\right)\right)}}{x \cdot \pi} \]

      2. lift-sin.f32 N/A

         \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi\right)}\right)\right)\right)}{x \cdot \pi} \]

      3. sin-+PI-rev N/A

         \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi + \mathsf{PI}\left(\right)\right)}\right)}{x \cdot \pi} \]

      4. cos-+PI/2-rev N/A

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

      5. lower-cos.f32 N/A

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

      6. +-commutative N/A

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

      7. lift-PI.f32 N/A

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

      8. associate-+l+ N/A

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

      9. +-commutative N/A

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

      10. lift-PI.f32 N/A

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

      11. +-commutative N/A

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

      12. lift-PI.f32 N/A

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

      13. mult-flip N/A

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

      14. metadata-eval N/A

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

      15. lift-*.f32 N/A

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

      16. *-commutative N/A

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

      17. distribute-lft-out N/A

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

      18. lift-PI.f32 N/A

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

      19. lower-fma.f32 N/A

          \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\cos \color{blue}{\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}}{x \cdot \pi} \]

   3. Applied rewrites 76.7%

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}}{x \cdot \pi} \]

   4. Taylor expanded in x around 0

      \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]
   5. Step-by-step derivation

   6. Applied rewrites 52.3%

      \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]
   7. Step-by-step derivation

      1. lift-cos.f32 N/A

         \[\leadsto 1 \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}}{x \cdot \pi} \]

      2. lift-fma.f32 N/A

         \[\leadsto 1 \cdot \frac{\cos \color{blue}{\left(\pi \cdot \left(\frac{1}{2} + x\right) + \pi\right)}}{x \cdot \pi} \]

      3. cos-sum N/A

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

      4. sub-negate-rev N/A

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

      5. sub-negate N/A

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

      6. cos-sum N/A

         \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + x\right) + \pi\right)}\right)\right)\right)}{x \cdot \pi} \]

      7. lift-fma.f32 N/A

         \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\cos \color{blue}{\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

      8. lift-cos.f32 N/A

         \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

      9. lift-cos.f32 N/A

         \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

      10. cos-+PI-rev N/A

          \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right) + \mathsf{PI}\left(\right)\right)}\right)}{x \cdot \pi} \]

      11. cos-neg-rev N/A

          \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{neg}\left(\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right) + \mathsf{PI}\left(\right)\right)\right)\right)}\right)}{x \cdot \pi} \]

   8. Applied rewrites 51.1%

      \[\leadsto 1 \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \left(-1.5 - x\right) - 1, \pi\right)\right)}}{x \cdot \pi} \]

   10. Applied rewrites 64.3%

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

Alternative 4: 64.3% accurate, 1.9× speedup

Math

\[\frac{1}{\frac{\pi \cdot x}{\sin \left(\pi \cdot x\right) \cdot 1}} \]

FPCore

(FPCore (x tau)
  :precision binary32
  (/ 1.0 (/ (* PI x) (* (sin (* PI x)) 1.0))))

C

float code(float x, float tau) {
	return 1.0f / ((((float) M_PI) * x) / (sinf((((float) M_PI) * x)) * 1.0f));
}

Julia

function code(x, tau)
	return Float32(Float32(1.0) / Float32(Float32(Float32(pi) * x) / Float32(sin(Float32(Float32(pi) * x)) * Float32(1.0))))
end

MATLAB

function tmp = code(x, tau)
	tmp = single(1.0) / ((single(pi) * x) / (sin((single(pi) * x)) * single(1.0)));
end

Derivation

1. Initial program 97.9%

   \[\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. remove-double-neg N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(x \cdot \pi\right)\right)\right)\right)}}{x \cdot \pi} \]

   2. lift-sin.f32 N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi\right)}\right)\right)\right)}{x \cdot \pi} \]

   3. sin-+PI-rev N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi + \mathsf{PI}\left(\right)\right)}\right)}{x \cdot \pi} \]

   4. cos-+PI/2-rev N/A

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

   5. lower-cos.f32 N/A

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

   6. +-commutative N/A

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

   7. lift-PI.f32 N/A

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

   8. associate-+l+ N/A

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

   9. +-commutative N/A

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

   10. lift-PI.f32 N/A

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

   11. +-commutative N/A

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

   12. lift-PI.f32 N/A

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

   13. mult-flip N/A

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

   14. metadata-eval N/A

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

   15. lift-*.f32 N/A

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

   16. *-commutative N/A

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

   17. distribute-lft-out N/A

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

   18. lift-PI.f32 N/A

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

   19. lower-fma.f32 N/A

       \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\cos \color{blue}{\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}}{x \cdot \pi} \]

3. Applied rewrites 76.7%

   \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}}{x \cdot \pi} \]

4. Taylor expanded in x around 0

   \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]
5. Step-by-step derivation

6. Applied rewrites 52.3%

   \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]
7. Step-by-step derivation

   1. lift-cos.f32 N/A

      \[\leadsto 1 \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}}{x \cdot \pi} \]

   2. lift-fma.f32 N/A

      \[\leadsto 1 \cdot \frac{\cos \color{blue}{\left(\pi \cdot \left(\frac{1}{2} + x\right) + \pi\right)}}{x \cdot \pi} \]

   3. cos-sum N/A

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

   4. sub-negate-rev N/A

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

   5. sub-negate N/A

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

   6. cos-sum N/A

      \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\pi \cdot \left(\frac{1}{2} + x\right) + \pi\right)}\right)\right)\right)}{x \cdot \pi} \]

   7. lift-fma.f32 N/A

      \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\cos \color{blue}{\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

   8. lift-cos.f32 N/A

      \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

   9. lift-cos.f32 N/A

      \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}\right)\right)\right)}{x \cdot \pi} \]

   10. cos-+PI-rev N/A

       \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right) + \mathsf{PI}\left(\right)\right)}\right)}{x \cdot \pi} \]

   11. cos-neg-rev N/A

       \[\leadsto 1 \cdot \frac{\mathsf{neg}\left(\color{blue}{\cos \left(\mathsf{neg}\left(\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right) + \mathsf{PI}\left(\right)\right)\right)\right)}\right)}{x \cdot \pi} \]

8. Applied rewrites 51.1%

   \[\leadsto 1 \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, \left(-1.5 - x\right) - 1, \pi\right)\right)}}{x \cdot \pi} \]

10. Applied rewrites 64.3%

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

Alternative 5: 64.3% accurate, 2.0× speedup

Math

\[1 \cdot \frac{\sin \left(x \cdot \pi\right)}{x \cdot \pi} \]

FPCore

(FPCore (x tau)
  :precision binary32
  (* 1.0 (/ (sin (* x PI)) (* x PI))))

C

float code(float x, float tau) {
	return 1.0f * (sinf((x * ((float) M_PI))) / (x * ((float) M_PI)));
}

Julia

function code(x, tau)
	return Float32(Float32(1.0) * Float32(sin(Float32(x * Float32(pi))) / Float32(x * Float32(pi))))
end

MATLAB

function tmp = code(x, tau)
	tmp = single(1.0) * (sin((x * single(pi))) / (x * single(pi)));
end

Derivation

1. Initial program 97.9%

   \[\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

4. Applied rewrites 64.3%

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

Alternative 6: 14.4% accurate, 2.2× speedup

Math

\[1 \cdot \frac{\cos 4.71238899230957}{x \cdot \pi} \]

FPCore

(FPCore (x tau)
  :precision binary32
  (* 1.0 (/ (cos 4.71238899230957) (* x PI))))

C

float code(float x, float tau) {
	return 1.0f * (cosf(4.71238899230957f) / (x * ((float) M_PI)));
}

Julia

function code(x, tau)
	return Float32(Float32(1.0) * Float32(cos(Float32(4.71238899230957)) / Float32(x * Float32(pi))))
end

MATLAB

function tmp = code(x, tau)
	tmp = single(1.0) * (cos(single(4.71238899230957)) / (x * single(pi)));
end

Derivation

1. Initial program 97.9%

   \[\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. remove-double-neg N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\mathsf{neg}\left(\left(\mathsf{neg}\left(\sin \left(x \cdot \pi\right)\right)\right)\right)}}{x \cdot \pi} \]

   2. lift-sin.f32 N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi\right)}\right)\right)\right)}{x \cdot \pi} \]

   3. sin-+PI-rev N/A

      \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\mathsf{neg}\left(\color{blue}{\sin \left(x \cdot \pi + \mathsf{PI}\left(\right)\right)}\right)}{x \cdot \pi} \]

   4. cos-+PI/2-rev N/A

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

   5. lower-cos.f32 N/A

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

   6. +-commutative N/A

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

   7. lift-PI.f32 N/A

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

   8. associate-+l+ N/A

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

   9. +-commutative N/A

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

   10. lift-PI.f32 N/A

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

   11. +-commutative N/A

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

   12. lift-PI.f32 N/A

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

   13. mult-flip N/A

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

   14. metadata-eval N/A

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

   15. lift-*.f32 N/A

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

   16. *-commutative N/A

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

   17. distribute-lft-out N/A

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

   18. lift-PI.f32 N/A

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

   19. lower-fma.f32 N/A

       \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\cos \color{blue}{\left(\mathsf{fma}\left(\pi, \frac{1}{2} + x, \pi\right)\right)}}{x \cdot \pi} \]

3. Applied rewrites 76.7%

   \[\leadsto \frac{\sin \left(\left(x \cdot \pi\right) \cdot tau\right)}{\left(x \cdot \pi\right) \cdot tau} \cdot \frac{\color{blue}{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}}{x \cdot \pi} \]

4. Taylor expanded in x around 0

   \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]
5. Step-by-step derivation

6. Applied rewrites 52.3%

   \[\leadsto \color{blue}{1} \cdot \frac{\cos \left(\mathsf{fma}\left(\pi, 0.5 + x, \pi\right)\right)}{x \cdot \pi} \]

7. Taylor expanded in x around 0

   \[\leadsto 1 \cdot \frac{\cos \color{blue}{\left(\pi + \frac{1}{2} \cdot \pi\right)}}{x \cdot \pi} \]
8. Step-by-step derivation

   1. lower-+.f32 N/A

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

   2. lower-PI.f32 N/A

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

   3. lower-*.f32 N/A

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

   4. lower-PI.f32 14.4%

      \[\leadsto 1 \cdot \frac{\cos \left(\pi + 0.5 \cdot \pi\right)}{x \cdot \pi} \]

9. Applied rewrites 14.4%

   \[\leadsto 1 \cdot \frac{\cos \color{blue}{\left(\pi + 0.5 \cdot \pi\right)}}{x \cdot \pi} \]

10. Evaluated real constant 14.4%

    \[\leadsto 1 \cdot \frac{\cos 4.71238899230957}{x \cdot \pi} \]
11. Add Preprocessing

Reproduce

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