ABCF->ab-angle angle

Percentage Accurate: 53.1% → 81.3%
Time: 7.5s
Alternatives: 15
Speedup: 2.6×

Specification

?
\[\begin{array}{l} \\ 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (*
  180.0
  (/
   (atan (* (/ 1.0 B) (- (- C A) (sqrt (+ (pow (- A C) 2.0) (pow B 2.0))))))
   (PI))))
\begin{array}{l}

\\
180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 15 alternatives:

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

Initial Program: 53.1% accurate, 1.0× speedup?

\[\begin{array}{l} \\ 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (*
  180.0
  (/
   (atan (* (/ 1.0 B) (- (- C A) (sqrt (+ (pow (- A C) 2.0) (pow B 2.0))))))
   (PI))))
\begin{array}{l}

\\
180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}
\end{array}

Alternative 1: 81.3% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\ \mathbf{if}\;A \leq -5.8 \cdot 10^{+134}:\\ \;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot t\_0\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (let* ((t_0 (/ 180.0 (PI))))
   (if (<= A -5.8e+134)
     (* t_0 (atan (* (/ B A) 0.5)))
     (* (atan (/ (- (- C A) (hypot (- A C) B)) B)) t_0))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\
\mathbf{if}\;A \leq -5.8 \cdot 10^{+134}:\\
\;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{else}:\\
\;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot t\_0\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if A < -5.80000000000000023e134

    1. Initial program 7.6%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6482.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites82.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6482.6

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites82.6%

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

    if -5.80000000000000023e134 < A

    1. Initial program 64.0%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      2. metadata-evalN/A

        \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      4. times-fracN/A

        \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
      7. /-rgt-identityN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      8. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      9. lower-/.f6464.0

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
      10. lift-*.f64N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      11. *-commutativeN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
    4. Applied rewrites85.1%

      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification84.6%

    \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -5.8 \cdot 10^{+134}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 72.2% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \tan^{-1} \left(\left(\left(C - A\right) - \sqrt{{B}^{2} + {\left(A - C\right)}^{2}}\right) \cdot \frac{1}{B}\right)\\ t_1 := \frac{C - A}{B}\\ \mathbf{if}\;t\_0 \leq -0.5:\\ \;\;\;\;\frac{\tan^{-1} \left(t\_1 - 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;t\_0 \leq 0:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(t\_1 + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (let* ((t_0
         (atan
          (* (- (- C A) (sqrt (+ (pow B 2.0) (pow (- A C) 2.0)))) (/ 1.0 B))))
        (t_1 (/ (- C A) B)))
   (if (<= t_0 -0.5)
     (* (/ (atan (- t_1 1.0)) (PI)) 180.0)
     (if (<= t_0 0.0)
       (* (/ 180.0 (PI)) (atan (* (/ B A) 0.5)))
       (* (/ (atan (+ t_1 1.0)) (PI)) 180.0)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \tan^{-1} \left(\left(\left(C - A\right) - \sqrt{{B}^{2} + {\left(A - C\right)}^{2}}\right) \cdot \frac{1}{B}\right)\\
t_1 := \frac{C - A}{B}\\
\mathbf{if}\;t\_0 \leq -0.5:\\
\;\;\;\;\frac{\tan^{-1} \left(t\_1 - 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\

\mathbf{elif}\;t\_0 \leq 0:\\
\;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(t\_1 + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (atan.f64 (*.f64 (/.f64 #s(literal 1 binary64) B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) #s(literal 2 binary64)) (pow.f64 B #s(literal 2 binary64))))))) < -0.5

    1. Initial program 60.5%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C}{B} - \left(1 + \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{C}{B} - \color{blue}{\left(\frac{A}{B} + 1\right)}\right)}{\mathsf{PI}\left(\right)} \]
      2. associate--r+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(\frac{C}{B} - \frac{A}{B}\right) - 1\right)}}{\mathsf{PI}\left(\right)} \]
      3. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right)} \]
      4. lower--.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} - 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6470.8

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} - 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites70.8%

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

    if -0.5 < (atan.f64 (*.f64 (/.f64 #s(literal 1 binary64) B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) #s(literal 2 binary64)) (pow.f64 B #s(literal 2 binary64))))))) < -0.0

    1. Initial program 18.0%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6451.0

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites51.0%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6451.2

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites51.2%

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

    if -0.0 < (atan.f64 (*.f64 (/.f64 #s(literal 1 binary64) B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) #s(literal 2 binary64)) (pow.f64 B #s(literal 2 binary64)))))))

    1. Initial program 56.1%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. associate--l+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
      2. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      4. lower-+.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6471.7

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites71.7%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification69.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\tan^{-1} \left(\left(\left(C - A\right) - \sqrt{{B}^{2} + {\left(A - C\right)}^{2}}\right) \cdot \frac{1}{B}\right) \leq -0.5:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} - 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;\tan^{-1} \left(\left(\left(C - A\right) - \sqrt{{B}^{2} + {\left(A - C\right)}^{2}}\right) \cdot \frac{1}{B}\right) \leq 0:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 75.3% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (if (<= A -5.2e+131)
   (* (/ 180.0 (PI)) (atan (* (/ B A) 0.5)))
   (if (<= A 2.4e+42)
     (/ (atan (/ (- C (hypot B C)) B)) (* 0.005555555555555556 (PI)))
     (* (/ (atan (+ (/ (- C A) B) 1.0)) (PI)) 180.0))))
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\
\;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if A < -5.2e131

    1. Initial program 7.6%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6482.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites82.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6482.6

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites82.6%

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

    if -5.2e131 < A < 2.3999999999999999e42

    1. Initial program 57.1%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      2. metadata-evalN/A

        \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      4. times-fracN/A

        \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
      7. /-rgt-identityN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      8. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      9. lower-/.f6457.1

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
      10. lift-*.f64N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      11. *-commutativeN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
    4. Applied rewrites80.5%

      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
      3. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      4. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      5. un-div-invN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. lift-hypot.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      8. +-commutativeN/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      9. lower-hypot.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      10. div-invN/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      11. lower-*.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      12. metadata-eval80.5

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
    7. Taylor expanded in A around 0

      \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
    8. Step-by-step derivation
      1. lower--.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      2. unpow2N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      3. unpow2N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      4. lower-hypot.f6478.2

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
    9. Applied rewrites78.2%

      \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]

    if 2.3999999999999999e42 < A

    1. Initial program 83.8%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. associate--l+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
      2. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      4. lower-+.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6489.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites89.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification81.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
  5. Add Preprocessing

Alternative 4: 75.3% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\ \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right) \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (let* ((t_0 (/ 180.0 (PI))))
   (if (<= A -5.2e+131)
     (* t_0 (atan (* (/ B A) 0.5)))
     (if (<= A 2.4e+42)
       (* (atan (/ (- C (hypot B C)) B)) t_0)
       (* (/ (atan (+ (/ (- C A) B) 1.0)) (PI)) 180.0)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\
\mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\
\;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\
\;\;\;\;\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right) \cdot t\_0\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if A < -5.2e131

    1. Initial program 7.6%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6482.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites82.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6482.6

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites82.6%

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

    if -5.2e131 < A < 2.3999999999999999e42

    1. Initial program 57.1%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      2. metadata-evalN/A

        \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      4. times-fracN/A

        \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
      7. /-rgt-identityN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      8. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      9. lower-/.f6457.1

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
      10. lift-*.f64N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      11. *-commutativeN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
    4. Applied rewrites80.5%

      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
    5. Taylor expanded in A around 0

      \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right) \]
    6. Step-by-step derivation
      1. lower--.f64N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right) \]
      2. unpow2N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right) \]
      3. unpow2N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right) \]
      4. lower-hypot.f6478.2

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right) \]
    7. Applied rewrites78.2%

      \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right) \]

    if 2.3999999999999999e42 < A

    1. Initial program 83.8%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. associate--l+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
      2. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      4. lower-+.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6489.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites89.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification81.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(B, C\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
  5. Add Preprocessing

Alternative 5: 75.3% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(C, B\right)}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (if (<= A -5.2e+131)
   (* (/ 180.0 (PI)) (atan (* (/ B A) 0.5)))
   (if (<= A 2.4e+42)
     (* (/ (atan (/ (- C (hypot C B)) B)) (PI)) 180.0)
     (* (/ (atan (+ (/ (- C A) B) 1.0)) (PI)) 180.0))))
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\
\;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(C, B\right)}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if A < -5.2e131

    1. Initial program 7.6%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6482.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites82.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6482.6

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites82.6%

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

    if -5.2e131 < A < 2.3999999999999999e42

    1. Initial program 57.1%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around 0

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - \sqrt{{B}^{2} + {C}^{2}}}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - \sqrt{{B}^{2} + {C}^{2}}}{B}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower--.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{{C}^{2} + {B}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right)} \]
      4. unpow2N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{C \cdot C} + {B}^{2}}}{B}\right)}{\mathsf{PI}\left(\right)} \]
      5. unpow2N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{C - \sqrt{C \cdot C + \color{blue}{B \cdot B}}}{B}\right)}{\mathsf{PI}\left(\right)} \]
      6. lower-hypot.f6478.2

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(C, B\right)}}{B}\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites78.2%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - \mathsf{hypot}\left(C, B\right)}{B}\right)}}{\mathsf{PI}\left(\right)} \]

    if 2.3999999999999999e42 < A

    1. Initial program 83.8%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. associate--l+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
      2. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      4. lower-+.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6489.4

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites89.4%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification81.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -5.2 \cdot 10^{+131}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.4 \cdot 10^{+42}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - \mathsf{hypot}\left(C, B\right)}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
  5. Add Preprocessing

Alternative 6: 63.3% accurate, 2.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\ \mathbf{if}\;A \leq -3.4 \cdot 10^{-11}:\\ \;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.16 \cdot 10^{-44}:\\ \;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}}{B}\right) \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (let* ((t_0 (/ 180.0 (PI))))
   (if (<= A -3.4e-11)
     (* t_0 (atan (* (/ B A) 0.5)))
     (if (<= A 2.16e-44)
       (* (atan (/ (- (- C A) (sqrt (fma C C (* B B)))) B)) t_0)
       (* (/ (atan (+ (/ (- C A) B) 1.0)) (PI)) 180.0)))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{180}{\mathsf{PI}\left(\right)}\\
\mathbf{if}\;A \leq -3.4 \cdot 10^{-11}:\\
\;\;\;\;t\_0 \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{elif}\;A \leq 2.16 \cdot 10^{-44}:\\
\;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}}{B}\right) \cdot t\_0\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if A < -3.3999999999999999e-11

    1. Initial program 18.9%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6470.5

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites70.5%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6470.7

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites70.7%

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

    if -3.3999999999999999e-11 < A < 2.15999999999999988e-44

    1. Initial program 58.9%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around 0

      \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\color{blue}{{B}^{2} + {C}^{2}}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\color{blue}{{C}^{2} + {B}^{2}}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      2. unpow2N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\color{blue}{C \cdot C} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      3. lower-fma.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\color{blue}{\mathsf{fma}\left(C, C, {B}^{2}\right)}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      4. unpow2N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, \color{blue}{B \cdot B}\right)}\right)\right)}{\mathsf{PI}\left(\right)} \]
      5. lower-*.f6458.9

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, \color{blue}{B \cdot B}\right)}\right)\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites58.9%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\color{blue}{\mathsf{fma}\left(C, C, B \cdot B\right)}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. div-invN/A

        \[\leadsto \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \frac{1}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      8. metadata-evalN/A

        \[\leadsto \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \frac{1}{\mathsf{PI}\left(\right) \cdot \color{blue}{\frac{1}{180}}} \]
      9. lift-*.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \frac{1}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      10. lower-*.f64N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}\right)\right) \cdot \frac{1}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
    7. Applied rewrites58.9%

      \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]

    if 2.15999999999999988e-44 < A

    1. Initial program 81.3%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in B around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. associate--l+N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
      2. div-subN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
      3. +-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      4. lower-+.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
      5. lower-/.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
      6. lower--.f6488.2

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites88.2%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification69.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -3.4 \cdot 10^{-11}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 2.16 \cdot 10^{-44}:\\ \;\;\;\;\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\mathsf{fma}\left(C, C, B \cdot B\right)}}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
  5. Add Preprocessing

Alternative 7: 61.0% accurate, 2.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq -1.6 \cdot 10^{-104}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
(FPCore (A B C)
 :precision binary64
 (if (<= A -2.9e-11)
   (* (/ 180.0 (PI)) (atan (* (/ B A) 0.5)))
   (if (<= A -1.6e-104)
     (/ (atan (/ (- C B) B)) (* 0.005555555555555556 (PI)))
     (* (/ (atan (+ (/ (- C A) B) 1.0)) (PI)) 180.0))))
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\
\;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\

\mathbf{elif}\;A \leq -1.6 \cdot 10^{-104}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if A < -2.9e-11

    1. Initial program 18.9%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Taylor expanded in A around -inf

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      2. lower-*.f64N/A

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
      3. lower-/.f6470.5

        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
    5. Applied rewrites70.5%

      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
    6. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
      3. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
      4. div-invN/A

        \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
      6. associate-/r/N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      8. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      9. lower-*.f6470.7

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
    7. Applied rewrites70.7%

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

    if -2.9e-11 < A < -1.59999999999999994e-104

    1. Initial program 55.4%

      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      2. metadata-evalN/A

        \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      3. lift-/.f64N/A

        \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
      4. times-fracN/A

        \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
      6. times-fracN/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
      7. /-rgt-identityN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      8. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      9. lower-/.f6455.4

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
      10. lift-*.f64N/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
      11. *-commutativeN/A

        \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
    4. Applied rewrites76.6%

      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
    5. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
      3. lift-/.f64N/A

        \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
      4. clear-numN/A

        \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      5. un-div-invN/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
      7. lift-hypot.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      8. +-commutativeN/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      9. lower-hypot.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
      10. div-invN/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      11. lower-*.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
      12. metadata-eval76.6

        \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
    6. Applied rewrites76.6%

      \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
    7. Taylor expanded in A around 0

      \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
    8. Step-by-step derivation
      1. lower--.f64N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      2. unpow2N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      3. unpow2N/A

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      4. lower-hypot.f6476.7

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
    9. Applied rewrites76.7%

      \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
    10. Taylor expanded in C around 0

      \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
    11. Step-by-step derivation
      1. Applied rewrites61.7%

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

      if -1.59999999999999994e-104 < A

      1. Initial program 68.4%

        \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in B around -inf

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\left(1 + \frac{C}{B}\right) - \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
      4. Step-by-step derivation
        1. associate--l+N/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(1 + \left(\frac{C}{B} - \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right)} \]
        2. div-subN/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \left(1 + \color{blue}{\frac{C - A}{B}}\right)}{\mathsf{PI}\left(\right)} \]
        3. +-commutativeN/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
        4. lower-+.f64N/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
        5. lower-/.f64N/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} + 1\right)}{\mathsf{PI}\left(\right)} \]
        6. lower--.f6466.9

          \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} + 1\right)}{\mathsf{PI}\left(\right)} \]
      5. Applied rewrites66.9%

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} + 1\right)}}{\mathsf{PI}\left(\right)} \]
    12. Recombined 3 regimes into one program.
    13. Final simplification67.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq -1.6 \cdot 10^{-104}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - A}{B} + 1\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
    14. Add Preprocessing

    Alternative 8: 56.0% accurate, 2.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
    (FPCore (A B C)
     :precision binary64
     (if (<= A -2.9e-11)
       (* (/ 180.0 (PI)) (atan (* (/ B A) 0.5)))
       (if (<= A 9e-39)
         (/ (atan (/ (- C B) B)) (* 0.005555555555555556 (PI)))
         (* (/ (atan (* -2.0 (/ A B))) (PI)) 180.0))))
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\
    \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\
    
    \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\
    \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\
    
    \mathbf{else}:\\
    \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if A < -2.9e-11

      1. Initial program 18.9%

        \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Taylor expanded in A around -inf

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
        2. lower-*.f64N/A

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
        3. lower-/.f6470.5

          \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
      5. Applied rewrites70.5%

        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot 0.5\right)}}{\mathsf{PI}\left(\right)} \]
      6. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \]
        2. *-commutativeN/A

          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)} \cdot 180} \]
        3. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right)}{\mathsf{PI}\left(\right)}} \cdot 180 \]
        4. div-invN/A

          \[\leadsto \color{blue}{\left(\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \frac{1}{\mathsf{PI}\left(\right)}\right)} \cdot 180 \]
        5. associate-*l*N/A

          \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \left(\frac{1}{\mathsf{PI}\left(\right)} \cdot 180\right)} \]
        6. associate-/r/N/A

          \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
        7. clear-numN/A

          \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
        8. lift-/.f64N/A

          \[\leadsto \tan^{-1} \left(\frac{B}{A} \cdot \frac{1}{2}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
        9. lower-*.f6470.7

          \[\leadsto \color{blue}{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
      7. Applied rewrites70.7%

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

      if -2.9e-11 < A < 9.0000000000000002e-39

      1. Initial program 58.5%

        \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
        2. metadata-evalN/A

          \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
        3. lift-/.f64N/A

          \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
        4. times-fracN/A

          \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
        5. *-commutativeN/A

          \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
        6. times-fracN/A

          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
        7. /-rgt-identityN/A

          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
        8. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
        9. lower-/.f6458.5

          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
        10. lift-*.f64N/A

          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
        11. *-commutativeN/A

          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
      4. Applied rewrites82.4%

        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
      5. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
        2. *-commutativeN/A

          \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
        3. lift-/.f64N/A

          \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
        4. clear-numN/A

          \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
        5. un-div-invN/A

          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
        6. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
        7. lift-hypot.f64N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
        8. +-commutativeN/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
        9. lower-hypot.f64N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
        10. div-invN/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
        11. lower-*.f64N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
        12. metadata-eval82.4

          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
      6. Applied rewrites82.4%

        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
      7. Taylor expanded in A around 0

        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      8. Step-by-step derivation
        1. lower--.f64N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
        2. unpow2N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
        3. unpow2N/A

          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
        4. lower-hypot.f6480.1

          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
      9. Applied rewrites80.1%

        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
      10. Taylor expanded in C around 0

        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
      11. Step-by-step derivation
        1. Applied rewrites48.2%

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

        if 9.0000000000000002e-39 < A

        1. Initial program 82.5%

          \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in A around inf

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(-2 \cdot \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
          2. lower-*.f64N/A

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
          3. lower-/.f6471.1

            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{A}{B}} \cdot -2\right)}{\mathsf{PI}\left(\right)} \]
        5. Applied rewrites71.1%

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
      12. Recombined 3 regimes into one program.
      13. Final simplification60.0%

        \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -2.9 \cdot 10^{-11}:\\ \;\;\;\;\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)\\ \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
      14. Add Preprocessing

      Alternative 9: 56.0% accurate, 2.5× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;A \leq -2.55 \cdot 10^{-11}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
      (FPCore (A B C)
       :precision binary64
       (if (<= A -2.55e-11)
         (* (/ (atan (* (/ B A) 0.5)) (PI)) 180.0)
         (if (<= A 9e-39)
           (/ (atan (/ (- C B) B)) (* 0.005555555555555556 (PI)))
           (* (/ (atan (* -2.0 (/ A B))) (PI)) 180.0))))
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;A \leq -2.55 \cdot 10^{-11}:\\
      \;\;\;\;\frac{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \cdot 180\\
      
      \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\
      \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if A < -2.54999999999999992e-11

        1. Initial program 18.9%

          \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Taylor expanded in A around -inf

          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{1}{2} \cdot \frac{B}{A}\right)}}{\mathsf{PI}\left(\right)} \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
          2. lower-*.f64N/A

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{B}{A} \cdot \frac{1}{2}\right)}}{\mathsf{PI}\left(\right)} \]
          3. lower-/.f6470.5

            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{A}} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \]
        5. Applied rewrites70.5%

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

        if -2.54999999999999992e-11 < A < 9.0000000000000002e-39

        1. Initial program 58.5%

          \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
          2. metadata-evalN/A

            \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
          3. lift-/.f64N/A

            \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
          4. times-fracN/A

            \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
          5. *-commutativeN/A

            \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
          6. times-fracN/A

            \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
          7. /-rgt-identityN/A

            \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
          8. lower-*.f64N/A

            \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
          9. lower-/.f6458.5

            \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
          10. lift-*.f64N/A

            \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
          11. *-commutativeN/A

            \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
        4. Applied rewrites82.4%

          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
        5. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
          2. *-commutativeN/A

            \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
          3. lift-/.f64N/A

            \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
          4. clear-numN/A

            \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
          5. un-div-invN/A

            \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
          6. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
          7. lift-hypot.f64N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
          8. +-commutativeN/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
          9. lower-hypot.f64N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
          10. div-invN/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
          11. lower-*.f64N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
          12. metadata-eval82.4

            \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
        6. Applied rewrites82.4%

          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
        7. Taylor expanded in A around 0

          \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
        8. Step-by-step derivation
          1. lower--.f64N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
          2. unpow2N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
          3. unpow2N/A

            \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
          4. lower-hypot.f6480.1

            \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
        9. Applied rewrites80.1%

          \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
        10. Taylor expanded in C around 0

          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
        11. Step-by-step derivation
          1. Applied rewrites48.2%

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

          if 9.0000000000000002e-39 < A

          1. Initial program 82.5%

            \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
          2. Add Preprocessing
          3. Taylor expanded in A around inf

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(-2 \cdot \frac{A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
          4. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
            2. lower-*.f64N/A

              \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
            3. lower-/.f6471.1

              \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{A}{B}} \cdot -2\right)}{\mathsf{PI}\left(\right)} \]
          5. Applied rewrites71.1%

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{A}{B} \cdot -2\right)}}{\mathsf{PI}\left(\right)} \]
        12. Recombined 3 regimes into one program.
        13. Final simplification59.9%

          \[\leadsto \begin{array}{l} \mathbf{if}\;A \leq -2.55 \cdot 10^{-11}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{B}{A} \cdot 0.5\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;A \leq 9 \cdot 10^{-39}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(-2 \cdot \frac{A}{B}\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
        14. Add Preprocessing

        Alternative 10: 51.0% accurate, 2.5× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} t_0 := 0.005555555555555556 \cdot \mathsf{PI}\left(\right)\\ \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 4 \cdot 10^{-244}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{t\_0}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{t\_0}\\ \end{array} \end{array} \]
        (FPCore (A B C)
         :precision binary64
         (let* ((t_0 (* 0.005555555555555556 (PI))))
           (if (<= B -4.3e-147)
             (* (/ (atan 1.0) (PI)) 180.0)
             (if (<= B 4e-244)
               (/ (atan (/ (- A) B)) t_0)
               (/ (atan (/ (- C B) B)) t_0)))))
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        t_0 := 0.005555555555555556 \cdot \mathsf{PI}\left(\right)\\
        \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\
        \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\
        
        \mathbf{elif}\;B \leq 4 \cdot 10^{-244}:\\
        \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{t\_0}\\
        
        \mathbf{else}:\\
        \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{t\_0}\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 3 regimes
        2. if B < -4.3000000000000001e-147

          1. Initial program 49.8%

            \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
          2. Add Preprocessing
          3. Taylor expanded in B around -inf

            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{1}}{\mathsf{PI}\left(\right)} \]
          4. Step-by-step derivation
            1. Applied rewrites53.1%

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

            if -4.3000000000000001e-147 < B < 3.9999999999999997e-244

            1. Initial program 57.3%

              \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
              2. metadata-evalN/A

                \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
              3. lift-/.f64N/A

                \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
              4. times-fracN/A

                \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
              5. *-commutativeN/A

                \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
              6. times-fracN/A

                \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
              7. /-rgt-identityN/A

                \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
              8. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
              9. lower-/.f6457.3

                \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
              10. lift-*.f64N/A

                \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
              11. *-commutativeN/A

                \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
            4. Applied rewrites83.2%

              \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
            5. Step-by-step derivation
              1. lift-*.f64N/A

                \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
              2. *-commutativeN/A

                \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
              3. lift-/.f64N/A

                \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
              4. clear-numN/A

                \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
              5. un-div-invN/A

                \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
              6. lower-/.f64N/A

                \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
              7. lift-hypot.f64N/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
              8. +-commutativeN/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
              9. lower-hypot.f64N/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
              10. div-invN/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
              11. lower-*.f64N/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
              12. metadata-eval83.2

                \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
            6. Applied rewrites83.2%

              \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
            7. Taylor expanded in B around inf

              \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C}{B} - \left(1 + \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
            8. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \frac{\tan^{-1} \left(\frac{C}{B} - \color{blue}{\left(\frac{A}{B} + 1\right)}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              2. associate--r+N/A

                \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\left(\frac{C}{B} - \frac{A}{B}\right) - 1\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              3. div-subN/A

                \[\leadsto \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              4. lower--.f64N/A

                \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} - 1\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              5. lower-/.f64N/A

                \[\leadsto \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              6. lower--.f6451.3

                \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} - 1\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
            9. Applied rewrites51.3%

              \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} - 1\right)}}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
            10. Taylor expanded in A around inf

              \[\leadsto \frac{\tan^{-1} \left(-1 \cdot \color{blue}{\frac{A}{B}}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
            11. Step-by-step derivation
              1. Applied rewrites41.0%

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

              if 3.9999999999999997e-244 < B

              1. Initial program 55.0%

                \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
              2. Add Preprocessing
              3. Step-by-step derivation
                1. lift-*.f64N/A

                  \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                2. metadata-evalN/A

                  \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                3. lift-/.f64N/A

                  \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                4. times-fracN/A

                  \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
                5. *-commutativeN/A

                  \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
                6. times-fracN/A

                  \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
                7. /-rgt-identityN/A

                  \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                8. lower-*.f64N/A

                  \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                9. lower-/.f6455.0

                  \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
                10. lift-*.f64N/A

                  \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                11. *-commutativeN/A

                  \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
              4. Applied rewrites78.4%

                \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
              5. Step-by-step derivation
                1. lift-*.f64N/A

                  \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
                2. *-commutativeN/A

                  \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
                3. lift-/.f64N/A

                  \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
                4. clear-numN/A

                  \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                5. un-div-invN/A

                  \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                6. lower-/.f64N/A

                  \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                7. lift-hypot.f64N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                8. +-commutativeN/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                9. lower-hypot.f64N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                10. div-invN/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                11. lower-*.f64N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                12. metadata-eval78.4

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
              6. Applied rewrites78.4%

                \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
              7. Taylor expanded in A around 0

                \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              8. Step-by-step derivation
                1. lower--.f64N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                2. unpow2N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                3. unpow2N/A

                  \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                4. lower-hypot.f6465.1

                  \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
              9. Applied rewrites65.1%

                \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
              10. Taylor expanded in C around 0

                \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
              11. Step-by-step derivation
                1. Applied rewrites56.4%

                  \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
              12. Recombined 3 regimes into one program.
              13. Final simplification52.0%

                \[\leadsto \begin{array}{l} \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 4 \cdot 10^{-244}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \end{array} \]
              14. Add Preprocessing

              Alternative 11: 45.3% accurate, 2.5× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 2.8 \cdot 10^{-223}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
              (FPCore (A B C)
               :precision binary64
               (if (<= B -4.3e-147)
                 (* (/ (atan 1.0) (PI)) 180.0)
                 (if (<= B 2.8e-223)
                   (/ (atan (/ (- A) B)) (* 0.005555555555555556 (PI)))
                   (if (<= B 6.5e-43)
                     (* (/ (atan 0.0) (PI)) 180.0)
                     (* (/ (atan -1.0) (PI)) 180.0)))))
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\
              \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\
              
              \mathbf{elif}\;B \leq 2.8 \cdot 10^{-223}:\\
              \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\
              
              \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\
              \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\
              
              \mathbf{else}:\\
              \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 4 regimes
              2. if B < -4.3000000000000001e-147

                1. Initial program 49.8%

                  \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                2. Add Preprocessing
                3. Taylor expanded in B around -inf

                  \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{1}}{\mathsf{PI}\left(\right)} \]
                4. Step-by-step derivation
                  1. Applied rewrites53.1%

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

                  if -4.3000000000000001e-147 < B < 2.80000000000000015e-223

                  1. Initial program 60.2%

                    \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-*.f64N/A

                      \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                    2. metadata-evalN/A

                      \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                    3. lift-/.f64N/A

                      \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                    4. times-fracN/A

                      \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
                    5. *-commutativeN/A

                      \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
                    6. times-fracN/A

                      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
                    7. /-rgt-identityN/A

                      \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                    8. lower-*.f64N/A

                      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                    9. lower-/.f6460.2

                      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
                    10. lift-*.f64N/A

                      \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                    11. *-commutativeN/A

                      \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
                  4. Applied rewrites84.4%

                    \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
                  5. Step-by-step derivation
                    1. lift-*.f64N/A

                      \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
                    2. *-commutativeN/A

                      \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
                    3. lift-/.f64N/A

                      \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
                    4. clear-numN/A

                      \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                    5. un-div-invN/A

                      \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                    6. lower-/.f64N/A

                      \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                    7. lift-hypot.f64N/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                    8. +-commutativeN/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                    9. lower-hypot.f64N/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                    10. div-invN/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                    11. lower-*.f64N/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                    12. metadata-eval84.4

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
                  6. Applied rewrites84.4%

                    \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
                  7. Taylor expanded in B around inf

                    \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C}{B} - \left(1 + \frac{A}{B}\right)\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                  8. Step-by-step derivation
                    1. +-commutativeN/A

                      \[\leadsto \frac{\tan^{-1} \left(\frac{C}{B} - \color{blue}{\left(\frac{A}{B} + 1\right)}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                    2. associate--r+N/A

                      \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\left(\frac{C}{B} - \frac{A}{B}\right) - 1\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                    3. div-subN/A

                      \[\leadsto \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                    4. lower--.f64N/A

                      \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} - 1\right)}}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                    5. lower-/.f64N/A

                      \[\leadsto \frac{\tan^{-1} \left(\color{blue}{\frac{C - A}{B}} - 1\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                    6. lower--.f6454.6

                      \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - A}}{B} - 1\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
                  9. Applied rewrites54.6%

                    \[\leadsto \frac{\tan^{-1} \color{blue}{\left(\frac{C - A}{B} - 1\right)}}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
                  10. Taylor expanded in A around inf

                    \[\leadsto \frac{\tan^{-1} \left(-1 \cdot \color{blue}{\frac{A}{B}}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                  11. Step-by-step derivation
                    1. Applied rewrites43.4%

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

                    if 2.80000000000000015e-223 < B < 6.50000000000000001e-43

                    1. Initial program 46.7%

                      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                    2. Add Preprocessing
                    3. Taylor expanded in C around inf

                      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(-1 \cdot \frac{A + -1 \cdot A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
                    4. Step-by-step derivation
                      1. distribute-rgt1-inN/A

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot A}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                      2. metadata-evalN/A

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0} \cdot A}{B}\right)}{\mathsf{PI}\left(\right)} \]
                      3. mul0-lftN/A

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                      4. div0N/A

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \color{blue}{0}\right)}{\mathsf{PI}\left(\right)} \]
                      5. metadata-eval39.2

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{0}}{\mathsf{PI}\left(\right)} \]
                    5. Applied rewrites39.2%

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

                    if 6.50000000000000001e-43 < B

                    1. Initial program 56.7%

                      \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                    2. Add Preprocessing
                    3. Taylor expanded in B around inf

                      \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                    4. Step-by-step derivation
                      1. Applied rewrites58.3%

                        \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                    5. Recombined 4 regimes into one program.
                    6. Final simplification50.3%

                      \[\leadsto \begin{array}{l} \mathbf{if}\;B \leq -4.3 \cdot 10^{-147}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 2.8 \cdot 10^{-223}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-A}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
                    7. Add Preprocessing

                    Alternative 12: 53.8% accurate, 2.6× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;C \leq 1.7 \cdot 10^{-68}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-0.5}{C} \cdot B\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
                    (FPCore (A B C)
                     :precision binary64
                     (if (<= C 1.7e-68)
                       (/ (atan (/ (- C B) B)) (* 0.005555555555555556 (PI)))
                       (* (/ (atan (* (/ -0.5 C) B)) (PI)) 180.0)))
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;C \leq 1.7 \cdot 10^{-68}:\\
                    \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;\frac{\tan^{-1} \left(\frac{-0.5}{C} \cdot B\right)}{\mathsf{PI}\left(\right)} \cdot 180\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if C < 1.70000000000000009e-68

                      1. Initial program 65.6%

                        \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                      2. Add Preprocessing
                      3. Step-by-step derivation
                        1. lift-*.f64N/A

                          \[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                        2. metadata-evalN/A

                          \[\leadsto \color{blue}{\frac{180}{1}} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                        3. lift-/.f64N/A

                          \[\leadsto \frac{180}{1} \cdot \color{blue}{\frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)}} \]
                        4. times-fracN/A

                          \[\leadsto \color{blue}{\frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1 \cdot \mathsf{PI}\left(\right)}} \]
                        5. *-commutativeN/A

                          \[\leadsto \frac{180 \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot 1}} \]
                        6. times-fracN/A

                          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{1}} \]
                        7. /-rgt-identityN/A

                          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \color{blue}{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                        8. lower-*.f64N/A

                          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                        9. lower-/.f6465.6

                          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \cdot \tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right) \]
                        10. lift-*.f64N/A

                          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)} \]
                        11. *-commutativeN/A

                          \[\leadsto \frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \color{blue}{\left(\left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right) \cdot \frac{1}{B}\right)} \]
                      4. Applied rewrites86.9%

                        \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
                      5. Step-by-step derivation
                        1. lift-*.f64N/A

                          \[\leadsto \color{blue}{\frac{180}{\mathsf{PI}\left(\right)} \cdot \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)} \]
                        2. *-commutativeN/A

                          \[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \frac{180}{\mathsf{PI}\left(\right)}} \]
                        3. lift-/.f64N/A

                          \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{180}{\mathsf{PI}\left(\right)}} \]
                        4. clear-numN/A

                          \[\leadsto \tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right) \cdot \color{blue}{\frac{1}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                        5. un-div-invN/A

                          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                        6. lower-/.f64N/A

                          \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(A - C, B\right)}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}}} \]
                        7. lift-hypot.f64N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\sqrt{\left(A - C\right) \cdot \left(A - C\right) + B \cdot B}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                        8. +-commutativeN/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \sqrt{\color{blue}{B \cdot B + \left(A - C\right) \cdot \left(A - C\right)}}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                        9. lower-hypot.f64N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \color{blue}{\mathsf{hypot}\left(B, A - C\right)}}{B}\right)}{\frac{\mathsf{PI}\left(\right)}{180}} \]
                        10. div-invN/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                        11. lower-*.f64N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\color{blue}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}}} \]
                        12. metadata-eval86.9

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot \color{blue}{0.005555555555555556}} \]
                      6. Applied rewrites86.9%

                        \[\leadsto \color{blue}{\frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556}} \]
                      7. Taylor expanded in A around 0

                        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                      8. Step-by-step derivation
                        1. lower--.f64N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \sqrt{{B}^{2} + {C}^{2}}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                        2. unpow2N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{\color{blue}{B \cdot B} + {C}^{2}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                        3. unpow2N/A

                          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \sqrt{B \cdot B + \color{blue}{C \cdot C}}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                        4. lower-hypot.f6472.7

                          \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{\mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
                      9. Applied rewrites72.7%

                        \[\leadsto \frac{\tan^{-1} \left(\frac{\color{blue}{C - \mathsf{hypot}\left(B, C\right)}}{B}\right)}{\mathsf{PI}\left(\right) \cdot 0.005555555555555556} \]
                      10. Taylor expanded in C around 0

                        \[\leadsto \frac{\tan^{-1} \left(\frac{C - \color{blue}{B}}{B}\right)}{\mathsf{PI}\left(\right) \cdot \frac{1}{180}} \]
                      11. Step-by-step derivation
                        1. Applied rewrites51.4%

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

                        if 1.70000000000000009e-68 < C

                        1. Initial program 29.8%

                          \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                        2. Add Preprocessing
                        3. Taylor expanded in C around inf

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

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\frac{-1}{2} \cdot \frac{B}{C} + -1 \cdot \frac{A + -1 \cdot A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
                          2. *-commutativeN/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\color{blue}{\frac{B}{C} \cdot \frac{-1}{2}} + -1 \cdot \frac{A + -1 \cdot A}{B}\right)}{\mathsf{PI}\left(\right)} \]
                          3. distribute-rgt1-inN/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{B}{C} \cdot \frac{-1}{2} + -1 \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot A}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                          4. metadata-evalN/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{B}{C} \cdot \frac{-1}{2} + -1 \cdot \frac{\color{blue}{0} \cdot A}{B}\right)}{\mathsf{PI}\left(\right)} \]
                          5. mul0-lftN/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{B}{C} \cdot \frac{-1}{2} + -1 \cdot \frac{\color{blue}{0}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                          6. div0N/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{B}{C} \cdot \frac{-1}{2} + -1 \cdot \color{blue}{0}\right)}{\mathsf{PI}\left(\right)} \]
                          7. metadata-evalN/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\frac{B}{C} \cdot \frac{-1}{2} + \color{blue}{0}\right)}{\mathsf{PI}\left(\right)} \]
                          8. lower-fma.f64N/A

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\mathsf{fma}\left(\frac{B}{C}, \frac{-1}{2}, 0\right)\right)}}{\mathsf{PI}\left(\right)} \]
                          9. lower-/.f6459.6

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(\mathsf{fma}\left(\color{blue}{\frac{B}{C}}, -0.5, 0\right)\right)}{\mathsf{PI}\left(\right)} \]
                        5. Applied rewrites59.6%

                          \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(\mathsf{fma}\left(\frac{B}{C}, -0.5, 0\right)\right)}}{\mathsf{PI}\left(\right)} \]
                        6. Step-by-step derivation
                          1. Applied rewrites59.5%

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \left(B \cdot \color{blue}{\frac{-0.5}{C}}\right)}{\mathsf{PI}\left(\right)} \]
                        7. Recombined 2 regimes into one program.
                        8. Final simplification54.1%

                          \[\leadsto \begin{array}{l} \mathbf{if}\;C \leq 1.7 \cdot 10^{-68}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{C - B}{B}\right)}{0.005555555555555556 \cdot \mathsf{PI}\left(\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} \left(\frac{-0.5}{C} \cdot B\right)}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
                        9. Add Preprocessing

                        Alternative 13: 45.1% accurate, 2.8× speedup?

                        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;B \leq -3.2 \cdot 10^{-112}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
                        (FPCore (A B C)
                         :precision binary64
                         (if (<= B -3.2e-112)
                           (* (/ (atan 1.0) (PI)) 180.0)
                           (if (<= B 6.5e-43)
                             (* (/ (atan 0.0) (PI)) 180.0)
                             (* (/ (atan -1.0) (PI)) 180.0))))
                        \begin{array}{l}
                        
                        \\
                        \begin{array}{l}
                        \mathbf{if}\;B \leq -3.2 \cdot 10^{-112}:\\
                        \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\
                        
                        \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\
                        \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\
                        
                        \mathbf{else}:\\
                        \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\
                        
                        
                        \end{array}
                        \end{array}
                        
                        Derivation
                        1. Split input into 3 regimes
                        2. if B < -3.19999999999999993e-112

                          1. Initial program 51.5%

                            \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                          2. Add Preprocessing
                          3. Taylor expanded in B around -inf

                            \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{1}}{\mathsf{PI}\left(\right)} \]
                          4. Step-by-step derivation
                            1. Applied rewrites56.2%

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

                            if -3.19999999999999993e-112 < B < 6.50000000000000001e-43

                            1. Initial program 53.4%

                              \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                            2. Add Preprocessing
                            3. Taylor expanded in C around inf

                              \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(-1 \cdot \frac{A + -1 \cdot A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
                            4. Step-by-step derivation
                              1. distribute-rgt1-inN/A

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot A}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                              2. metadata-evalN/A

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0} \cdot A}{B}\right)}{\mathsf{PI}\left(\right)} \]
                              3. mul0-lftN/A

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                              4. div0N/A

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \color{blue}{0}\right)}{\mathsf{PI}\left(\right)} \]
                              5. metadata-eval34.0

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{0}}{\mathsf{PI}\left(\right)} \]
                            5. Applied rewrites34.0%

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

                            if 6.50000000000000001e-43 < B

                            1. Initial program 56.7%

                              \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                            2. Add Preprocessing
                            3. Taylor expanded in B around inf

                              \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                            4. Step-by-step derivation
                              1. Applied rewrites58.3%

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                            5. Recombined 3 regimes into one program.
                            6. Final simplification47.7%

                              \[\leadsto \begin{array}{l} \mathbf{if}\;B \leq -3.2 \cdot 10^{-112}:\\ \;\;\;\;\frac{\tan^{-1} 1}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{elif}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
                            7. Add Preprocessing

                            Alternative 14: 29.0% accurate, 2.9× speedup?

                            \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \end{array} \]
                            (FPCore (A B C)
                             :precision binary64
                             (if (<= B 6.5e-43)
                               (* (/ (atan 0.0) (PI)) 180.0)
                               (* (/ (atan -1.0) (PI)) 180.0)))
                            \begin{array}{l}
                            
                            \\
                            \begin{array}{l}
                            \mathbf{if}\;B \leq 6.5 \cdot 10^{-43}:\\
                            \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\
                            
                            \mathbf{else}:\\
                            \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\
                            
                            
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Split input into 2 regimes
                            2. if B < 6.50000000000000001e-43

                              1. Initial program 52.6%

                                \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                              2. Add Preprocessing
                              3. Taylor expanded in C around inf

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{\left(-1 \cdot \frac{A + -1 \cdot A}{B}\right)}}{\mathsf{PI}\left(\right)} \]
                              4. Step-by-step derivation
                                1. distribute-rgt1-inN/A

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{\left(-1 + 1\right) \cdot A}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                                2. metadata-evalN/A

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0} \cdot A}{B}\right)}{\mathsf{PI}\left(\right)} \]
                                3. mul0-lftN/A

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \frac{\color{blue}{0}}{B}\right)}{\mathsf{PI}\left(\right)} \]
                                4. div0N/A

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \left(-1 \cdot \color{blue}{0}\right)}{\mathsf{PI}\left(\right)} \]
                                5. metadata-eval21.5

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{0}}{\mathsf{PI}\left(\right)} \]
                              5. Applied rewrites21.5%

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

                              if 6.50000000000000001e-43 < B

                              1. Initial program 56.7%

                                \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                              2. Add Preprocessing
                              3. Taylor expanded in B around inf

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                              4. Step-by-step derivation
                                1. Applied rewrites58.3%

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                              5. Recombined 2 regimes into one program.
                              6. Final simplification32.4%

                                \[\leadsto \begin{array}{l} \mathbf{if}\;B \leq 6.5 \cdot 10^{-43}:\\ \;\;\;\;\frac{\tan^{-1} 0}{\mathsf{PI}\left(\right)} \cdot 180\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180\\ \end{array} \]
                              7. Add Preprocessing

                              Alternative 15: 20.8% accurate, 3.1× speedup?

                              \[\begin{array}{l} \\ \frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180 \end{array} \]
                              (FPCore (A B C) :precision binary64 (* (/ (atan -1.0) (PI)) 180.0))
                              \begin{array}{l}
                              
                              \\
                              \frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180
                              \end{array}
                              
                              Derivation
                              1. Initial program 53.8%

                                \[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\mathsf{PI}\left(\right)} \]
                              2. Add Preprocessing
                              3. Taylor expanded in B around inf

                                \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                              4. Step-by-step derivation
                                1. Applied rewrites21.3%

                                  \[\leadsto 180 \cdot \frac{\tan^{-1} \color{blue}{-1}}{\mathsf{PI}\left(\right)} \]
                                2. Final simplification21.3%

                                  \[\leadsto \frac{\tan^{-1} -1}{\mathsf{PI}\left(\right)} \cdot 180 \]
                                3. Add Preprocessing

                                Reproduce

                                ?
                                herbie shell --seed 2024332 
                                (FPCore (A B C)
                                  :name "ABCF->ab-angle angle"
                                  :precision binary64
                                  (* 180.0 (/ (atan (* (/ 1.0 B) (- (- C A) (sqrt (+ (pow (- A C) 2.0) (pow B 2.0)))))) (PI))))