mixedcos

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(x \cdot \left(x \cdot {s}^{2}\right)\right)}} \]

   2. associate-*r*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot {s}^{2}\right)}} \]

   3. associate-*r*67.4%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot \left(x \cdot x\right)\right) \cdot {s}^{2}}} \]

   4. unpow267.4%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(x \cdot x\right)\right) \cdot {s}^{2}} \]

   5. unswap-sqr80.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot x\right) \cdot \left(c \cdot x\right)\right)} \cdot {s}^{2}} \]

   6. unpow280.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\left(c \cdot x\right) \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot s\right)}} \]

   7. swap-sqr98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot x\right) \cdot s\right) \cdot \left(\left(c \cdot x\right) \cdot s\right)}} \]

   8. *-commutative98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)} \cdot \left(\left(c \cdot x\right) \cdot s\right)} \]

   9. *-commutative98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}} \]

   10. *-commutative98.7%

       \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \color{blue}{\left(x \cdot c\right)}\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]

   11. *-commutative98.7%

       \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \color{blue}{\left(x \cdot c\right)}\right)} \]

3. Simplified98.7%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)}} \]

4. Final simplification98.7%

   \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)} \]

1. Split input into 2 regimes

2. if x < -4.79999999999999997e-8 or 2.2499999999999999e-4 < x

   1. Initial program 72.4%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative72.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow270.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*76.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*76.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative76.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow276.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified76.4%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]
   4. Step-by-step derivation

      1. add-sqr-sqrt33.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)} \cdot \sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)}\right)}} \]

      2. pow233.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(\sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)}\right)}^{2}}} \]

      3. sqrt-prod33.5%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(\sqrt{x \cdot x} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}}^{2}} \]

      4. sqrt-prod13.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}^{2}} \]

      5. add-sqr-sqrt35.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{x} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}^{2}} \]

      6. sqrt-prod36.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \color{blue}{\left(\sqrt{c \cdot c} \cdot \sqrt{s}\right)}\right)}^{2}} \]

      7. sqrt-prod24.2%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \left(\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \sqrt{s}\right)\right)}^{2}} \]

      8. add-sqr-sqrt41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \left(\color{blue}{c} \cdot \sqrt{s}\right)\right)}^{2}} \]

   5. Applied egg-rr41.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(x \cdot \left(c \cdot \sqrt{s}\right)\right)}^{2}}} \]
   6. Step-by-step derivation

      1. associate-*r*41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(\left(x \cdot c\right) \cdot \sqrt{s}\right)}}^{2}} \]

      2. *-commutative41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{\left(c \cdot x\right)} \cdot \sqrt{s}\right)}^{2}} \]

      3. associate-*l*41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(c \cdot \left(x \cdot \sqrt{s}\right)\right)}}^{2}} \]

   7. Simplified41.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(c \cdot \left(x \cdot \sqrt{s}\right)\right)}^{2}}} \]
   8. Step-by-step derivation

      1. unpow241.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(c \cdot \left(x \cdot \sqrt{s}\right)\right) \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)}} \]

      2. associate-*r*41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\color{blue}{\left(\left(c \cdot x\right) \cdot \sqrt{s}\right)} \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)} \]

      3. *-commutative41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\color{blue}{\left(x \cdot c\right)} \cdot \sqrt{s}\right) \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)} \]

      4. associate-*r*41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \sqrt{s}\right) \cdot \color{blue}{\left(\left(c \cdot x\right) \cdot \sqrt{s}\right)}\right)} \]

      5. *-commutative41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \sqrt{s}\right) \cdot \left(\color{blue}{\left(x \cdot c\right)} \cdot \sqrt{s}\right)\right)} \]

      6. swap-sqr35.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot \left(x \cdot c\right)\right) \cdot \left(\sqrt{s} \cdot \sqrt{s}\right)\right)}} \]

      7. add-sqr-sqrt84.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \left(x \cdot c\right)\right) \cdot \color{blue}{s}\right)} \]

      8. associate-*r*96.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(x \cdot c\right) \cdot \left(\left(x \cdot c\right) \cdot s\right)\right)}} \]

      9. associate-*r*96.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot c\right) \cdot \color{blue}{\left(x \cdot \left(c \cdot s\right)\right)}\right)} \]

      10. *-commutative96.1%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot c\right) \cdot \left(x \cdot \color{blue}{\left(s \cdot c\right)}\right)\right)} \]

      11. associate-*r*91.1%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot x\right) \cdot \left(s \cdot c\right)\right)}} \]

   9. Applied egg-rr91.1%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot x\right) \cdot \left(s \cdot c\right)\right)}} \]

   if -4.79999999999999997e-8 < x < 2.2499999999999999e-4

   1. Initial program 72.9%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative72.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*67.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*66.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative66.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow266.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*69.2%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*74.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative74.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow274.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified74.7%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

   4. Taylor expanded in x around 0 68.4%

      \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   5. Step-by-step derivation

      1. unpow268.4%

         \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

      2. associate-*r*66.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

      3. *-commutative66.0%

         \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

      4. unpow266.0%

         \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

      5. unpow266.0%

         \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

   6. Simplified66.0%

      \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]

   7. Taylor expanded in c around 0 68.4%

      \[\leadsto \frac{1}{\color{blue}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   8. Step-by-step derivation

      1. unpow268.4%

         \[\leadsto \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]

      2. associate-*r*66.0%

         \[\leadsto \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      3. unpow266.0%

         \[\leadsto \frac{1}{\left(\color{blue}{\left(s \cdot s\right)} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)} \]

      4. unpow266.0%

         \[\leadsto \frac{1}{\left(\left(s \cdot s\right) \cdot \color{blue}{\left(c \cdot c\right)}\right) \cdot \left(x \cdot x\right)} \]

      5. swap-sqr76.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

      6. swap-sqr97.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right) \cdot \left(\left(s \cdot c\right) \cdot x\right)}} \]

      7. *-commutative97.0%

         \[\leadsto \frac{1}{\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)} \cdot \left(\left(s \cdot c\right) \cdot x\right)} \]

      8. *-commutative97.0%

         \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}} \]

      9. unpow297.0%

         \[\leadsto \frac{1}{\color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{2}}} \]

      10. *-commutative97.0%

          \[\leadsto \frac{1}{{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right)}}^{2}} \]

      11. associate-*r*98.8%

          \[\leadsto \frac{1}{{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}}^{2}} \]

   9. Simplified98.8%

      \[\leadsto \frac{1}{\color{blue}{{\left(s \cdot \left(c \cdot x\right)\right)}^{2}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification94.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4.8 \cdot 10^{-8} \lor \neg \left(x \leq 0.000225\right):\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot c\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{{\left(s \cdot \left(x \cdot c\right)\right)}^{2}}\\ \end{array} \]

1. Split input into 2 regimes

2. if x < -5.00000000000000018e-11 or 1.9000000000000001e-4 < x

   1. Initial program 72.4%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative72.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative70.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow270.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*76.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*76.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative76.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow276.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified76.4%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]
   4. Step-by-step derivation

      1. add-sqr-sqrt33.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)} \cdot \sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)}\right)}} \]

      2. pow233.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(\sqrt{\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)}\right)}^{2}}} \]

      3. sqrt-prod33.5%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(\sqrt{x \cdot x} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}}^{2}} \]

      4. sqrt-prod13.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}^{2}} \]

      5. add-sqr-sqrt35.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{x} \cdot \sqrt{\left(c \cdot c\right) \cdot s}\right)}^{2}} \]

      6. sqrt-prod36.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \color{blue}{\left(\sqrt{c \cdot c} \cdot \sqrt{s}\right)}\right)}^{2}} \]

      7. sqrt-prod24.2%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \left(\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \sqrt{s}\right)\right)}^{2}} \]

      8. add-sqr-sqrt41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(x \cdot \left(\color{blue}{c} \cdot \sqrt{s}\right)\right)}^{2}} \]

   5. Applied egg-rr41.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(x \cdot \left(c \cdot \sqrt{s}\right)\right)}^{2}}} \]
   6. Step-by-step derivation

      1. associate-*r*41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(\left(x \cdot c\right) \cdot \sqrt{s}\right)}}^{2}} \]

      2. *-commutative41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\left(\color{blue}{\left(c \cdot x\right)} \cdot \sqrt{s}\right)}^{2}} \]

      3. associate-*l*41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot {\color{blue}{\left(c \cdot \left(x \cdot \sqrt{s}\right)\right)}}^{2}} \]

   7. Simplified41.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{{\left(c \cdot \left(x \cdot \sqrt{s}\right)\right)}^{2}}} \]
   8. Step-by-step derivation

      1. unpow241.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(c \cdot \left(x \cdot \sqrt{s}\right)\right) \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)}} \]

      2. associate-*r*41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\color{blue}{\left(\left(c \cdot x\right) \cdot \sqrt{s}\right)} \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)} \]

      3. *-commutative41.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\color{blue}{\left(x \cdot c\right)} \cdot \sqrt{s}\right) \cdot \left(c \cdot \left(x \cdot \sqrt{s}\right)\right)\right)} \]

      4. associate-*r*41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \sqrt{s}\right) \cdot \color{blue}{\left(\left(c \cdot x\right) \cdot \sqrt{s}\right)}\right)} \]

      5. *-commutative41.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \sqrt{s}\right) \cdot \left(\color{blue}{\left(x \cdot c\right)} \cdot \sqrt{s}\right)\right)} \]

      6. swap-sqr35.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot \left(x \cdot c\right)\right) \cdot \left(\sqrt{s} \cdot \sqrt{s}\right)\right)}} \]

      7. add-sqr-sqrt84.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(\left(x \cdot c\right) \cdot \left(x \cdot c\right)\right) \cdot \color{blue}{s}\right)} \]

      8. associate-*r*96.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(x \cdot c\right) \cdot \left(\left(x \cdot c\right) \cdot s\right)\right)}} \]

      9. *-commutative96.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot c\right) \cdot \color{blue}{\left(s \cdot \left(x \cdot c\right)\right)}\right)} \]

      10. associate-*r*95.5%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot c\right) \cdot \color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}\right)} \]

      11. *-commutative95.5%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot c\right) \cdot \left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)\right)} \]

      12. associate-*r*93.4%

          \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot \left(x \cdot s\right)\right) \cdot c\right)}} \]

   9. Applied egg-rr93.4%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \color{blue}{\left(\left(\left(x \cdot c\right) \cdot \left(x \cdot s\right)\right) \cdot c\right)}} \]

   if -5.00000000000000018e-11 < x < 1.9000000000000001e-4

   1. Initial program 72.9%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative72.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*67.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*66.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative66.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow266.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*69.2%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*74.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative74.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow274.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified74.7%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

   4. Taylor expanded in x around 0 68.4%

      \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   5. Step-by-step derivation

      1. unpow268.4%

         \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

      2. associate-*r*66.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

      3. *-commutative66.0%

         \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

      4. unpow266.0%

         \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

      5. unpow266.0%

         \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

   6. Simplified66.0%

      \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]

   7. Taylor expanded in c around 0 68.4%

      \[\leadsto \frac{1}{\color{blue}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   8. Step-by-step derivation

      1. unpow268.4%

         \[\leadsto \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]

      2. associate-*r*66.0%

         \[\leadsto \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      3. unpow266.0%

         \[\leadsto \frac{1}{\left(\color{blue}{\left(s \cdot s\right)} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)} \]

      4. unpow266.0%

         \[\leadsto \frac{1}{\left(\left(s \cdot s\right) \cdot \color{blue}{\left(c \cdot c\right)}\right) \cdot \left(x \cdot x\right)} \]

      5. swap-sqr76.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

      6. swap-sqr97.0%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right) \cdot \left(\left(s \cdot c\right) \cdot x\right)}} \]

      7. *-commutative97.0%

         \[\leadsto \frac{1}{\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)} \cdot \left(\left(s \cdot c\right) \cdot x\right)} \]

      8. *-commutative97.0%

         \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}} \]

      9. unpow297.0%

         \[\leadsto \frac{1}{\color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{2}}} \]

      10. *-commutative97.0%

          \[\leadsto \frac{1}{{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right)}}^{2}} \]

      11. associate-*r*98.8%

          \[\leadsto \frac{1}{{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}}^{2}} \]

   9. Simplified98.8%

      \[\leadsto \frac{1}{\color{blue}{{\left(s \cdot \left(c \cdot x\right)\right)}^{2}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification96.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -5 \cdot 10^{-11} \lor \neg \left(x \leq 0.00019\right):\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(c \cdot \left(\left(x \cdot c\right) \cdot \left(x \cdot s\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{{\left(s \cdot \left(x \cdot c\right)\right)}^{2}}\\ \end{array} \]

1. Split input into 3 regimes

2. if c < -5.9e85

   1. Initial program 58.1%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative58.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*55.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*55.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative55.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow255.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*65.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*65.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative65.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow265.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified65.6%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

   4. Taylor expanded in x around 0 53.0%

      \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   5. Step-by-step derivation

      1. unpow253.0%

         \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

      2. associate-*r*53.1%

         \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

      3. *-commutative53.1%

         \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

      4. unpow253.1%

         \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

      5. unpow253.1%

         \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

   6. Simplified53.1%

      \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
   7. Step-by-step derivation

      1. inv-pow53.1%

         \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

      2. *-commutative53.1%

         \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

      3. *-commutative53.1%

         \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

      4. associate-*r*53.3%

         \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

      5. swap-sqr66.1%

         \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

      6. swap-sqr84.2%

         \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

      7. *-commutative84.2%

         \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

      8. *-commutative84.2%

         \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

      9. *-commutative84.2%

         \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

      10. *-commutative84.2%

          \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

      11. pow-prod-down84.2%

          \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

      12. pow-sqr84.2%

          \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

      13. metadata-eval84.2%

          \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

      14. *-commutative84.2%

          \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

      15. *-commutative84.2%

          \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

      16. associate-*r*88.8%

          \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

      17. sqr-pow88.7%

          \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

      18. pow288.7%

          \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

   8. Applied egg-rr88.7%

      \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
   9. Step-by-step derivation

      1. unpow288.7%

         \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

      2. associate-/r*88.7%

         \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{\frac{1}{x}}{s \cdot c}} \]

      3. frac-times88.8%

         \[\leadsto \color{blue}{\frac{1 \cdot \frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

      4. *-un-lft-identity88.8%

         \[\leadsto \frac{\color{blue}{\frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

   10. Applied egg-rr88.8%

       \[\leadsto \color{blue}{\frac{\frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]
   11. Step-by-step derivation

       1. *-un-lft-identity88.8%

          \[\leadsto \frac{\color{blue}{1 \cdot \frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

       2. frac-times88.7%

          \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{\frac{1}{x}}{s \cdot c}} \]

       3. *-commutative88.7%

          \[\leadsto \frac{1}{\color{blue}{\left(s \cdot c\right) \cdot x}} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

       4. *-commutative88.7%

          \[\leadsto \frac{1}{\color{blue}{\left(c \cdot s\right)} \cdot x} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

       5. associate-/l/88.7%

          \[\leadsto \color{blue}{\frac{\frac{1}{x}}{c \cdot s}} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

       6. *-commutative88.7%

          \[\leadsto \frac{\frac{1}{x}}{c \cdot s} \cdot \frac{\frac{1}{x}}{\color{blue}{c \cdot s}} \]

       7. associate-/r*88.8%

          \[\leadsto \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s}} \cdot \frac{\frac{1}{x}}{c \cdot s} \]

       8. associate-/r*93.3%

          \[\leadsto \frac{\frac{\frac{1}{x}}{c}}{s} \cdot \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s}} \]

   12. Applied egg-rr93.3%

       \[\leadsto \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s} \cdot \frac{\frac{\frac{1}{x}}{c}}{s}} \]

   if -5.9e85 < c < -7.60000000000000025e-124

   1. Initial program 88.2%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative88.2%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*84.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*81.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative81.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow281.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*84.0%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*87.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative87.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow287.9%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified87.9%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

   if -7.60000000000000025e-124 < c

   1. Initial program 71.6%

      \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
   2. Step-by-step derivation

      1. *-commutative71.6%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

      2. associate-*l*67.7%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

      3. associate-*r*67.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

      4. *-commutative67.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

      5. unpow267.1%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

      6. associate-*r*71.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

      7. associate-*r*74.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

      8. *-commutative74.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

      9. unpow274.3%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

   3. Simplified74.3%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

   4. Taylor expanded in x around inf 65.4%

      \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   5. Step-by-step derivation

      1. unpow265.4%

         \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

      2. *-commutative65.4%

         \[\leadsto \frac{\cos \color{blue}{\left(x \cdot 2\right)}}{\left(s \cdot s\right) \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

      3. *-commutative65.4%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\color{blue}{\left({c}^{2} \cdot {x}^{2}\right) \cdot \left(s \cdot s\right)}} \]

      4. associate-*r*67.7%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\color{blue}{{c}^{2} \cdot \left({x}^{2} \cdot \left(s \cdot s\right)\right)}} \]

      5. unpow267.7%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\color{blue}{\left(c \cdot c\right)} \cdot \left({x}^{2} \cdot \left(s \cdot s\right)\right)} \]

      6. unpow267.7%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\left(c \cdot c\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot \left(s \cdot s\right)\right)} \]

      7. swap-sqr78.6%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\left(c \cdot c\right) \cdot \color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)}} \]

      8. swap-sqr98.0%

         \[\leadsto \frac{\cos \left(x \cdot 2\right)}{\color{blue}{\left(c \cdot \left(x \cdot s\right)\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)}} \]

      9. associate-/r*98.0%

         \[\leadsto \color{blue}{\frac{\frac{\cos \left(x \cdot 2\right)}{c \cdot \left(x \cdot s\right)}}{c \cdot \left(x \cdot s\right)}} \]

      10. *-rgt-identity98.0%

          \[\leadsto \frac{\color{blue}{\frac{\cos \left(x \cdot 2\right)}{c \cdot \left(x \cdot s\right)} \cdot 1}}{c \cdot \left(x \cdot s\right)} \]

      11. associate-*r/98.0%

          \[\leadsto \color{blue}{\frac{\cos \left(x \cdot 2\right)}{c \cdot \left(x \cdot s\right)} \cdot \frac{1}{c \cdot \left(x \cdot s\right)}} \]

      12. *-rgt-identity98.0%

          \[\leadsto \color{blue}{\left(\frac{\cos \left(x \cdot 2\right)}{c \cdot \left(x \cdot s\right)} \cdot 1\right)} \cdot \frac{1}{c \cdot \left(x \cdot s\right)} \]

      13. associate-*l/98.0%

          \[\leadsto \color{blue}{\frac{\cos \left(x \cdot 2\right) \cdot 1}{c \cdot \left(x \cdot s\right)}} \cdot \frac{1}{c \cdot \left(x \cdot s\right)} \]

      14. associate-*r/97.9%

          \[\leadsto \color{blue}{\left(\cos \left(x \cdot 2\right) \cdot \frac{1}{c \cdot \left(x \cdot s\right)}\right)} \cdot \frac{1}{c \cdot \left(x \cdot s\right)} \]

      15. associate-*r*97.9%

          \[\leadsto \color{blue}{\cos \left(x \cdot 2\right) \cdot \left(\frac{1}{c \cdot \left(x \cdot s\right)} \cdot \frac{1}{c \cdot \left(x \cdot s\right)}\right)} \]

   6. Simplified99.1%

      \[\leadsto \color{blue}{\cos \left(2 \cdot x\right) \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{-2}} \]
   7. Step-by-step derivation

      1. associate-*r*98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\color{blue}{\left(\left(x \cdot s\right) \cdot c\right)}}^{-2} \]

      2. *-commutative98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)}^{-2} \]

      3. *-commutative98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}}^{-2} \]

      4. metadata-eval98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{\left(2 \cdot -1\right)}} \]

      5. pow-sqr97.9%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot \color{blue}{\left({\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}\right)} \]

      6. pow-prod-down98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot \color{blue}{{\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(c \cdot \left(s \cdot x\right)\right)\right)}^{-1}} \]

      7. *-commutative98.0%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\left(\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)} \cdot \left(c \cdot \left(s \cdot x\right)\right)\right)}^{-1} \]

      8. associate-*r*97.1%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot {\left(\color{blue}{\left(s \cdot \left(x \cdot c\right)\right)} \cdot \left(c \cdot \left(s \cdot x\right)\right)\right)}^{-1} \]

      9. inv-pow97.1%

         \[\leadsto \cos \left(2 \cdot x\right) \cdot \color{blue}{\frac{1}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(c \cdot \left(s \cdot x\right)\right)}} \]

      10. div-inv97.1%

          \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(c \cdot \left(s \cdot x\right)\right)}} \]

      11. associate-/r*97.1%

          \[\leadsto \color{blue}{\frac{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(x \cdot c\right)}}{c \cdot \left(s \cdot x\right)}} \]

      12. clear-num97.2%

          \[\leadsto \color{blue}{\frac{1}{\frac{c \cdot \left(s \cdot x\right)}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(x \cdot c\right)}}}} \]

      13. *-commutative97.2%

          \[\leadsto \frac{1}{\frac{\color{blue}{\left(s \cdot x\right) \cdot c}}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(x \cdot c\right)}}} \]

      14. *-commutative97.2%

          \[\leadsto \frac{1}{\frac{\color{blue}{\left(x \cdot s\right)} \cdot c}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(x \cdot c\right)}}} \]

      15. associate-*r*98.2%

          \[\leadsto \frac{1}{\frac{\color{blue}{x \cdot \left(s \cdot c\right)}}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(x \cdot c\right)}}} \]

      16. *-commutative98.2%

          \[\leadsto \frac{1}{\frac{x \cdot \left(s \cdot c\right)}{\frac{\cos \color{blue}{\left(x \cdot 2\right)}}{s \cdot \left(x \cdot c\right)}}} \]

      17. associate-*r*97.5%

          \[\leadsto \frac{1}{\frac{x \cdot \left(s \cdot c\right)}{\frac{\cos \left(x \cdot 2\right)}{\color{blue}{\left(s \cdot x\right) \cdot c}}}} \]

      18. *-commutative97.5%

          \[\leadsto \frac{1}{\frac{x \cdot \left(s \cdot c\right)}{\frac{\cos \left(x \cdot 2\right)}{\color{blue}{\left(x \cdot s\right)} \cdot c}}} \]

      19. associate-*r*99.1%

          \[\leadsto \frac{1}{\frac{x \cdot \left(s \cdot c\right)}{\frac{\cos \left(x \cdot 2\right)}{\color{blue}{x \cdot \left(s \cdot c\right)}}}} \]

   8. Applied egg-rr99.1%

      \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot \left(s \cdot c\right)}{\frac{\cos \left(x \cdot 2\right)}{x \cdot \left(s \cdot c\right)}}}} \]

   9. Taylor expanded in x around 0 60.9%

      \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
   10. Step-by-step derivation

       1. unpow260.9%

          \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

       2. unpow260.9%

          \[\leadsto \frac{1}{\left(s \cdot s\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot {x}^{2}\right)} \]

       3. unpow260.9%

          \[\leadsto \frac{1}{\left(s \cdot s\right) \cdot \left(\left(c \cdot c\right) \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]

       4. *-commutative60.9%

          \[\leadsto \frac{1}{\left(s \cdot s\right) \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(c \cdot c\right)\right)}} \]

       5. swap-sqr70.6%

          \[\leadsto \frac{1}{\left(s \cdot s\right) \cdot \color{blue}{\left(\left(x \cdot c\right) \cdot \left(x \cdot c\right)\right)}} \]

       6. swap-sqr82.6%

          \[\leadsto \frac{1}{\color{blue}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)}} \]

       7. *-commutative82.6%

          \[\leadsto \frac{1}{\left(s \cdot \color{blue}{\left(c \cdot x\right)}\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)} \]

       8. associate-*r*82.1%

          \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right)} \cdot \left(s \cdot \left(x \cdot c\right)\right)} \]

       9. *-commutative82.1%

          \[\leadsto \frac{1}{\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)} \cdot \left(s \cdot \left(x \cdot c\right)\right)} \]

       10. *-commutative82.1%

           \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot \color{blue}{\left(c \cdot x\right)}\right)} \]

       11. associate-*r*82.5%

           \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(\left(s \cdot c\right) \cdot x\right)}} \]

       12. *-commutative82.5%

           \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}} \]

       13. associate-/r*82.5%

           \[\leadsto \color{blue}{\frac{\frac{1}{x \cdot \left(s \cdot c\right)}}{x \cdot \left(s \cdot c\right)}} \]

       14. *-lft-identity82.5%

           \[\leadsto \frac{\color{blue}{1 \cdot \frac{1}{x \cdot \left(s \cdot c\right)}}}{x \cdot \left(s \cdot c\right)} \]

       15. associate-*l/82.5%

           \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

       16. unpow-182.5%

           \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{-1}} \cdot \frac{1}{x \cdot \left(s \cdot c\right)} \]

       17. unpow-182.5%

           \[\leadsto {\left(x \cdot \left(s \cdot c\right)\right)}^{-1} \cdot \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{-1}} \]

       18. pow-sqr82.5%

           \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(2 \cdot -1\right)}} \]

       19. metadata-eval82.5%

           \[\leadsto {\left(x \cdot \left(s \cdot c\right)\right)}^{\color{blue}{-2}} \]

   11. Simplified82.4%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-2}} \]
3. Recombined 3 regimes into one program.

4. Final simplification85.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;c \leq -5.9 \cdot 10^{+85}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{c}}{s} \cdot \frac{\frac{\frac{1}{x}}{c}}{s}\\ \mathbf{elif}\;c \leq -7.6 \cdot 10^{-124}:\\ \;\;\;\;\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(s \cdot \left(c \cdot c\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;{\left(c \cdot \left(x \cdot s\right)\right)}^{-2}\\ \end{array} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(x \cdot \left(x \cdot {s}^{2}\right)\right)}} \]

   2. associate-*r*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot {s}^{2}\right)}} \]

   3. associate-*r*67.4%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot \left(x \cdot x\right)\right) \cdot {s}^{2}}} \]

   4. unpow267.4%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(x \cdot x\right)\right) \cdot {s}^{2}} \]

   5. unswap-sqr80.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot x\right) \cdot \left(c \cdot x\right)\right)} \cdot {s}^{2}} \]

   6. unpow280.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\left(c \cdot x\right) \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot s\right)}} \]

   7. swap-sqr98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(c \cdot x\right) \cdot s\right) \cdot \left(\left(c \cdot x\right) \cdot s\right)}} \]

   8. *-commutative98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)} \cdot \left(\left(c \cdot x\right) \cdot s\right)} \]

   9. *-commutative98.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(c \cdot x\right)\right) \cdot \color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}} \]

   10. *-commutative98.7%

       \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \color{blue}{\left(x \cdot c\right)}\right) \cdot \left(s \cdot \left(c \cdot x\right)\right)} \]

   11. *-commutative98.7%

       \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \color{blue}{\left(x \cdot c\right)}\right)} \]

3. Simplified98.7%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot \left(x \cdot c\right)\right)}} \]

4. Taylor expanded in s around 0 96.2%

   \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}} \]

5. Final simplification96.2%

   \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(c \cdot \left(x \cdot s\right)\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]

7. Taylor expanded in c around 0 63.0%

   \[\leadsto \frac{1}{\color{blue}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
8. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   3. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(s \cdot s\right)} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left(\left(s \cdot s\right) \cdot \color{blue}{\left(c \cdot c\right)}\right) \cdot \left(x \cdot x\right)} \]

   5. swap-sqr71.9%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

   6. swap-sqr83.6%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right) \cdot \left(\left(s \cdot c\right) \cdot x\right)}} \]

   7. *-commutative83.6%

      \[\leadsto \frac{1}{\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)} \cdot \left(\left(s \cdot c\right) \cdot x\right)} \]

   8. *-commutative83.6%

      \[\leadsto \frac{1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}} \]

   9. unpow283.6%

      \[\leadsto \frac{1}{\color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{2}}} \]

   10. *-commutative83.6%

       \[\leadsto \frac{1}{{\color{blue}{\left(\left(s \cdot c\right) \cdot x\right)}}^{2}} \]

   11. associate-*r*84.5%

       \[\leadsto \frac{1}{{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)}}^{2}} \]

9. Simplified84.5%

   \[\leadsto \frac{1}{\color{blue}{{\left(s \cdot \left(c \cdot x\right)\right)}^{2}}} \]

10. Final simplification84.5%

    \[\leadsto \frac{1}{{\left(s \cdot \left(x \cdot c\right)\right)}^{2}} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. inv-pow62.0%

      \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

   2. *-commutative62.0%

      \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

   3. *-commutative62.0%

      \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

   4. associate-*r*62.8%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

   5. swap-sqr72.2%

      \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

   6. swap-sqr82.9%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

   7. *-commutative82.9%

      \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   8. *-commutative82.9%

      \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   9. *-commutative82.9%

      \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

   10. *-commutative82.9%

       \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

   11. pow-prod-down82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

   12. pow-sqr82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

   13. metadata-eval82.9%

       \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   14. *-commutative82.9%

       \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

   15. *-commutative82.9%

       \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

   16. associate-*r*83.6%

       \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

   17. sqr-pow83.6%

       \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

   18. pow283.6%

       \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

8. Applied egg-rr83.6%

   \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
9. Step-by-step derivation

   1. unpow283.6%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

   2. associate-/r*83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{\frac{1}{x}}{s \cdot c}} \]

   3. frac-times81.8%

      \[\leadsto \color{blue}{\frac{1 \cdot \frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

   4. *-un-lft-identity81.8%

      \[\leadsto \frac{\color{blue}{\frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

10. Applied egg-rr81.8%

    \[\leadsto \color{blue}{\frac{\frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]
11. Step-by-step derivation

    1. *-un-lft-identity81.8%

       \[\leadsto \frac{\color{blue}{1 \cdot \frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

    2. frac-times83.6%

       \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{\frac{1}{x}}{s \cdot c}} \]

    3. *-commutative83.6%

       \[\leadsto \frac{1}{\color{blue}{\left(s \cdot c\right) \cdot x}} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

    4. *-commutative83.6%

       \[\leadsto \frac{1}{\color{blue}{\left(c \cdot s\right)} \cdot x} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

    5. associate-/l/83.6%

       \[\leadsto \color{blue}{\frac{\frac{1}{x}}{c \cdot s}} \cdot \frac{\frac{1}{x}}{s \cdot c} \]

    6. *-commutative83.6%

       \[\leadsto \frac{\frac{1}{x}}{c \cdot s} \cdot \frac{\frac{1}{x}}{\color{blue}{c \cdot s}} \]

    7. associate-/r*82.9%

       \[\leadsto \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s}} \cdot \frac{\frac{1}{x}}{c \cdot s} \]

    8. associate-/r*84.0%

       \[\leadsto \frac{\frac{\frac{1}{x}}{c}}{s} \cdot \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s}} \]

12. Applied egg-rr84.0%

    \[\leadsto \color{blue}{\frac{\frac{\frac{1}{x}}{c}}{s} \cdot \frac{\frac{\frac{1}{x}}{c}}{s}} \]

13. Final simplification84.0%

    \[\leadsto \frac{\frac{\frac{1}{x}}{c}}{s} \cdot \frac{\frac{\frac{1}{x}}{c}}{s} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. inv-pow62.0%

      \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

   2. *-commutative62.0%

      \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

   3. *-commutative62.0%

      \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

   4. associate-*r*62.8%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

   5. swap-sqr72.2%

      \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

   6. swap-sqr82.9%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

   7. *-commutative82.9%

      \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   8. *-commutative82.9%

      \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   9. *-commutative82.9%

      \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

   10. *-commutative82.9%

       \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

   11. pow-prod-down82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

   12. pow-sqr82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

   13. metadata-eval82.9%

       \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   14. *-commutative82.9%

       \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

   15. *-commutative82.9%

       \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

   16. associate-*r*83.6%

       \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

   17. sqr-pow83.6%

       \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

   18. pow283.6%

       \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

8. Applied egg-rr83.6%

   \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
9. Step-by-step derivation

   1. unpow283.6%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

   2. frac-2neg83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{-1}{-x \cdot \left(s \cdot c\right)}} \]

   3. metadata-eval83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{\color{blue}{-1}}{-x \cdot \left(s \cdot c\right)} \]

   4. frac-times83.6%

      \[\leadsto \color{blue}{\frac{1 \cdot -1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(-x \cdot \left(s \cdot c\right)\right)}} \]

   5. metadata-eval83.6%

      \[\leadsto \frac{\color{blue}{-1}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(-x \cdot \left(s \cdot c\right)\right)} \]

10. Applied egg-rr83.6%

    \[\leadsto \color{blue}{\frac{-1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(-x \cdot \left(s \cdot c\right)\right)}} \]

11. Final simplification83.6%

    \[\leadsto \frac{-1}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(x \cdot \left(s \cdot \left(-c\right)\right)\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]

7. Taylor expanded in c around 0 63.0%

   \[\leadsto \frac{1}{\color{blue}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
8. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot \color{blue}{\left(x \cdot x\right)}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({s}^{2} \cdot {c}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right)} \cdot \left(x \cdot x\right)} \]

   4. associate-*r*62.8%

      \[\leadsto \frac{1}{\color{blue}{{c}^{2} \cdot \left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   5. unpow262.8%

      \[\leadsto \frac{1}{\color{blue}{\left(c \cdot c\right)} \cdot \left({s}^{2} \cdot \left(x \cdot x\right)\right)} \]

   6. unpow262.8%

      \[\leadsto \frac{1}{\left(c \cdot c\right) \cdot \left(\color{blue}{\left(s \cdot s\right)} \cdot \left(x \cdot x\right)\right)} \]

9. Simplified62.8%

   \[\leadsto \frac{1}{\color{blue}{\left(c \cdot c\right) \cdot \left(\left(s \cdot s\right) \cdot \left(x \cdot x\right)\right)}} \]

10. Final simplification62.8%

    \[\leadsto \frac{1}{\left(c \cdot c\right) \cdot \left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

   2. swap-sqr71.9%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

   3. pow271.9%

      \[\leadsto \frac{1}{\color{blue}{{\left(s \cdot c\right)}^{2}} \cdot \left(x \cdot x\right)} \]

8. Applied egg-rr71.9%

   \[\leadsto \frac{1}{\color{blue}{{\left(s \cdot c\right)}^{2}} \cdot \left(x \cdot x\right)} \]
9. Step-by-step derivation

   1. unpow271.9%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

10. Applied egg-rr71.9%

    \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \cdot \left(x \cdot x\right)} \]

11. Final simplification71.9%

    \[\leadsto \frac{1}{\left(x \cdot x\right) \cdot \left(\left(s \cdot c\right) \cdot \left(s \cdot c\right)\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. inv-pow62.0%

      \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

   2. *-commutative62.0%

      \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

   3. *-commutative62.0%

      \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

   4. associate-*r*62.8%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

   5. swap-sqr72.2%

      \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

   6. swap-sqr82.9%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

   7. *-commutative82.9%

      \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   8. *-commutative82.9%

      \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   9. *-commutative82.9%

      \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

   10. *-commutative82.9%

       \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

   11. pow-prod-down82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

   12. pow-sqr82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

   13. metadata-eval82.9%

       \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   14. *-commutative82.9%

       \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

   15. *-commutative82.9%

       \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

   16. associate-*r*83.6%

       \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

   17. sqr-pow83.6%

       \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

   18. pow283.6%

       \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

8. Applied egg-rr83.6%

   \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
9. Step-by-step derivation

   1. unpow283.6%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

   2. associate-/r*83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{\frac{1}{x}}{s \cdot c}} \]

   3. frac-times81.8%

      \[\leadsto \color{blue}{\frac{1 \cdot \frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

   4. *-un-lft-identity81.8%

      \[\leadsto \frac{\color{blue}{\frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

10. Applied egg-rr81.8%

    \[\leadsto \color{blue}{\frac{\frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

11. Taylor expanded in x around 0 80.0%

    \[\leadsto \frac{\frac{1}{x}}{\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(s \cdot c\right)} \]

12. Final simplification80.0%

    \[\leadsto \frac{\frac{1}{x}}{\left(c \cdot \left(x \cdot s\right)\right) \cdot \left(s \cdot c\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. inv-pow62.0%

      \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

   2. *-commutative62.0%

      \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

   3. *-commutative62.0%

      \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

   4. associate-*r*62.8%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

   5. swap-sqr72.2%

      \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

   6. swap-sqr82.9%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

   7. *-commutative82.9%

      \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   8. *-commutative82.9%

      \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   9. *-commutative82.9%

      \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

   10. *-commutative82.9%

       \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

   11. pow-prod-down82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

   12. pow-sqr82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

   13. metadata-eval82.9%

       \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   14. *-commutative82.9%

       \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

   15. *-commutative82.9%

       \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

   16. associate-*r*83.6%

       \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

   17. sqr-pow83.6%

       \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

   18. pow283.6%

       \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

8. Applied egg-rr83.6%

   \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
9. Step-by-step derivation

   1. unpow283.6%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

   2. associate-/r*83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{\frac{1}{x}}{s \cdot c}} \]

   3. frac-times81.8%

      \[\leadsto \color{blue}{\frac{1 \cdot \frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

   4. *-un-lft-identity81.8%

      \[\leadsto \frac{\color{blue}{\frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

10. Applied egg-rr81.8%

    \[\leadsto \color{blue}{\frac{\frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

11. Taylor expanded in x around 0 80.0%

    \[\leadsto \frac{\frac{1}{x}}{\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(s \cdot c\right)} \]
12. Step-by-step derivation

    1. associate-*r*81.8%

       \[\leadsto \frac{\frac{1}{x}}{\color{blue}{\left(\left(c \cdot s\right) \cdot x\right)} \cdot \left(s \cdot c\right)} \]

    2. *-commutative81.8%

       \[\leadsto \frac{\frac{1}{x}}{\left(\color{blue}{\left(s \cdot c\right)} \cdot x\right) \cdot \left(s \cdot c\right)} \]

    3. associate-*r*81.5%

       \[\leadsto \frac{\frac{1}{x}}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)} \cdot \left(s \cdot c\right)} \]

13. Simplified81.5%

    \[\leadsto \frac{\frac{1}{x}}{\color{blue}{\left(s \cdot \left(c \cdot x\right)\right)} \cdot \left(s \cdot c\right)} \]

14. Final simplification81.5%

    \[\leadsto \frac{\frac{1}{x}}{\left(s \cdot \left(x \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

1. Initial program 72.7%

   \[\frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\left(x \cdot {s}^{2}\right) \cdot x\right)} \]
2. Step-by-step derivation

   1. *-commutative72.7%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \left(\color{blue}{\left({s}^{2} \cdot x\right)} \cdot x\right)} \]

   2. associate-*l*68.9%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{{c}^{2} \cdot \color{blue}{\left({s}^{2} \cdot \left(x \cdot x\right)\right)}} \]

   3. associate-*r*68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left({c}^{2} \cdot {s}^{2}\right) \cdot \left(x \cdot x\right)}} \]

   4. *-commutative68.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot {s}^{2}\right)}} \]

   5. unpow268.0%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \left({c}^{2} \cdot \color{blue}{\left(s \cdot s\right)}\right)} \]

   6. associate-*r*72.8%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(x \cdot x\right) \cdot \color{blue}{\left(\left({c}^{2} \cdot s\right) \cdot s\right)}} \]

   7. associate-*r*75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{\left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right) \cdot s}} \]

   8. *-commutative75.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\color{blue}{s \cdot \left(\left(x \cdot x\right) \cdot \left({c}^{2} \cdot s\right)\right)}} \]

   9. unpow275.6%

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(c \cdot c\right)} \cdot s\right)\right)} \]

3. Simplified75.6%

   \[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{s \cdot \left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot s\right)\right)}} \]

4. Taylor expanded in x around 0 63.0%

   \[\leadsto \color{blue}{\frac{1}{{s}^{2} \cdot \left({c}^{2} \cdot {x}^{2}\right)}} \]
5. Step-by-step derivation

   1. unpow263.0%

      \[\leadsto \frac{1}{\color{blue}{\left(s \cdot s\right)} \cdot \left({c}^{2} \cdot {x}^{2}\right)} \]

   2. associate-*r*62.0%

      \[\leadsto \frac{1}{\color{blue}{\left(\left(s \cdot s\right) \cdot {c}^{2}\right) \cdot {x}^{2}}} \]

   3. *-commutative62.0%

      \[\leadsto \frac{1}{\color{blue}{\left({c}^{2} \cdot \left(s \cdot s\right)\right)} \cdot {x}^{2}} \]

   4. unpow262.0%

      \[\leadsto \frac{1}{\left({c}^{2} \cdot \left(s \cdot s\right)\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]

   5. unpow262.0%

      \[\leadsto \frac{1}{\left(\color{blue}{\left(c \cdot c\right)} \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)} \]

6. Simplified62.0%

   \[\leadsto \color{blue}{\frac{1}{\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)}} \]
7. Step-by-step derivation

   1. inv-pow62.0%

      \[\leadsto \color{blue}{{\left(\left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right) \cdot \left(x \cdot x\right)\right)}^{-1}} \]

   2. *-commutative62.0%

      \[\leadsto {\color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(c \cdot c\right) \cdot \left(s \cdot s\right)\right)\right)}}^{-1} \]

   3. *-commutative62.0%

      \[\leadsto {\left(\left(x \cdot x\right) \cdot \color{blue}{\left(\left(s \cdot s\right) \cdot \left(c \cdot c\right)\right)}\right)}^{-1} \]

   4. associate-*r*62.8%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot x\right) \cdot \left(s \cdot s\right)\right) \cdot \left(c \cdot c\right)\right)}}^{-1} \]

   5. swap-sqr72.2%

      \[\leadsto {\left(\color{blue}{\left(\left(x \cdot s\right) \cdot \left(x \cdot s\right)\right)} \cdot \left(c \cdot c\right)\right)}^{-1} \]

   6. swap-sqr82.9%

      \[\leadsto {\color{blue}{\left(\left(\left(x \cdot s\right) \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}}^{-1} \]

   7. *-commutative82.9%

      \[\leadsto {\left(\left(\color{blue}{\left(s \cdot x\right)} \cdot c\right) \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   8. *-commutative82.9%

      \[\leadsto {\left(\color{blue}{\left(c \cdot \left(s \cdot x\right)\right)} \cdot \left(\left(x \cdot s\right) \cdot c\right)\right)}^{-1} \]

   9. *-commutative82.9%

      \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \left(\color{blue}{\left(s \cdot x\right)} \cdot c\right)\right)}^{-1} \]

   10. *-commutative82.9%

       \[\leadsto {\left(\left(c \cdot \left(s \cdot x\right)\right) \cdot \color{blue}{\left(c \cdot \left(s \cdot x\right)\right)}\right)}^{-1} \]

   11. pow-prod-down82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{-1} \cdot {\left(c \cdot \left(s \cdot x\right)\right)}^{-1}} \]

   12. pow-sqr82.9%

       \[\leadsto \color{blue}{{\left(c \cdot \left(s \cdot x\right)\right)}^{\left(2 \cdot -1\right)}} \]

   13. metadata-eval82.9%

       \[\leadsto {\left(c \cdot \left(s \cdot x\right)\right)}^{\color{blue}{-2}} \]

   14. *-commutative82.9%

       \[\leadsto {\color{blue}{\left(\left(s \cdot x\right) \cdot c\right)}}^{-2} \]

   15. *-commutative82.9%

       \[\leadsto {\left(\color{blue}{\left(x \cdot s\right)} \cdot c\right)}^{-2} \]

   16. associate-*r*83.6%

       \[\leadsto {\color{blue}{\left(x \cdot \left(s \cdot c\right)\right)}}^{-2} \]

   17. sqr-pow83.6%

       \[\leadsto \color{blue}{{\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)} \cdot {\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}} \]

   18. pow283.6%

       \[\leadsto \color{blue}{{\left({\left(x \cdot \left(s \cdot c\right)\right)}^{\left(\frac{-2}{2}\right)}\right)}^{2}} \]

8. Applied egg-rr83.6%

   \[\leadsto \color{blue}{{\left(\frac{1}{x \cdot \left(s \cdot c\right)}\right)}^{2}} \]
9. Step-by-step derivation

   1. unpow283.6%

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(s \cdot c\right)} \cdot \frac{1}{x \cdot \left(s \cdot c\right)}} \]

   2. associate-/r*83.6%

      \[\leadsto \frac{1}{x \cdot \left(s \cdot c\right)} \cdot \color{blue}{\frac{\frac{1}{x}}{s \cdot c}} \]

   3. frac-times81.8%

      \[\leadsto \color{blue}{\frac{1 \cdot \frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

   4. *-un-lft-identity81.8%

      \[\leadsto \frac{\color{blue}{\frac{1}{x}}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)} \]

10. Applied egg-rr81.8%

    \[\leadsto \color{blue}{\frac{\frac{1}{x}}{\left(x \cdot \left(s \cdot c\right)\right) \cdot \left(s \cdot c\right)}} \]

11. Final simplification81.8%

    \[\leadsto \frac{\frac{1}{x}}{\left(s \cdot c\right) \cdot \left(x \cdot \left(s \cdot c\right)\right)} \]

herbie shell --seed 2023167 
(FPCore (x c s)
  :name "mixedcos"
  :precision binary64
  (/ (cos (* 2.0 x)) (* (pow c 2.0) (* (* x (pow s 2.0)) x))))