ab-angle->ABCF B

Percentage Accurate: 54.2% → 67.7%

Time: 8.5s

Alternatives: 20

Speedup: 13.7×

• 32.1% of points produce a very large (infinite) output. You may want to add a precondition.

Specification

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot \frac{angle}{180}\\ \left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin t\_0\right) \cdot \cos t\_0 \end{array} \end{array} \]

FPCore

(FPCore (a b angle)
 :precision binary64
 (let* ((t_0 (* (PI) (/ angle 180.0))))
   (* (* (* 2.0 (- (pow b 2.0) (pow a 2.0))) (sin t_0)) (cos t_0))))

Initial Program: 54.2% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{PI}\left(\right) \cdot \frac{angle}{180}\\ \left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin t\_0\right) \cdot \cos t\_0 \end{array} \end{array} \]

FPCore

(FPCore (a b angle)
 :precision binary64
 (let* ((t_0 (* (PI) (/ angle 180.0))))
   (* (* (* 2.0 (- (pow b 2.0) (pow a 2.0))) (sin t_0)) (cos t_0))))

Alternative 1: 67.7% accurate, 1.7× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} t_0 := \sqrt{\mathsf{PI}\left(\right)}\\ \mathbf{if}\;a\_m \leq 1.52 \cdot 10^{+153}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(\left(b\_m - a\_m\right) \cdot 2\right) \cdot \left(\sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \cos \left(\frac{\mathsf{PI}\left(\right) \cdot angle}{-180}\right)\right)\right)\\ \mathbf{elif}\;a\_m \leq 1.25 \cdot 10^{+266}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(\mathsf{fma}\left(-2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, 0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right) \cdot \left(b\_m - a\_m\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\sin \left(2 \cdot \frac{\left(angle \cdot t\_0\right) \cdot t\_0}{180}\right) \cdot \left(b\_m - a\_m\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (let* ((t_0 (sqrt (PI))))
   (if (<= a_m 1.52e+153)
     (*
      (+ a_m b_m)
      (*
       (* (- b_m a_m) 2.0)
       (* (sin (* (/ angle 180.0) (PI))) (cos (/ (* (PI) angle) -180.0)))))
     (if (<= a_m 1.25e+266)
       (*
        (+ a_m b_m)
        (*
         (*
          (fma
           (* -2.2862368541380886e-7 (* angle angle))
           (pow (PI) 3.0)
           (* 0.011111111111111112 (PI)))
          angle)
         (- b_m a_m)))
       (*
        (+ a_m b_m)
        (* (sin (* 2.0 (/ (* (* angle t_0) t_0) 180.0))) (- b_m a_m)))))))

Derivation

1. Split input into 3 regimes

2. if a < 1.52e153

   1. Initial program 55.6%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 57.4%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 65.3

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 65.3%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

      2. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

      3. associate-*r/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      4. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      5. lower-/.f64 65.4

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      6. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      7. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      8. lower-*.f64 65.4

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. Applied rewrites 65.4%

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
   9. Step-by-step derivation

      1. lift--.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \color{blue}{\left(b - a\right)}\right) \]

      2. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b - a\right)\right)} \]

      3. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right)\right)} \]

      4. lift-sin.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \color{blue}{\sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right)}\right) \]

      5. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \color{blue}{\left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right)}\right) \]

      6. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right)\right) \]

      7. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right)\right) \]

      9. associate-*r/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right)\right) \]

      10. lift-PI.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \left(\color{blue}{\mathsf{PI}\left(\right)} \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-PI.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \left(\color{blue}{\mathsf{PI}\left(\right)} \cdot \frac{angle}{180}\right)\right)\right) \]

      12. lift-/.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right)\right) \]

      13. lift-*.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right)\right) \]

      14. sin-2 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\left(b - a\right) \cdot \color{blue}{\left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)}\right) \]

      15. associate-*r* N/A

          \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(\left(b - a\right) \cdot 2\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   10. Applied rewrites 65.5%

       \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(\left(b - a\right) \cdot 2\right) \cdot \left(\sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \cos \left(\frac{\mathsf{PI}\left(\right) \cdot angle}{-180}\right)\right)\right)} \]

   if 1.52e153 < a < 1.25e266

   1. Initial program 38.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 49.3%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 78.9

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 78.9%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in angle around 0

      \[\leadsto \left(a + b\right) \cdot \left(\color{blue}{\left(angle \cdot \left(\frac{-1}{4374000} \cdot \left({angle}^{2} \cdot {\mathsf{PI}\left(\right)}^{3}\right) + \frac{1}{90} \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \left(b - a\right)\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 89.6%

      \[\leadsto \left(a + b\right) \cdot \left(\color{blue}{\left(\mathsf{fma}\left(-2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, 0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)} \cdot \left(b - a\right)\right) \]

   if 1.25e266 < a

   1. Initial program 53.8%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 62.1%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 69.0

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 69.0%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

      2. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

      3. associate-*r/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      4. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      5. lower-/.f64 84.4

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      6. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      7. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      8. lower-*.f64 84.4

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. Applied rewrites 84.4%

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      2. lift-PI.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{angle \cdot \color{blue}{\mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      3. add-sqr-sqrt N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{angle \cdot \color{blue}{\left(\sqrt{\mathsf{PI}\left(\right)} \cdot \sqrt{\mathsf{PI}\left(\right)}\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      4. associate-*r* N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}}}{180}\right) \cdot \left(b - a\right)\right) \]

      5. lower-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}}}{180}\right) \cdot \left(b - a\right)\right) \]

      6. lower-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right)} \cdot \sqrt{\mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      7. lift-PI.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\left(angle \cdot \sqrt{\color{blue}{\mathsf{PI}\left(\right)}}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      8. lower-sqrt.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\left(angle \cdot \color{blue}{\sqrt{\mathsf{PI}\left(\right)}}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      9. lift-PI.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\color{blue}{\mathsf{PI}\left(\right)}}}{180}\right) \cdot \left(b - a\right)\right) \]

      10. lower-sqrt.f64 84.4

          \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \color{blue}{\sqrt{\mathsf{PI}\left(\right)}}}{180}\right) \cdot \left(b - a\right)\right) \]

   10. Applied rewrites 84.4%

       \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\left(angle \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}}}{180}\right) \cdot \left(b - a\right)\right) \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 2: 63.2% accurate, 0.7× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} t_0 := \sqrt{\mathsf{PI}\left(\right)}\\ t_1 := \mathsf{PI}\left(\right) \cdot \frac{angle}{180}\\ \mathbf{if}\;\left(\left(2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right)\right) \cdot \sin t\_1\right) \cdot \cos t\_1 \leq -2 \cdot 10^{+295}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(\mathsf{fma}\left(2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, -0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right) \cdot a\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\sin \left(2 \cdot \left(\left(\frac{angle}{180} \cdot t\_0\right) \cdot t\_0\right)\right) \cdot \left(b\_m - a\_m\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (let* ((t_0 (sqrt (PI))) (t_1 (* (PI) (/ angle 180.0))))
   (if (<=
        (* (* (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) (sin t_1)) (cos t_1))
        -2e+295)
     (*
      (+ a_m b_m)
      (*
       (*
        (fma
         (* 2.2862368541380886e-7 (* angle angle))
         (pow (PI) 3.0)
         (* -0.011111111111111112 (PI)))
        angle)
       a_m))
     (*
      (+ a_m b_m)
      (* (sin (* 2.0 (* (* (/ angle 180.0) t_0) t_0))) (- b_m a_m))))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) (sin.f64 (*.f64 (PI.f64) (/.f64 angle #s(literal 180 binary64))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle #s(literal 180 binary64))))) < -2e295

   1. Initial program 50.8%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 50.8%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 74.4

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 74.4%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around inf

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(-1 \cdot \left(a \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 37.2%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right)} \]

   10. Taylor expanded in angle around 0

       \[\leadsto \left(a + b\right) \cdot \left(\left(angle \cdot \left(\frac{-1}{90} \cdot \mathsf{PI}\left(\right) + \frac{1}{4374000} \cdot \left({angle}^{2} \cdot {\mathsf{PI}\left(\right)}^{3}\right)\right)\right) \cdot a\right) \]
   11. Step-by-step derivation

   12. Applied rewrites 58.0%

       \[\leadsto \left(a + b\right) \cdot \left(\left(\mathsf{fma}\left(2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, -0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right) \cdot a\right) \]

   if -2e295 < (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) (sin.f64 (*.f64 (PI.f64) (/.f64 angle #s(literal 180 binary64))))) (cos.f64 (*.f64 (PI.f64) (/.f64 angle #s(literal 180 binary64)))))

   1. Initial program 55.0%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 58.5%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 64.7

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 64.7%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

      2. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

      3. associate-*r/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      4. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      5. lower-/.f64 64.3

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      6. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      7. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      8. lower-*.f64 64.3

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. Applied rewrites 64.3%

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
   9. Step-by-step derivation

      1. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]

      2. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      3. associate-*l/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)}\right) \cdot \left(b - a\right)\right) \]

      4. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\color{blue}{\frac{angle}{180}} \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(b - a\right)\right) \]

      5. lift-PI.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\frac{angle}{180} \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \cdot \left(b - a\right)\right) \]

      6. add-sqr-sqrt N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\frac{angle}{180} \cdot \color{blue}{\left(\sqrt{\mathsf{PI}\left(\right)} \cdot \sqrt{\mathsf{PI}\left(\right)}\right)}\right)\right) \cdot \left(b - a\right)\right) \]

      7. associate-*r* N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}\right)}\right) \cdot \left(b - a\right)\right) \]

      8. lower-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}\right)}\right) \cdot \left(b - a\right)\right) \]

      9. lower-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\color{blue}{\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right)} \cdot \sqrt{\mathsf{PI}\left(\right)}\right)\right) \cdot \left(b - a\right)\right) \]

      10. lift-PI.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\left(\frac{angle}{180} \cdot \sqrt{\color{blue}{\mathsf{PI}\left(\right)}}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}\right)\right) \cdot \left(b - a\right)\right) \]

      11. lower-sqrt.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\left(\frac{angle}{180} \cdot \color{blue}{\sqrt{\mathsf{PI}\left(\right)}}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}\right)\right) \cdot \left(b - a\right)\right) \]

      12. lift-PI.f64 N/A

          \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\color{blue}{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(b - a\right)\right) \]

      13. lower-sqrt.f64 64.2

          \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \color{blue}{\sqrt{\mathsf{PI}\left(\right)}}\right)\right) \cdot \left(b - a\right)\right) \]

   10. Applied rewrites 64.2%

       \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\left(\frac{angle}{180} \cdot \sqrt{\mathsf{PI}\left(\right)}\right) \cdot \sqrt{\mathsf{PI}\left(\right)}\right)}\right) \cdot \left(b - a\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 66.5% accurate, 0.8× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} t_0 := 2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right)\\ \mathbf{if}\;t\_0 \leq -2 \cdot 10^{+300}:\\ \;\;\;\;\left(b\_m - a\_m\right) \cdot \left(\left(0.011111111111111112 \cdot angle\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(a\_m + b\_m\right)\right)\right)\\ \mathbf{elif}\;t\_0 \leq 2 \cdot 10^{-204}:\\ \;\;\;\;\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot \left(a\_m \cdot a\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (let* ((t_0 (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0)))))
   (if (<= t_0 -2e+300)
     (* (- b_m a_m) (* (* 0.011111111111111112 angle) (* (PI) (+ a_m b_m))))
     (if (<= t_0 2e-204)
       (* (sin (* -0.011111111111111112 (* (PI) angle))) (* a_m a_m))
       (*
        (+ a_m b_m)
        (* (- b_m a_m) (* (* 0.011111111111111112 (PI)) angle)))))))

Derivation

1. Split input into 3 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -2.0000000000000001e300

   1. Initial program 49.9%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 44.6%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 69.6%

      \[\leadsto \left(b - a\right) \cdot \color{blue}{\left(\left(0.011111111111111112 \cdot angle\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \left(a + b\right)\right)\right)} \]

   if -2.0000000000000001e300 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < 2e-204

   1. Initial program 63.5%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 63.5%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 63.5

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 63.5%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around inf

      \[\leadsto \color{blue}{-1 \cdot \left({a}^{2} \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 62.1%

      \[\leadsto \color{blue}{\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot \left(a \cdot a\right)} \]

   if 2e-204 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 49.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 53.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 62.6%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 4: 68.0% accurate, 1.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq -5 \cdot 10^{+295}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(\mathsf{fma}\left(2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, -0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right) \cdot a\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b\_m - a\_m\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) -5e+295)
   (*
    (+ a_m b_m)
    (*
     (*
      (fma
       (* 2.2862368541380886e-7 (* angle angle))
       (pow (PI) 3.0)
       (* -0.011111111111111112 (PI)))
      angle)
     a_m))
   (* (+ a_m b_m) (* (sin (* 2.0 (/ (* angle (PI)) 180.0))) (- b_m a_m)))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -4.99999999999999991e295

   1. Initial program 49.0%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 49.0%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 73.7

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 73.7%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around inf

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(-1 \cdot \left(a \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 71.8%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right)} \]

   10. Taylor expanded in angle around 0

       \[\leadsto \left(a + b\right) \cdot \left(\left(angle \cdot \left(\frac{-1}{90} \cdot \mathsf{PI}\left(\right) + \frac{1}{4374000} \cdot \left({angle}^{2} \cdot {\mathsf{PI}\left(\right)}^{3}\right)\right)\right) \cdot a\right) \]
   11. Step-by-step derivation

   12. Applied rewrites 80.8%

       \[\leadsto \left(a + b\right) \cdot \left(\left(\mathsf{fma}\left(2.2862368541380886 \cdot 10^{-7} \cdot \left(angle \cdot angle\right), {\mathsf{PI}\left(\right)}^{3}, -0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right) \cdot a\right) \]

   if -4.99999999999999991e295 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 55.7%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 59.3%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 64.4

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 64.4%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

      2. lift-/.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

      3. associate-*r/ N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      4. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      5. lower-/.f64 65.0

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

      6. lift-*.f64 N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

      7. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

      8. lower-*.f64 65.0

         \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. Applied rewrites 65.0%

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 66.4% accurate, 1.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq 2 \cdot 10^{-204}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\sin \left(\left(-0.011111111111111112 \cdot angle\right) \cdot \mathsf{PI}\left(\right)\right) \cdot a\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) 2e-204)
   (* (+ a_m b_m) (* (sin (* (* -0.011111111111111112 angle) (PI))) a_m))
   (* (+ a_m b_m) (* (- b_m a_m) (* (* 0.011111111111111112 (PI)) angle)))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < 2e-204

   1. Initial program 58.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 58.2%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 68.0

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 68.0%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around inf

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(-1 \cdot \left(a \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 65.9%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right)} \]
   10. Step-by-step derivation

   11. Applied rewrites 67.5%

       \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\left(-0.011111111111111112 \cdot angle\right) \cdot \mathsf{PI}\left(\right)\right) \cdot a\right) \]

   if 2e-204 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 49.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 53.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 62.6%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 66.5% accurate, 1.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq 2 \cdot 10^{-204}:\\ \;\;\;\;a\_m \cdot \left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) 2e-204)
   (* a_m (* (sin (* -0.011111111111111112 (* (PI) angle))) a_m))
   (* (+ a_m b_m) (* (- b_m a_m) (* (* 0.011111111111111112 (PI)) angle)))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < 2e-204

   1. Initial program 58.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 58.2%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 68.0

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 68.0%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around inf

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(-1 \cdot \left(a \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 65.9%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right)} \]

   10. Taylor expanded in a around inf

       \[\leadsto \color{blue}{a} \cdot \left(\sin \left(\frac{-1}{90} \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right) \]
   11. Step-by-step derivation

   12. Applied rewrites 66.4%

       \[\leadsto \color{blue}{a} \cdot \left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right) \]

   if 2e-204 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 49.2%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 53.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 62.6%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification 64.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;2 \cdot \left({b}^{2} - {a}^{2}\right) \leq 2 \cdot 10^{-204}:\\ \;\;\;\;a \cdot \left(\sin \left(-0.011111111111111112 \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot a\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a + b\right) \cdot \left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 7: 59.7% accurate, 1.9× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq -\infty:\\ \;\;\;\;\left(a\_m \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\_m\right)\right) \cdot -0.011111111111111112\\ \mathbf{else}:\\ \;\;\;\;\left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(a\_m + b\_m\right)\right)\right) \cdot angle\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) (- INFINITY))
   (* (* a_m (* (* (PI) angle) a_m)) -0.011111111111111112)
   (* (* (* 0.011111111111111112 (PI)) (* (- b_m a_m) (+ a_m b_m))) angle)))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -inf.0

   1. Initial program 48.1%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 42.5%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around inf

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

   8. Applied rewrites 42.5%

      \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
   9. Step-by-step derivation

   10. Applied rewrites 42.5%

       \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]

   11. Taylor expanded in a around inf

       \[\leadsto \frac{-1}{90} \cdot \color{blue}{\left({a}^{2} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
   12. Step-by-step derivation

   13. Applied rewrites 68.4%

       \[\leadsto \left(a \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\right)\right) \cdot \color{blue}{-0.011111111111111112} \]

   if -inf.0 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 55.8%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 55.6%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 55.6%

      \[\leadsto \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(b - a\right) \cdot \left(a + b\right)\right)\right) \cdot \color{blue}{angle} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 8: 59.7% accurate, 1.9× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq -\infty:\\ \;\;\;\;\left(a\_m \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\_m\right)\right) \cdot -0.011111111111111112\\ \mathbf{else}:\\ \;\;\;\;\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b\_m + a\_m\right) \cdot \left(b\_m - a\_m\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) (- INFINITY))
   (* (* a_m (* (* (PI) angle) a_m)) -0.011111111111111112)
   (* (* angle (* 0.011111111111111112 (PI))) (* (+ b_m a_m) (- b_m a_m)))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -inf.0

   1. Initial program 48.1%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 42.5%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around inf

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

   8. Applied rewrites 42.5%

      \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
   9. Step-by-step derivation

   10. Applied rewrites 42.5%

       \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]

   11. Taylor expanded in a around inf

       \[\leadsto \frac{-1}{90} \cdot \color{blue}{\left({a}^{2} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
   12. Step-by-step derivation

   13. Applied rewrites 68.4%

       \[\leadsto \left(a \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\right)\right) \cdot \color{blue}{-0.011111111111111112} \]

   if -inf.0 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 55.8%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 55.6%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 9: 59.4% accurate, 1.9× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq -1 \cdot 10^{-238}:\\ \;\;\;\;\left(a\_m \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\_m\right)\right) \cdot -0.011111111111111112\\ \mathbf{else}:\\ \;\;\;\;\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(b\_m \cdot \left(b\_m - a\_m\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) -1e-238)
   (* (* a_m (* (* (PI) angle) a_m)) -0.011111111111111112)
   (* (* angle (* 0.011111111111111112 (PI))) (* b_m (- b_m a_m)))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -9.9999999999999999e-239

   1. Initial program 52.5%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 45.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around inf

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

   8. Applied rewrites 45.2%

      \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
   9. Step-by-step derivation

   10. Applied rewrites 45.2%

       \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]

   11. Taylor expanded in a around inf

       \[\leadsto \frac{-1}{90} \cdot \color{blue}{\left({a}^{2} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
   12. Step-by-step derivation

   13. Applied rewrites 57.0%

       \[\leadsto \left(a \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\right)\right) \cdot \color{blue}{-0.011111111111111112} \]

   if -9.9999999999999999e-239 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 55.6%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 59.0%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around 0

      \[\leadsto \left(angle \cdot \left(\frac{1}{90} \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(b \cdot \left(\color{blue}{b} - a\right)\right) \]
   7. Step-by-step derivation

   8. Applied rewrites 57.6%

      \[\leadsto \left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(b \cdot \left(\color{blue}{b} - a\right)\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 10: 58.4% accurate, 1.9× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;2 \cdot \left({b\_m}^{2} - {a\_m}^{2}\right) \leq -1 \cdot 10^{-238}:\\ \;\;\;\;\left(a\_m \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\_m\right)\right) \cdot -0.011111111111111112\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\mathsf{PI}\left(\right) \cdot \left(b\_m \cdot b\_m\right)\right) \cdot angle\right) \cdot 0.011111111111111112\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= (* 2.0 (- (pow b_m 2.0) (pow a_m 2.0))) -1e-238)
   (* (* a_m (* (* (PI) angle) a_m)) -0.011111111111111112)
   (* (* (* (PI) (* b_m b_m)) angle) 0.011111111111111112)))

Derivation

1. Split input into 2 regimes

2. if (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64)))) < -9.9999999999999999e-239

   1. Initial program 52.5%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 45.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around inf

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

   8. Applied rewrites 45.2%

      \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
   9. Step-by-step derivation

   10. Applied rewrites 45.2%

       \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]

   11. Taylor expanded in a around inf

       \[\leadsto \frac{-1}{90} \cdot \color{blue}{\left({a}^{2} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
   12. Step-by-step derivation

   13. Applied rewrites 57.0%

       \[\leadsto \left(a \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\right)\right) \cdot \color{blue}{-0.011111111111111112} \]

   if -9.9999999999999999e-239 < (*.f64 #s(literal 2 binary64) (-.f64 (pow.f64 b #s(literal 2 binary64)) (pow.f64 a #s(literal 2 binary64))))

   1. Initial program 55.6%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 59.0%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

   6. Taylor expanded in a around 0

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

   8. Applied rewrites 58.3%

      \[\leadsto \left(\left(\mathsf{PI}\left(\right) \cdot \left(b \cdot b\right)\right) \cdot angle\right) \cdot \color{blue}{0.011111111111111112} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 11: 68.3% accurate, 3.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(a\_m + b\_m\right) \cdot \left(\sin \left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b\_m - a\_m\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (+ a_m b_m) (* (sin (* 2.0 (/ (* angle (PI)) 180.0))) (- b_m a_m))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

   4. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   5. *-commutative N/A

      \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   6. associate-*l* N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   7. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   8. lift--.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   9. lift-pow.f64 N/A

      \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   10. unpow2 N/A

       \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   11. lift-pow.f64 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   12. unpow2 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   13. difference-of-squares N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   14. lower-*.f64 N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   15. lower-+.f64 N/A

       \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   16. lower--.f64 N/A

       \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

4. Applied rewrites 57.1%

   \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   4. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   5. lift-+.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   6. +-commutative N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   7. lower-+.f64 N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   8. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   9. lower-*.f64 66.5

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

6. Applied rewrites 66.5%

   \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
7. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

   2. lift-/.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

   3. associate-*r/ N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

   4. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

   5. lower-/.f64 66.9

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

   6. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

   7. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. lower-*.f64 66.9

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

8. Applied rewrites 66.9%

   \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
9. Add Preprocessing

Alternative 12: 68.1% accurate, 3.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(a\_m + b\_m\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b\_m - a\_m\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (+ a_m b_m) (* (sin (* 2.0 (* (PI) (/ angle 180.0)))) (- b_m a_m))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

   4. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   5. *-commutative N/A

      \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   6. associate-*l* N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   7. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   8. lift--.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   9. lift-pow.f64 N/A

      \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   10. unpow2 N/A

       \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   11. lift-pow.f64 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   12. unpow2 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   13. difference-of-squares N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   14. lower-*.f64 N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   15. lower-+.f64 N/A

       \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   16. lower--.f64 N/A

       \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

4. Applied rewrites 57.1%

   \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   4. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   5. lift-+.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   6. +-commutative N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   7. lower-+.f64 N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   8. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   9. lower-*.f64 66.5

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

6. Applied rewrites 66.5%

   \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
7. Add Preprocessing

Alternative 13: 68.2% accurate, 3.3× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(a\_m + b\_m\right) \cdot \left(\sin \left(\frac{\mathsf{PI}\left(\right)}{180} \cdot \left(angle + angle\right)\right) \cdot \left(b\_m - a\_m\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (+ a_m b_m) (* (sin (* (/ (PI) 180.0) (+ angle angle))) (- b_m a_m))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

   4. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   5. *-commutative N/A

      \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   6. associate-*l* N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   7. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   8. lift--.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   9. lift-pow.f64 N/A

      \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   10. unpow2 N/A

       \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   11. lift-pow.f64 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   12. unpow2 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   13. difference-of-squares N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   14. lower-*.f64 N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   15. lower-+.f64 N/A

       \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   16. lower--.f64 N/A

       \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

4. Applied rewrites 57.1%

   \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   4. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   5. lift-+.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   6. +-commutative N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   7. lower-+.f64 N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   8. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   9. lower-*.f64 66.5

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

6. Applied rewrites 66.5%

   \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]
7. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)}\right) \cdot \left(b - a\right)\right) \]

   2. lift-/.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{angle}{180}}\right)\right) \cdot \left(b - a\right)\right) \]

   3. associate-*r/ N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

   4. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

   5. lower-/.f64 66.9

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{\mathsf{PI}\left(\right) \cdot angle}{180}}\right) \cdot \left(b - a\right)\right) \]

   6. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right) \cdot angle}}{180}\right) \cdot \left(b - a\right)\right) \]

   7. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. lower-*.f64 66.9

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

8. Applied rewrites 66.9%

   \[\leadsto \left(a + b\right) \cdot \left(\sin \left(2 \cdot \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]
9. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(2 \cdot \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right)} \cdot \left(b - a\right)\right) \]

   2. count-2-rev N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\frac{angle \cdot \mathsf{PI}\left(\right)}{180} + \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right)} \cdot \left(b - a\right)\right) \]

   3. lift-/.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}} + \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b - a\right)\right) \]

   4. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180} + \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b - a\right)\right) \]

   5. associate-/l* N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\color{blue}{angle \cdot \frac{\mathsf{PI}\left(\right)}{180}} + \frac{angle \cdot \mathsf{PI}\left(\right)}{180}\right) \cdot \left(b - a\right)\right) \]

   6. lift-/.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(angle \cdot \frac{\mathsf{PI}\left(\right)}{180} + \color{blue}{\frac{angle \cdot \mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]

   7. lift-*.f64 N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(angle \cdot \frac{\mathsf{PI}\left(\right)}{180} + \frac{\color{blue}{angle \cdot \mathsf{PI}\left(\right)}}{180}\right) \cdot \left(b - a\right)\right) \]

   8. associate-/l* N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \left(angle \cdot \frac{\mathsf{PI}\left(\right)}{180} + \color{blue}{angle \cdot \frac{\mathsf{PI}\left(\right)}{180}}\right) \cdot \left(b - a\right)\right) \]

   9. distribute-rgt-out N/A

      \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{180} \cdot \left(angle + angle\right)\right)} \cdot \left(b - a\right)\right) \]

   10. lower-*.f64 N/A

       \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{180} \cdot \left(angle + angle\right)\right)} \cdot \left(b - a\right)\right) \]

   11. lower-/.f64 N/A

       \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\color{blue}{\frac{\mathsf{PI}\left(\right)}{180}} \cdot \left(angle + angle\right)\right) \cdot \left(b - a\right)\right) \]

   12. lower-+.f64 65.9

       \[\leadsto \left(a + b\right) \cdot \left(\sin \left(\frac{\mathsf{PI}\left(\right)}{180} \cdot \color{blue}{\left(angle + angle\right)}\right) \cdot \left(b - a\right)\right) \]

10. Applied rewrites 65.9%

    \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\frac{\mathsf{PI}\left(\right)}{180} \cdot \left(angle + angle\right)\right)} \cdot \left(b - a\right)\right) \]
11. Add Preprocessing

Alternative 14: 64.5% accurate, 3.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} \mathbf{if}\;a\_m \leq 5.4 \cdot 10^{-124}:\\ \;\;\;\;\sin \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot 0.011111111111111112\right) \cdot \left(b\_m \cdot b\_m\right)\\ \mathbf{else}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (if (<= a_m 5.4e-124)
   (* (sin (* (* (PI) angle) 0.011111111111111112)) (* b_m b_m))
   (* (+ a_m b_m) (* (- b_m a_m) (* (* 0.011111111111111112 (PI)) angle)))))

Derivation

1. Split input into 2 regimes

2. if a < 5.40000000000000035e-124

   1. Initial program 55.9%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing
   3. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

      4. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      5. *-commutative N/A

         \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

      6. associate-*l* N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      7. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

      8. lift--.f64 N/A

         \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      9. lift-pow.f64 N/A

         \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      10. unpow2 N/A

          \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      11. lift-pow.f64 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      12. unpow2 N/A

          \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      13. difference-of-squares N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      14. lower-*.f64 N/A

          \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      15. lower-+.f64 N/A

          \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

      16. lower--.f64 N/A

          \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   4. Applied rewrites 58.4%

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

      2. lift-*.f64 N/A

         \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

      3. associate-*l* N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      4. lower-*.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

      5. lift-+.f64 N/A

         \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      6. +-commutative N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      7. lower-+.f64 N/A

         \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

      9. lower-*.f64 68.2

         \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   6. Applied rewrites 68.2%

      \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

   7. Taylor expanded in a around 0

      \[\leadsto \color{blue}{{b}^{2} \cdot \sin \left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
   8. Step-by-step derivation

   9. Applied rewrites 40.6%

      \[\leadsto \color{blue}{\sin \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot 0.011111111111111112\right) \cdot \left(b \cdot b\right)} \]

   if 5.40000000000000035e-124 < a

   1. Initial program 51.4%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 52.5%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 61.4%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 15: 68.2% accurate, 3.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(a\_m + b\_m\right) \cdot \left(\sin \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot 0.011111111111111112\right) \cdot \left(b\_m - a\_m\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (+ a_m b_m) (* (sin (* (* (PI) angle) 0.011111111111111112)) (- b_m a_m))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)} \]

   4. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   5. *-commutative N/A

      \[\leadsto \color{blue}{\left(\left({b}^{2} - {a}^{2}\right) \cdot 2\right)} \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \]

   6. associate-*l* N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   7. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right)} \]

   8. lift--.f64 N/A

      \[\leadsto \color{blue}{\left({b}^{2} - {a}^{2}\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   9. lift-pow.f64 N/A

      \[\leadsto \left(\color{blue}{{b}^{2}} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   10. unpow2 N/A

       \[\leadsto \left(\color{blue}{b \cdot b} - {a}^{2}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   11. lift-pow.f64 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{{a}^{2}}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   12. unpow2 N/A

       \[\leadsto \left(b \cdot b - \color{blue}{a \cdot a}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   13. difference-of-squares N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   14. lower-*.f64 N/A

       \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   15. lower-+.f64 N/A

       \[\leadsto \left(\color{blue}{\left(b + a\right)} \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

   16. lower--.f64 N/A

       \[\leadsto \left(\left(b + a\right) \cdot \color{blue}{\left(b - a\right)}\right) \cdot \left(2 \cdot \left(\sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right)\right) \]

4. Applied rewrites 57.1%

   \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]
5. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)} \]

   2. lift-*.f64 N/A

      \[\leadsto \color{blue}{\left(\left(b + a\right) \cdot \left(b - a\right)\right)} \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \]

   3. associate-*l* N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   4. lower-*.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right) \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right)} \]

   5. lift-+.f64 N/A

      \[\leadsto \color{blue}{\left(b + a\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   6. +-commutative N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   7. lower-+.f64 N/A

      \[\leadsto \color{blue}{\left(a + b\right)} \cdot \left(\left(b - a\right) \cdot \left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right)\right) \]

   8. *-commutative N/A

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

   9. lower-*.f64 66.5

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(2 \cdot \left(\cos \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right) \cdot \sin \left(\frac{angle}{180} \cdot \mathsf{PI}\left(\right)\right)\right)\right) \cdot \left(b - a\right)\right)} \]

6. Applied rewrites 66.5%

   \[\leadsto \color{blue}{\left(a + b\right) \cdot \left(\sin \left(2 \cdot \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \left(b - a\right)\right)} \]

7. Taylor expanded in angle around 0

   \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\frac{1}{90} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot \left(b - a\right)\right) \]
8. Step-by-step derivation

9. Applied rewrites 65.6%

   \[\leadsto \left(a + b\right) \cdot \left(\sin \color{blue}{\left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot 0.011111111111111112\right)} \cdot \left(b - a\right)\right) \]
10. Add Preprocessing

Alternative 16: 64.6% accurate, 13.7× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \begin{array}{l} t_0 := 0.011111111111111112 \cdot \mathsf{PI}\left(\right)\\ \mathbf{if}\;angle \leq 5.5 \cdot 10^{-35}:\\ \;\;\;\;\left(a\_m + b\_m\right) \cdot \left(\left(b\_m - a\_m\right) \cdot \left(t\_0 \cdot angle\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(t\_0 \cdot \left(\left(b\_m - a\_m\right) \cdot \left(a\_m + b\_m\right)\right)\right) \cdot angle\\ \end{array} \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (let* ((t_0 (* 0.011111111111111112 (PI))))
   (if (<= angle 5.5e-35)
     (* (+ a_m b_m) (* (- b_m a_m) (* t_0 angle)))
     (* (* t_0 (* (- b_m a_m) (+ a_m b_m))) angle))))

Derivation

1. Split input into 2 regimes

2. if angle < 5.4999999999999997e-35

   1. Initial program 60.8%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 72.7%

      \[\leadsto \left(a + b\right) \cdot \color{blue}{\left(\left(b - a\right) \cdot \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot angle\right)\right)} \]

   if 5.4999999999999997e-35 < angle

   1. Initial program 37.1%

      \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
   2. Add Preprocessing

   3. Taylor expanded in angle around 0

      \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
   4. Step-by-step derivation

   5. Applied rewrites 32.4%

      \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]
   6. Step-by-step derivation

   7. Applied rewrites 32.4%

      \[\leadsto \left(\left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right) \cdot \left(\left(b - a\right) \cdot \left(a + b\right)\right)\right) \cdot \color{blue}{angle} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 17: 39.8% accurate, 21.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(a\_m \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\_m\right)\right) \cdot -0.011111111111111112 \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (* a_m (* (* (PI) angle) a_m)) -0.011111111111111112))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing

3. Taylor expanded in angle around 0

   \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
4. Step-by-step derivation

5. Applied rewrites 52.9%

   \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

6. Taylor expanded in a around inf

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

8. Applied rewrites 33.1%

   \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
9. Step-by-step derivation

10. Applied rewrites 33.1%

    \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]

11. Taylor expanded in a around inf

    \[\leadsto \frac{-1}{90} \cdot \color{blue}{\left({a}^{2} \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right)} \]
12. Step-by-step derivation

13. Applied rewrites 37.5%

    \[\leadsto \left(a \cdot \left(\left(\mathsf{PI}\left(\right) \cdot angle\right) \cdot a\right)\right) \cdot \color{blue}{-0.011111111111111112} \]
14. Add Preprocessing

Alternative 18: 39.8% accurate, 21.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ \left(-0.011111111111111112 \cdot a\_m\right) \cdot \left(a\_m \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* (* -0.011111111111111112 a_m) (* a_m (* (PI) angle))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing

3. Taylor expanded in angle around 0

   \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
4. Step-by-step derivation

5. Applied rewrites 52.9%

   \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

6. Taylor expanded in a around inf

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

8. Applied rewrites 33.1%

   \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
9. Step-by-step derivation

10. Applied rewrites 33.1%

    \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]
11. Step-by-step derivation

12. Applied rewrites 37.5%

    \[\leadsto \left(-0.011111111111111112 \cdot a\right) \cdot \left(a \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)}\right) \]
13. Add Preprocessing

Alternative 19: 39.8% accurate, 21.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ a\_m \cdot \left(\left(a\_m \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot -0.011111111111111112\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* a_m (* (* a_m (* (PI) angle)) -0.011111111111111112)))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing

3. Taylor expanded in angle around 0

   \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
4. Step-by-step derivation

5. Applied rewrites 52.9%

   \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

6. Taylor expanded in a around inf

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

8. Applied rewrites 33.1%

   \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
9. Step-by-step derivation

10. Applied rewrites 33.1%

    \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]
11. Step-by-step derivation

12. Applied rewrites 37.5%

    \[\leadsto a \cdot \left(\left(a \cdot \left(\mathsf{PI}\left(\right) \cdot angle\right)\right) \cdot \color{blue}{-0.011111111111111112}\right) \]
13. Add Preprocessing

Alternative 20: 36.0% accurate, 21.6× speedup

Math

\[\begin{array}{l} a_m = \left|a\right| \\ b_m = \left|b\right| \\ -0.011111111111111112 \cdot \left(\left(a\_m \cdot a\_m\right) \cdot \left(angle \cdot \mathsf{PI}\left(\right)\right)\right) \end{array} \]

FPCore

a_m = (fabs.f64 a)
b_m = (fabs.f64 b)
(FPCore (a_m b_m angle)
 :precision binary64
 (* -0.011111111111111112 (* (* a_m a_m) (* angle (PI)))))

Derivation

1. Initial program 54.2%

   \[\left(\left(2 \cdot \left({b}^{2} - {a}^{2}\right)\right) \cdot \sin \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right)\right) \cdot \cos \left(\mathsf{PI}\left(\right) \cdot \frac{angle}{180}\right) \]
2. Add Preprocessing

3. Taylor expanded in angle around 0

   \[\leadsto \color{blue}{\frac{1}{90} \cdot \left(angle \cdot \left(\mathsf{PI}\left(\right) \cdot \left({b}^{2} - {a}^{2}\right)\right)\right)} \]
4. Step-by-step derivation

5. Applied rewrites 52.9%

   \[\leadsto \color{blue}{\left(angle \cdot \left(0.011111111111111112 \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\left(b + a\right) \cdot \left(b - a\right)\right)} \]

6. Taylor expanded in a around inf

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

8. Applied rewrites 33.1%

   \[\leadsto \left(-0.011111111111111112 \cdot \left(a \cdot a\right)\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot angle\right)} \]
9. Step-by-step derivation

10. Applied rewrites 33.1%

    \[\leadsto -0.011111111111111112 \cdot \left(\left(a \cdot a\right) \cdot \color{blue}{\left(angle \cdot \mathsf{PI}\left(\right)\right)}\right) \]
11. Add Preprocessing

Reproduce

herbie shell --seed 2025025 
(FPCore (a b angle)
  :name "ab-angle->ABCF B"
  :precision binary64
  (* (* (* 2.0 (- (pow b 2.0) (pow a 2.0))) (sin (* (PI) (/ angle 180.0)))) (cos (* (PI) (/ angle 180.0)))))