Maksimov and Kolovsky, Equation (3)

1. Initial program 73.3%

   \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
2. Step-by-step derivation

   1. *-commutative73.3%

      \[\leadsto \left(\color{blue}{\left(J \cdot -2\right)} \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]

   2. associate-*l*73.3%

      \[\leadsto \color{blue}{\left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]

   3. unpow273.3%

      \[\leadsto \left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}} \]

   4. hypot-1-def86.7%

      \[\leadsto \left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)} \]

   5. *-commutative86.7%

      \[\leadsto \left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right) \]

   6. associate-*l*86.7%

      \[\leadsto \left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right) \]

3. Simplified86.7%

   \[\leadsto \color{blue}{\left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)} \]

4. Final simplification86.7%

   \[\leadsto \left(J \cdot \left(-2 \cdot \cos \left(\frac{K}{2}\right)\right)\right) \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right) \]

1. Initial program 73.3%

   \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
2. Step-by-step derivation

   1. *-commutative73.3%

      \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

   2. associate-*l*73.3%

      \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

   3. associate-*r*73.3%

      \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

   4. *-commutative73.3%

      \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

   5. associate-*l*73.2%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

   6. *-commutative73.2%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

   7. unpow273.2%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

   8. hypot-1-def86.6%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

   9. *-commutative86.6%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

   10. associate-*l*86.6%

       \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

3. Simplified86.6%

   \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

4. Final simplification86.6%

   \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right) \]

1. Split input into 2 regimes

2. if K < -8.2000000000000001e43 or 6e-10 < K

   1. Initial program 74.6%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative74.6%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*74.6%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*74.6%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative74.6%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*74.5%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative74.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow274.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def86.7%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative86.7%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*86.7%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified86.7%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in U around 0 58.7%

      \[\leadsto J \cdot \color{blue}{\left(-2 \cdot \cos \left(0.5 \cdot K\right)\right)} \]

   if -8.2000000000000001e43 < K < 6e-10

   1. Initial program 72.2%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative72.2%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*72.2%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*72.2%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative72.2%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*72.2%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative72.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow272.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def86.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative86.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*86.5%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified86.5%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in K around 0 53.1%

      \[\leadsto \color{blue}{-2 \cdot \left(\sqrt{1 + 0.25 \cdot \frac{{U}^{2}}{{J}^{2}}} \cdot J\right)} \]
   5. Step-by-step derivation

      1. associate-*r*53.1%

         \[\leadsto \color{blue}{\left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{{U}^{2}}{{J}^{2}}}\right) \cdot J} \]

      2. unpow253.1%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{\color{blue}{U \cdot U}}{{J}^{2}}}\right) \cdot J \]

      3. unpow253.1%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{U \cdot U}{\color{blue}{J \cdot J}}}\right) \cdot J \]

   6. Simplified53.1%

      \[\leadsto \color{blue}{\left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{U \cdot U}{J \cdot J}}\right) \cdot J} \]
   7. Step-by-step derivation

      1. clear-num53.1%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \color{blue}{\frac{1}{\frac{J \cdot J}{U \cdot U}}}}\right) \cdot J \]

      2. inv-pow53.1%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \color{blue}{{\left(\frac{J \cdot J}{U \cdot U}\right)}^{-1}}}\right) \cdot J \]

   8. Applied egg-rr53.1%

      \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \color{blue}{{\left(\frac{J \cdot J}{U \cdot U}\right)}^{-1}}}\right) \cdot J \]
   9. Step-by-step derivation

      1. unpow-153.1%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \color{blue}{\frac{1}{\frac{J \cdot J}{U \cdot U}}}}\right) \cdot J \]

      2. times-frac67.8%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{1}{\color{blue}{\frac{J}{U} \cdot \frac{J}{U}}}}\right) \cdot J \]

   10. Simplified67.8%

       \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \color{blue}{\frac{1}{\frac{J}{U} \cdot \frac{J}{U}}}}\right) \cdot J \]
   11. Step-by-step derivation

       1. add-sqr-sqrt67.8%

          \[\leadsto \left(-2 \cdot \sqrt{1 + \color{blue}{\sqrt{0.25 \cdot \frac{1}{\frac{J}{U} \cdot \frac{J}{U}}} \cdot \sqrt{0.25 \cdot \frac{1}{\frac{J}{U} \cdot \frac{J}{U}}}}}\right) \cdot J \]

       2. hypot-1-def67.8%

          \[\leadsto \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \sqrt{0.25 \cdot \frac{1}{\frac{J}{U} \cdot \frac{J}{U}}}\right)}\right) \cdot J \]

       3. *-commutative67.8%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \sqrt{\color{blue}{\frac{1}{\frac{J}{U} \cdot \frac{J}{U}} \cdot 0.25}}\right)\right) \cdot J \]

       4. sqrt-prod67.8%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \color{blue}{\sqrt{\frac{1}{\frac{J}{U} \cdot \frac{J}{U}}} \cdot \sqrt{0.25}}\right)\right) \cdot J \]

       5. sqrt-div67.8%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \color{blue}{\frac{\sqrt{1}}{\sqrt{\frac{J}{U} \cdot \frac{J}{U}}}} \cdot \sqrt{0.25}\right)\right) \cdot J \]

       6. metadata-eval67.8%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \frac{\color{blue}{1}}{\sqrt{\frac{J}{U} \cdot \frac{J}{U}}} \cdot \sqrt{0.25}\right)\right) \cdot J \]

       7. sqrt-prod50.7%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \frac{1}{\color{blue}{\sqrt{\frac{J}{U}} \cdot \sqrt{\frac{J}{U}}}} \cdot \sqrt{0.25}\right)\right) \cdot J \]

       8. add-sqr-sqrt80.8%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \frac{1}{\color{blue}{\frac{J}{U}}} \cdot \sqrt{0.25}\right)\right) \cdot J \]

       9. clear-num80.9%

          \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \color{blue}{\frac{U}{J}} \cdot \sqrt{0.25}\right)\right) \cdot J \]

       10. metadata-eval80.9%

           \[\leadsto \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J} \cdot \color{blue}{0.5}\right)\right) \cdot J \]

   12. Applied egg-rr80.9%

       \[\leadsto \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{J} \cdot 0.5\right)}\right) \cdot J \]
3. Recombined 2 regimes into one program.

4. Final simplification70.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;K \leq -8.2 \cdot 10^{+43} \lor \neg \left(K \leq 6 \cdot 10^{-10}\right):\\ \;\;\;\;J \cdot \left(-2 \cdot \cos \left(K \cdot 0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;J \cdot \left(-2 \cdot \mathsf{hypot}\left(1, 0.5 \cdot \frac{U}{J}\right)\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if J < -1.74999999999999993e-81 or 5.19999999999999979e-110 < J

   1. Initial program 91.8%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative91.8%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*91.8%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*91.8%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative91.8%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*91.8%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative91.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow291.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def96.4%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative96.4%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*96.4%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified96.4%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in U around 0 75.7%

      \[\leadsto J \cdot \color{blue}{\left(-2 \cdot \cos \left(0.5 \cdot K\right)\right)} \]

   if -1.74999999999999993e-81 < J < 1.65000000000000013e-244

   1. Initial program 40.2%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative40.2%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*40.2%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*40.2%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative40.2%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*40.1%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative40.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow240.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def69.4%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative69.4%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*69.4%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified69.4%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in J around 0 55.9%

      \[\leadsto \color{blue}{-1 \cdot U} \]
   5. Step-by-step derivation

      1. neg-mul-155.9%

         \[\leadsto \color{blue}{-U} \]

   6. Simplified55.9%

      \[\leadsto \color{blue}{-U} \]

   if 1.65000000000000013e-244 < J < 5.19999999999999979e-110

   1. Initial program 45.1%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative45.1%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*45.1%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*45.1%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative45.1%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*45.1%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative45.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow245.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def71.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative71.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*71.2%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified71.2%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in U around -inf 52.9%

      \[\leadsto \color{blue}{U} \]
3. Recombined 3 regimes into one program.

4. Final simplification67.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;J \leq -1.75 \cdot 10^{-81}:\\ \;\;\;\;J \cdot \left(-2 \cdot \cos \left(K \cdot 0.5\right)\right)\\ \mathbf{elif}\;J \leq 1.65 \cdot 10^{-244}:\\ \;\;\;\;-U\\ \mathbf{elif}\;J \leq 5.2 \cdot 10^{-110}:\\ \;\;\;\;U\\ \mathbf{else}:\\ \;\;\;\;J \cdot \left(-2 \cdot \cos \left(K \cdot 0.5\right)\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if J < -2.7999999999999998e-28 or 1.79999999999999998e49 < J

   1. Initial program 97.5%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative97.5%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*97.5%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*97.5%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative97.5%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*97.5%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative97.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow297.5%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def99.7%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative99.7%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*99.7%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified99.7%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in K around 0 47.9%

      \[\leadsto \color{blue}{-2 \cdot \left(\sqrt{1 + 0.25 \cdot \frac{{U}^{2}}{{J}^{2}}} \cdot J\right)} \]
   5. Step-by-step derivation

      1. associate-*r*47.9%

         \[\leadsto \color{blue}{\left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{{U}^{2}}{{J}^{2}}}\right) \cdot J} \]

      2. unpow247.9%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{\color{blue}{U \cdot U}}{{J}^{2}}}\right) \cdot J \]

      3. unpow247.9%

         \[\leadsto \left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{U \cdot U}{\color{blue}{J \cdot J}}}\right) \cdot J \]

   6. Simplified47.9%

      \[\leadsto \color{blue}{\left(-2 \cdot \sqrt{1 + 0.25 \cdot \frac{U \cdot U}{J \cdot J}}\right) \cdot J} \]

   7. Taylor expanded in U around 0 46.9%

      \[\leadsto \color{blue}{-2 \cdot J} \]

   if -2.7999999999999998e-28 < J < -4.49999999999999993e-188 or 5.2000000000000003e-244 < J < 4.70000000000000013e-108

   1. Initial program 51.9%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative51.9%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*51.9%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*51.9%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative51.9%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*51.8%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative51.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow251.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def79.3%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative79.3%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*79.3%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified79.3%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in U around -inf 46.8%

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

   if -4.49999999999999993e-188 < J < 5.2000000000000003e-244 or 4.70000000000000013e-108 < J < 1.79999999999999998e49

   1. Initial program 53.4%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative53.4%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*53.4%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*53.4%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative53.4%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*53.3%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative53.3%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow253.3%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def70.9%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative70.9%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*70.9%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified70.9%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in J around 0 57.0%

      \[\leadsto \color{blue}{-1 \cdot U} \]
   5. Step-by-step derivation

      1. neg-mul-157.0%

         \[\leadsto \color{blue}{-U} \]

   6. Simplified57.0%

      \[\leadsto \color{blue}{-U} \]
3. Recombined 3 regimes into one program.

4. Final simplification49.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;J \leq -2.8 \cdot 10^{-28}:\\ \;\;\;\;J \cdot -2\\ \mathbf{elif}\;J \leq -4.5 \cdot 10^{-188}:\\ \;\;\;\;U\\ \mathbf{elif}\;J \leq 5.2 \cdot 10^{-244}:\\ \;\;\;\;-U\\ \mathbf{elif}\;J \leq 4.7 \cdot 10^{-108}:\\ \;\;\;\;U\\ \mathbf{elif}\;J \leq 1.8 \cdot 10^{+49}:\\ \;\;\;\;-U\\ \mathbf{else}:\\ \;\;\;\;J \cdot -2\\ \end{array} \]

1. Split input into 2 regimes

2. if U < -1.7999999999999999e166 or 16000 < U < 1.69999999999999998e188 or 1.35999999999999995e281 < U

   1. Initial program 43.1%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative43.1%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*43.1%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*43.1%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative43.1%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*43.0%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative43.0%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow243.0%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def71.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative71.1%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*71.1%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified71.1%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in U around -inf 50.0%

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

   if -1.7999999999999999e166 < U < 16000 or 1.69999999999999998e188 < U < 1.35999999999999995e281

   1. Initial program 87.3%

      \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
   2. Step-by-step derivation

      1. *-commutative87.3%

         \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      2. associate-*l*87.3%

         \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

      3. associate-*r*87.3%

         \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

      4. *-commutative87.3%

         \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

      5. associate-*l*87.2%

         \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

      6. *-commutative87.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

      7. unpow287.2%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

      8. hypot-1-def93.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

      9. *-commutative93.8%

         \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

      10. associate-*l*93.8%

          \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

   3. Simplified93.8%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

   4. Taylor expanded in J around 0 27.2%

      \[\leadsto \color{blue}{-1 \cdot U} \]
   5. Step-by-step derivation

      1. neg-mul-127.2%

         \[\leadsto \color{blue}{-U} \]

   6. Simplified27.2%

      \[\leadsto \color{blue}{-U} \]
3. Recombined 2 regimes into one program.

4. Final simplification34.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;U \leq -1.8 \cdot 10^{+166}:\\ \;\;\;\;U\\ \mathbf{elif}\;U \leq 16000:\\ \;\;\;\;-U\\ \mathbf{elif}\;U \leq 1.7 \cdot 10^{+188}:\\ \;\;\;\;U\\ \mathbf{elif}\;U \leq 1.36 \cdot 10^{+281}:\\ \;\;\;\;-U\\ \mathbf{else}:\\ \;\;\;\;U\\ \end{array} \]

1. Initial program 73.3%

   \[\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \]
2. Step-by-step derivation

   1. *-commutative73.3%

      \[\leadsto \color{blue}{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right)} \]

   2. associate-*l*73.3%

      \[\leadsto \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \color{blue}{\left(-2 \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)\right)} \]

   3. associate-*r*73.3%

      \[\leadsto \color{blue}{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right) \cdot \left(J \cdot \cos \left(\frac{K}{2}\right)\right)} \]

   4. *-commutative73.3%

      \[\leadsto \color{blue}{\left(J \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)} \]

   5. associate-*l*73.2%

      \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot -2\right)\right)} \]

   6. *-commutative73.2%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(-2 \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}\right) \]

   7. unpow273.2%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \sqrt{1 + \color{blue}{\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)} \cdot \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}}}\right)\right) \]

   8. hypot-1-def86.6%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \color{blue}{\mathsf{hypot}\left(1, \frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}\right)\right) \]

   9. *-commutative86.6%

      \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{\left(J \cdot 2\right)} \cdot \cos \left(\frac{K}{2}\right)}\right)\right)\right) \]

   10. associate-*l*86.6%

       \[\leadsto J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{\color{blue}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}}\right)\right)\right) \]

3. Simplified86.6%

   \[\leadsto \color{blue}{J \cdot \left(\cos \left(\frac{K}{2}\right) \cdot \left(-2 \cdot \mathsf{hypot}\left(1, \frac{U}{J \cdot \left(2 \cdot \cos \left(\frac{K}{2}\right)\right)}\right)\right)\right)} \]

4. Taylor expanded in U around -inf 25.2%

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

5. Final simplification25.2%

   \[\leadsto U \]

herbie shell --seed 2023166 
(FPCore (J K U)
  :name "Maksimov and Kolovsky, Equation (3)"
  :precision binary64
  (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))))