VandenBroeck and Keller, Equation (24)

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. +-commutative99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

   2. unsub-neg99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

   3. associate-*r/99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

   4. *-rgt-identity99.8%

      \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

3. Simplified99.8%

   \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]

4. Final simplification99.8%

   \[\leadsto \frac{1}{\sin B} - \frac{x}{\tan B} \]

1. Split input into 2 regimes

2. if x < -3.2e8 or 9.5e9 < x

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.9%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.9%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.6%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.8%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in x around inf 99.7%

      \[\leadsto \color{blue}{-1 \cdot \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. mul-1-neg99.7%

         \[\leadsto \color{blue}{-\frac{\cos B \cdot x}{\sin B}} \]

      2. *-commutative99.7%

         \[\leadsto -\frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      3. associate-*r/99.6%

         \[\leadsto -\color{blue}{x \cdot \frac{\cos B}{\sin B}} \]

      4. distribute-lft-neg-in99.6%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]

   8. Simplified99.6%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]

   if -3.2e8 < x < 9.5e9

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.7%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.7%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in B around 0 98.6%

      \[\leadsto \frac{1 - \color{blue}{x}}{\sin B} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -320000000 \lor \neg \left(x \leq 9500000000\right):\\ \;\;\;\;\left(-x\right) \cdot \frac{\cos B}{\sin B}\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - x}{\sin B}\\ \end{array} \]

1. Split input into 3 regimes

2. if x < -2.4e7

   1. Initial program 99.6%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.6%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.6%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.8%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.8%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.6%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.8%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.8%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.8%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.8%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.8%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.8%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in x around inf 99.8%

      \[\leadsto \color{blue}{-1 \cdot \frac{\cos B \cdot x}{\sin B}} \]
   10. Step-by-step derivation

       1. mul-1-neg99.8%

          \[\leadsto \color{blue}{-\frac{\cos B \cdot x}{\sin B}} \]

       2. associate-/l*99.7%

          \[\leadsto -\color{blue}{\frac{\cos B}{\frac{\sin B}{x}}} \]

       3. *-lft-identity99.7%

          \[\leadsto -\frac{\cos B}{\frac{\color{blue}{1 \cdot \sin B}}{x}} \]

       4. associate-*l/99.6%

          \[\leadsto -\frac{\cos B}{\color{blue}{\frac{1}{x} \cdot \sin B}} \]

       5. *-commutative99.6%

          \[\leadsto -\frac{\cos B}{\color{blue}{\sin B \cdot \frac{1}{x}}} \]

       6. distribute-neg-frac99.6%

          \[\leadsto \color{blue}{\frac{-\cos B}{\sin B \cdot \frac{1}{x}}} \]

       7. *-commutative99.6%

          \[\leadsto \frac{-\cos B}{\color{blue}{\frac{1}{x} \cdot \sin B}} \]

       8. associate-*l/99.7%

          \[\leadsto \frac{-\cos B}{\color{blue}{\frac{1 \cdot \sin B}{x}}} \]

       9. *-lft-identity99.7%

          \[\leadsto \frac{-\cos B}{\frac{\color{blue}{\sin B}}{x}} \]

   11. Simplified99.7%

       \[\leadsto \color{blue}{\frac{-\cos B}{\frac{\sin B}{x}}} \]

   if -2.4e7 < x < 7.3e9

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.7%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.7%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in B around 0 98.6%

      \[\leadsto \frac{1 - \color{blue}{x}}{\sin B} \]

   if 7.3e9 < x

   1. Initial program 99.8%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.8%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.8%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.9%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.9%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in x around inf 99.7%

      \[\leadsto \color{blue}{-1 \cdot \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. mul-1-neg99.7%

         \[\leadsto \color{blue}{-\frac{\cos B \cdot x}{\sin B}} \]

      2. *-commutative99.7%

         \[\leadsto -\frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      3. associate-*r/99.7%

         \[\leadsto -\color{blue}{x \cdot \frac{\cos B}{\sin B}} \]

      4. distribute-lft-neg-in99.7%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]
3. Recombined 3 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -24000000:\\ \;\;\;\;\frac{-\cos B}{\frac{\sin B}{x}}\\ \mathbf{elif}\;x \leq 7300000000:\\ \;\;\;\;\frac{1 - x}{\sin B}\\ \mathbf{else}:\\ \;\;\;\;\left(-x\right) \cdot \frac{\cos B}{\sin B}\\ \end{array} \]

1. Split input into 3 regimes

2. if x < -1.35e9

   1. Initial program 99.6%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.6%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.6%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.8%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.8%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.6%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.8%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.8%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.8%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.8%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.8%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.8%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in x around inf 99.8%

      \[\leadsto \frac{\color{blue}{-1 \cdot \left(\cos B \cdot x\right)}}{\sin B} \]
   10. Step-by-step derivation

       1. mul-1-neg99.8%

          \[\leadsto \frac{\color{blue}{-\cos B \cdot x}}{\sin B} \]

       2. distribute-rgt-neg-out99.8%

          \[\leadsto \frac{\color{blue}{\cos B \cdot \left(-x\right)}}{\sin B} \]

   11. Simplified99.8%

       \[\leadsto \frac{\color{blue}{\cos B \cdot \left(-x\right)}}{\sin B} \]

   if -1.35e9 < x < 4e10

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.7%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.7%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in B around 0 98.6%

      \[\leadsto \frac{1 - \color{blue}{x}}{\sin B} \]

   if 4e10 < x

   1. Initial program 99.8%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.8%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.8%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.9%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.9%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in x around inf 99.7%

      \[\leadsto \color{blue}{-1 \cdot \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. mul-1-neg99.7%

         \[\leadsto \color{blue}{-\frac{\cos B \cdot x}{\sin B}} \]

      2. *-commutative99.7%

         \[\leadsto -\frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      3. associate-*r/99.7%

         \[\leadsto -\color{blue}{x \cdot \frac{\cos B}{\sin B}} \]

      4. distribute-lft-neg-in99.7%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{\cos B}{\sin B}} \]
3. Recombined 3 regimes into one program.

4. Final simplification99.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1350000000:\\ \;\;\;\;\frac{x \cdot \left(-\cos B\right)}{\sin B}\\ \mathbf{elif}\;x \leq 40000000000:\\ \;\;\;\;\frac{1 - x}{\sin B}\\ \mathbf{else}:\\ \;\;\;\;\left(-x\right) \cdot \frac{\cos B}{\sin B}\\ \end{array} \]

1. Split input into 2 regimes

2. if x < -8e80 or 3.00000000000000015e109 < x

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.9%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.9%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]

   4. Taylor expanded in B around 0 89.4%

      \[\leadsto \color{blue}{\left(0.16666666666666666 \cdot B + \frac{1}{B}\right)} - \frac{x}{\tan B} \]

   5. Taylor expanded in B around inf 89.4%

      \[\leadsto \color{blue}{0.16666666666666666 \cdot B} - \frac{x}{\tan B} \]
   6. Step-by-step derivation

      1. *-commutative89.4%

         \[\leadsto \color{blue}{B \cdot 0.16666666666666666} - \frac{x}{\tan B} \]

   7. Simplified89.4%

      \[\leadsto \color{blue}{B \cdot 0.16666666666666666} - \frac{x}{\tan B} \]

   if -8e80 < x < 3.00000000000000015e109

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. +-commutative99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

      2. unsub-neg99.7%

         \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

      3. associate-*r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

      4. *-rgt-identity99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
   4. Step-by-step derivation

      1. tan-quot99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

      2. associate-/r/99.7%

         \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   5. Applied egg-rr99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

   6. Taylor expanded in B around inf 99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
   7. Step-by-step derivation

      1. *-commutative99.7%

         \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

      2. div-sub99.7%

         \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

      3. *-commutative99.7%

         \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

   8. Simplified99.7%

      \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

   9. Taylor expanded in B around 0 88.7%

      \[\leadsto \frac{1 - \color{blue}{x}}{\sin B} \]
3. Recombined 2 regimes into one program.

4. Final simplification89.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -8 \cdot 10^{+80} \lor \neg \left(x \leq 3 \cdot 10^{+109}\right):\\ \;\;\;\;B \cdot 0.16666666666666666 - \frac{x}{\tan B}\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - x}{\sin B}\\ \end{array} \]

1. Split input into 2 regimes

2. if x < -1.79999999999999992e-11 or 1.15e-6 < x

   1. Initial program 99.6%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. distribute-lft-neg-in99.6%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

   3. Simplified99.6%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

   4. Taylor expanded in B around 0 55.9%

      \[\leadsto \color{blue}{-1 \cdot \frac{x}{B} + \left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right)} \]
   5. Step-by-step derivation

      1. +-commutative55.9%

         \[\leadsto \color{blue}{\left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) + -1 \cdot \frac{x}{B}} \]

      2. mul-1-neg55.9%

         \[\leadsto \left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) + \color{blue}{\left(-\frac{x}{B}\right)} \]

      3. sub-neg55.9%

         \[\leadsto \color{blue}{\left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) - \frac{x}{B}} \]

      4. associate--l+55.9%

         \[\leadsto \color{blue}{\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \left(\frac{1}{B} - \frac{x}{B}\right)} \]

      5. *-commutative55.9%

         \[\leadsto \color{blue}{B \cdot \left(0.16666666666666666 + 0.3333333333333333 \cdot x\right)} + \left(\frac{1}{B} - \frac{x}{B}\right) \]

      6. *-commutative55.9%

         \[\leadsto B \cdot \left(0.16666666666666666 + \color{blue}{x \cdot 0.3333333333333333}\right) + \left(\frac{1}{B} - \frac{x}{B}\right) \]

      7. div-sub55.9%

         \[\leadsto B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \color{blue}{\frac{1 - x}{B}} \]

   6. Simplified55.9%

      \[\leadsto \color{blue}{B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \frac{1 - x}{B}} \]

   if -1.79999999999999992e-11 < x < 1.15e-6

   1. Initial program 99.8%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. distribute-lft-neg-in99.8%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

   4. Taylor expanded in x around 0 99.2%

      \[\leadsto \color{blue}{\frac{1}{\sin B}} \]
3. Recombined 2 regimes into one program.

4. Final simplification76.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.8 \cdot 10^{-11} \lor \neg \left(x \leq 1.15 \cdot 10^{-6}\right):\\ \;\;\;\;B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \frac{1 - x}{B}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sin B}\\ \end{array} \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. +-commutative99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

   2. unsub-neg99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

   3. associate-*r/99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

   4. *-rgt-identity99.8%

      \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

3. Simplified99.8%

   \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]
4. Step-by-step derivation

   1. tan-quot99.7%

      \[\leadsto \frac{1}{\sin B} - \frac{x}{\color{blue}{\frac{\sin B}{\cos B}}} \]

   2. associate-/r/99.7%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

5. Applied egg-rr99.7%

   \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x}{\sin B} \cdot \cos B} \]

6. Taylor expanded in B around inf 99.7%

   \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{\cos B \cdot x}{\sin B}} \]
7. Step-by-step derivation

   1. *-commutative99.7%

      \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x \cdot \cos B}}{\sin B} \]

   2. div-sub99.7%

      \[\leadsto \color{blue}{\frac{1 - x \cdot \cos B}{\sin B}} \]

   3. *-commutative99.7%

      \[\leadsto \frac{1 - \color{blue}{\cos B \cdot x}}{\sin B} \]

8. Simplified99.7%

   \[\leadsto \color{blue}{\frac{1 - \cos B \cdot x}{\sin B}} \]

9. Taylor expanded in B around 0 77.9%

   \[\leadsto \frac{1 - \color{blue}{x}}{\sin B} \]

10. Final simplification77.9%

    \[\leadsto \frac{1 - x}{\sin B} \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. distribute-lft-neg-in99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

3. Simplified99.7%

   \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

4. Taylor expanded in B around 0 53.8%

   \[\leadsto \color{blue}{-1 \cdot \frac{x}{B} + \left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right)} \]
5. Step-by-step derivation

   1. +-commutative53.8%

      \[\leadsto \color{blue}{\left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) + -1 \cdot \frac{x}{B}} \]

   2. mul-1-neg53.8%

      \[\leadsto \left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) + \color{blue}{\left(-\frac{x}{B}\right)} \]

   3. sub-neg53.8%

      \[\leadsto \color{blue}{\left(\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \frac{1}{B}\right) - \frac{x}{B}} \]

   4. associate--l+53.8%

      \[\leadsto \color{blue}{\left(0.16666666666666666 + 0.3333333333333333 \cdot x\right) \cdot B + \left(\frac{1}{B} - \frac{x}{B}\right)} \]

   5. *-commutative53.8%

      \[\leadsto \color{blue}{B \cdot \left(0.16666666666666666 + 0.3333333333333333 \cdot x\right)} + \left(\frac{1}{B} - \frac{x}{B}\right) \]

   6. *-commutative53.8%

      \[\leadsto B \cdot \left(0.16666666666666666 + \color{blue}{x \cdot 0.3333333333333333}\right) + \left(\frac{1}{B} - \frac{x}{B}\right) \]

   7. div-sub53.8%

      \[\leadsto B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \color{blue}{\frac{1 - x}{B}} \]

6. Simplified53.8%

   \[\leadsto \color{blue}{B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \frac{1 - x}{B}} \]

7. Final simplification53.8%

   \[\leadsto B \cdot \left(0.16666666666666666 + x \cdot 0.3333333333333333\right) + \frac{1 - x}{B} \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. +-commutative99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

   2. unsub-neg99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

   3. associate-*r/99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

   4. *-rgt-identity99.8%

      \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

3. Simplified99.8%

   \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]

4. Taylor expanded in B around 0 66.1%

   \[\leadsto \color{blue}{\left(0.16666666666666666 \cdot B + \frac{1}{B}\right)} - \frac{x}{\tan B} \]

5. Taylor expanded in B around 0 53.7%

   \[\leadsto \left(0.16666666666666666 \cdot B + \frac{1}{B}\right) - \color{blue}{\frac{x}{B}} \]

6. Final simplification53.7%

   \[\leadsto \left(B \cdot 0.16666666666666666 + \frac{1}{B}\right) - \frac{x}{B} \]

1. Split input into 2 regimes

2. if x < -3.4499999999999999e22 or 1 < x

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. distribute-lft-neg-in99.7%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

   4. Taylor expanded in B around 0 54.3%

      \[\leadsto \color{blue}{\frac{1 + -1 \cdot x}{B}} \]
   5. Step-by-step derivation

      1. mul-1-neg54.3%

         \[\leadsto \frac{1 + \color{blue}{\left(-x\right)}}{B} \]

      2. sub-neg54.3%

         \[\leadsto \frac{\color{blue}{1 - x}}{B} \]

   6. Simplified54.3%

      \[\leadsto \color{blue}{\frac{1 - x}{B}} \]

   7. Taylor expanded in x around inf 54.1%

      \[\leadsto \color{blue}{-1 \cdot \frac{x}{B}} \]
   8. Step-by-step derivation

      1. neg-mul-154.1%

         \[\leadsto \color{blue}{-\frac{x}{B}} \]

      2. distribute-neg-frac54.1%

         \[\leadsto \color{blue}{\frac{-x}{B}} \]

   9. Simplified54.1%

      \[\leadsto \color{blue}{\frac{-x}{B}} \]

   if -3.4499999999999999e22 < x < 1

   1. Initial program 99.7%

      \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
   2. Step-by-step derivation

      1. distribute-lft-neg-in99.7%

         \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

   4. Taylor expanded in B around 0 52.5%

      \[\leadsto \color{blue}{\frac{1 + -1 \cdot x}{B}} \]
   5. Step-by-step derivation

      1. mul-1-neg52.5%

         \[\leadsto \frac{1 + \color{blue}{\left(-x\right)}}{B} \]

      2. sub-neg52.5%

         \[\leadsto \frac{\color{blue}{1 - x}}{B} \]

   6. Simplified52.5%

      \[\leadsto \color{blue}{\frac{1 - x}{B}} \]

   7. Taylor expanded in x around 0 50.8%

      \[\leadsto \color{blue}{\frac{1}{B}} \]
3. Recombined 2 regimes into one program.

4. Final simplification52.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -3.45 \cdot 10^{+22} \lor \neg \left(x \leq 1\right):\\ \;\;\;\;\frac{-x}{B}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{B}\\ \end{array} \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. distribute-lft-neg-in99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

3. Simplified99.7%

   \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

4. Taylor expanded in B around 0 53.5%

   \[\leadsto \color{blue}{\frac{1 + -1 \cdot x}{B}} \]
5. Step-by-step derivation

   1. mul-1-neg53.5%

      \[\leadsto \frac{1 + \color{blue}{\left(-x\right)}}{B} \]

   2. sub-neg53.5%

      \[\leadsto \frac{\color{blue}{1 - x}}{B} \]

6. Simplified53.5%

   \[\leadsto \color{blue}{\frac{1 - x}{B}} \]

7. Final simplification53.5%

   \[\leadsto \frac{1 - x}{B} \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. +-commutative99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} + \left(-x \cdot \frac{1}{\tan B}\right)} \]

   2. unsub-neg99.7%

      \[\leadsto \color{blue}{\frac{1}{\sin B} - x \cdot \frac{1}{\tan B}} \]

   3. associate-*r/99.8%

      \[\leadsto \frac{1}{\sin B} - \color{blue}{\frac{x \cdot 1}{\tan B}} \]

   4. *-rgt-identity99.8%

      \[\leadsto \frac{1}{\sin B} - \frac{\color{blue}{x}}{\tan B} \]

3. Simplified99.8%

   \[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}} \]

4. Taylor expanded in B around 0 66.1%

   \[\leadsto \color{blue}{\left(0.16666666666666666 \cdot B + \frac{1}{B}\right)} - \frac{x}{\tan B} \]

5. Taylor expanded in B around 0 53.7%

   \[\leadsto \left(0.16666666666666666 \cdot B + \frac{1}{B}\right) - \color{blue}{\frac{x}{B}} \]

6. Taylor expanded in B around inf 3.0%

   \[\leadsto \color{blue}{0.16666666666666666 \cdot B} \]
7. Step-by-step derivation

   1. *-commutative3.0%

      \[\leadsto \color{blue}{B \cdot 0.16666666666666666} \]

8. Simplified3.0%

   \[\leadsto \color{blue}{B \cdot 0.16666666666666666} \]

9. Final simplification3.0%

   \[\leadsto B \cdot 0.16666666666666666 \]

1. Initial program 99.7%

   \[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B} \]
2. Step-by-step derivation

   1. distribute-lft-neg-in99.7%

      \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B}} + \frac{1}{\sin B} \]

3. Simplified99.7%

   \[\leadsto \color{blue}{\left(-x\right) \cdot \frac{1}{\tan B} + \frac{1}{\sin B}} \]

4. Taylor expanded in B around 0 53.5%

   \[\leadsto \color{blue}{\frac{1 + -1 \cdot x}{B}} \]
5. Step-by-step derivation

   1. mul-1-neg53.5%

      \[\leadsto \frac{1 + \color{blue}{\left(-x\right)}}{B} \]

   2. sub-neg53.5%

      \[\leadsto \frac{\color{blue}{1 - x}}{B} \]

6. Simplified53.5%

   \[\leadsto \color{blue}{\frac{1 - x}{B}} \]

7. Taylor expanded in x around 0 26.3%

   \[\leadsto \color{blue}{\frac{1}{B}} \]

8. Final simplification26.3%

   \[\leadsto \frac{1}{B} \]

herbie shell --seed 2023166 
(FPCore (B x)
  :name "VandenBroeck and Keller, Equation (24)"
  :precision binary64
  (+ (- (* x (/ 1.0 (tan B)))) (/ 1.0 (sin B))))