tan-example (used to crash)

1. Initial program 78.3%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
2. Step-by-step derivation

   1. tan-sum99.7%

      \[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} - \tan a\right) \]

   2. div-inv99.7%

      \[\leadsto x + \left(\color{blue}{\left(\tan y + \tan z\right) \cdot \frac{1}{1 - \tan y \cdot \tan z}} - \tan a\right) \]

3. Applied egg-rr99.7%

   \[\leadsto x + \left(\color{blue}{\left(\tan y + \tan z\right) \cdot \frac{1}{1 - \tan y \cdot \tan z}} - \tan a\right) \]
4. Step-by-step derivation

   1. associate-*r/99.7%

      \[\leadsto x + \left(\color{blue}{\frac{\left(\tan y + \tan z\right) \cdot 1}{1 - \tan y \cdot \tan z}} - \tan a\right) \]

   2. *-rgt-identity99.7%

      \[\leadsto x + \left(\frac{\color{blue}{\tan y + \tan z}}{1 - \tan y \cdot \tan z} - \tan a\right) \]

5. Simplified99.7%

   \[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} - \tan a\right) \]

6. Final simplification99.7%

   \[\leadsto x + \left(\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} - \tan a\right) \]

1. Split input into 3 regimes

2. if a < -3.5e-12

   1. Initial program 80.3%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. +-commutative80.3%

         \[\leadsto \color{blue}{\left(\tan \left(y + z\right) - \tan a\right) + x} \]

      2. associate-+l-80.5%

         \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]

   3. Applied egg-rr80.5%

      \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]
   4. Step-by-step derivation

      1. add-log-exp80.5%

         \[\leadsto \tan \left(y + z\right) - \color{blue}{\log \left(e^{\tan a - x}\right)} \]

   5. Applied egg-rr80.5%

      \[\leadsto \tan \left(y + z\right) - \color{blue}{\log \left(e^{\tan a - x}\right)} \]

   if -3.5e-12 < a < 4.8000000000000002e-26

   1. Initial program 76.2%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. +-commutative76.2%

         \[\leadsto \color{blue}{\left(\tan \left(y + z\right) - \tan a\right) + x} \]

      2. associate-+l-76.2%

         \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]

   3. Applied egg-rr76.2%

      \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]

   4. Taylor expanded in a around 0 76.2%

      \[\leadsto \tan \left(y + z\right) - \color{blue}{-1 \cdot x} \]
   5. Step-by-step derivation

      1. neg-mul-176.2%

         \[\leadsto \tan \left(y + z\right) - \color{blue}{\left(-x\right)} \]

   6. Simplified76.2%

      \[\leadsto \tan \left(y + z\right) - \color{blue}{\left(-x\right)} \]
   7. Step-by-step derivation

      1. sub-neg76.2%

         \[\leadsto \color{blue}{\tan \left(y + z\right) + \left(-\left(-x\right)\right)} \]

      2. add-sqr-sqrt0.0%

         \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{-x} \cdot \sqrt{-x}}\right) \]

      3. sqrt-unprod3.1%

         \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{\left(-x\right) \cdot \left(-x\right)}}\right) \]

      4. sqr-neg3.1%

         \[\leadsto \tan \left(y + z\right) + \left(-\sqrt{\color{blue}{x \cdot x}}\right) \]

      5. sqrt-unprod3.1%

         \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right) \]

      6. add-sqr-sqrt3.1%

         \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{x}\right) \]

      7. add-sqr-sqrt0.0%

         \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{-x} \cdot \sqrt{-x}} \]

      8. sqrt-unprod76.2%

         \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{\left(-x\right) \cdot \left(-x\right)}} \]

      9. sqr-neg76.2%

         \[\leadsto \tan \left(y + z\right) + \sqrt{\color{blue}{x \cdot x}} \]

      10. sqrt-unprod75.7%

          \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{x} \cdot \sqrt{x}} \]

      11. add-sqr-sqrt76.2%

          \[\leadsto \tan \left(y + z\right) + \color{blue}{x} \]

      12. +-commutative76.2%

          \[\leadsto \tan \color{blue}{\left(z + y\right)} + x \]

   8. Applied egg-rr76.2%

      \[\leadsto \color{blue}{\tan \left(z + y\right) + x} \]
   9. Step-by-step derivation

      1. tan-sum99.9%

         \[\leadsto \color{blue}{\frac{\tan z + \tan y}{1 - \tan z \cdot \tan y}} + x \]

      2. tan-quot99.8%

         \[\leadsto \frac{\color{blue}{\frac{\sin z}{\cos z}} + \tan y}{1 - \tan z \cdot \tan y} + x \]

      3. *-commutative99.8%

         \[\leadsto \frac{\frac{\sin z}{\cos z} + \tan y}{1 - \color{blue}{\tan y \cdot \tan z}} + x \]

      4. div-inv99.8%

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

      5. tan-quot99.8%

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

      6. +-commutative99.8%

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

   10. Applied egg-rr99.8%

       \[\leadsto \color{blue}{\left(\tan y + \tan z\right) \cdot \frac{1}{1 - \tan y \cdot \tan z}} + x \]
   11. Step-by-step derivation

       1. associate-*r/99.9%

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

       2. *-rgt-identity99.9%

          \[\leadsto \frac{\color{blue}{\tan y + \tan z}}{1 - \tan y \cdot \tan z} + x \]

   12. Simplified99.9%

       \[\leadsto \color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} + x \]

   if 4.8000000000000002e-26 < a

   1. Initial program 79.9%

      \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
   2. Step-by-step derivation

      1. add-cbrt-cube79.9%

         \[\leadsto x + \left(\color{blue}{\sqrt[3]{\left(\tan \left(y + z\right) \cdot \tan \left(y + z\right)\right) \cdot \tan \left(y + z\right)}} - \tan a\right) \]

      2. pow379.9%

         \[\leadsto x + \left(\sqrt[3]{\color{blue}{{\tan \left(y + z\right)}^{3}}} - \tan a\right) \]

   3. Applied egg-rr79.9%

      \[\leadsto x + \left(\color{blue}{\sqrt[3]{{\tan \left(y + z\right)}^{3}}} - \tan a\right) \]
3. Recombined 3 regimes into one program.

4. Final simplification89.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -3.5 \cdot 10^{-12}:\\ \;\;\;\;\tan \left(y + z\right) - \log \left(e^{\tan a - x}\right)\\ \mathbf{elif}\;a \leq 4.8 \cdot 10^{-26}:\\ \;\;\;\;x + \frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}\\ \mathbf{else}:\\ \;\;\;\;x + \left(\sqrt[3]{{\tan \left(y + z\right)}^{3}} - \tan a\right)\\ \end{array} \]

1. Initial program 78.3%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

2. Final simplification78.3%

   \[\leadsto x + \left(\tan \left(y + z\right) - \tan a\right) \]

1. Initial program 78.3%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]
2. Step-by-step derivation

   1. +-commutative78.3%

      \[\leadsto \color{blue}{\left(\tan \left(y + z\right) - \tan a\right) + x} \]

   2. associate-+l-78.3%

      \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]

3. Applied egg-rr78.3%

   \[\leadsto \color{blue}{\tan \left(y + z\right) - \left(\tan a - x\right)} \]

4. Taylor expanded in a around 0 48.6%

   \[\leadsto \tan \left(y + z\right) - \color{blue}{-1 \cdot x} \]
5. Step-by-step derivation

   1. neg-mul-148.6%

      \[\leadsto \tan \left(y + z\right) - \color{blue}{\left(-x\right)} \]

6. Simplified48.6%

   \[\leadsto \tan \left(y + z\right) - \color{blue}{\left(-x\right)} \]
7. Step-by-step derivation

   1. sub-neg48.6%

      \[\leadsto \color{blue}{\tan \left(y + z\right) + \left(-\left(-x\right)\right)} \]

   2. add-sqr-sqrt0.0%

      \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{-x} \cdot \sqrt{-x}}\right) \]

   3. sqrt-unprod3.4%

      \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{\left(-x\right) \cdot \left(-x\right)}}\right) \]

   4. sqr-neg3.4%

      \[\leadsto \tan \left(y + z\right) + \left(-\sqrt{\color{blue}{x \cdot x}}\right) \]

   5. sqrt-unprod3.4%

      \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right) \]

   6. add-sqr-sqrt3.4%

      \[\leadsto \tan \left(y + z\right) + \left(-\color{blue}{x}\right) \]

   7. add-sqr-sqrt0.0%

      \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{-x} \cdot \sqrt{-x}} \]

   8. sqrt-unprod48.6%

      \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{\left(-x\right) \cdot \left(-x\right)}} \]

   9. sqr-neg48.6%

      \[\leadsto \tan \left(y + z\right) + \sqrt{\color{blue}{x \cdot x}} \]

   10. sqrt-unprod48.3%

       \[\leadsto \tan \left(y + z\right) + \color{blue}{\sqrt{x} \cdot \sqrt{x}} \]

   11. add-sqr-sqrt48.6%

       \[\leadsto \tan \left(y + z\right) + \color{blue}{x} \]

   12. +-commutative48.6%

       \[\leadsto \tan \color{blue}{\left(z + y\right)} + x \]

8. Applied egg-rr48.6%

   \[\leadsto \color{blue}{\tan \left(z + y\right) + x} \]

9. Final simplification48.6%

   \[\leadsto x + \tan \left(y + z\right) \]

1. Initial program 78.3%

   \[x + \left(\tan \left(y + z\right) - \tan a\right) \]

2. Taylor expanded in x around inf 30.9%

   \[\leadsto \color{blue}{x} \]

3. Final simplification30.9%

   \[\leadsto x \]

herbie shell --seed 2023166 
(FPCore (x y z a)
  :name "tan-example (used to crash)"
  :precision binary64
  :pre (and (and (and (or (== x 0.0) (and (<= 0.5884142 x) (<= x 505.5909))) (or (and (<= -1.796658e+308 y) (<= y -9.425585e-310)) (and (<= 1.284938e-309 y) (<= y 1.751224e+308)))) (or (and (<= -1.776707e+308 z) (<= z -8.599796e-310)) (and (<= 3.293145e-311 z) (<= z 1.725154e+308)))) (or (and (<= -1.796658e+308 a) (<= a -9.425585e-310)) (and (<= 1.284938e-309 a) (<= a 1.751224e+308))))
  (+ x (- (tan (+ y z)) (tan a))))