HairBSDF, Mp, upper

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

3. Applied egg-rr98.5%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
4. Step-by-step derivation

   1. div-inv98.7%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(\color{blue}{\left(cosTheta_O \cdot \frac{1}{v}\right)} \cdot cosTheta_i\right)}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

5. Applied egg-rr98.7%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(\color{blue}{\left(cosTheta_O \cdot \frac{1}{v}\right)} \cdot cosTheta_i\right)}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

6. Final simplification98.7%

   \[\leadsto \frac{e^{\frac{sinTheta_i \cdot \left(-sinTheta_O\right)}{v}} \cdot \left(\left(cosTheta_O \cdot \frac{1}{v}\right) \cdot cosTheta_i\right)}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

3. Applied egg-rr98.5%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
4. Step-by-step derivation

   1. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\sinh \left(\frac{1}{v}\right) \cdot 2} \cdot \frac{\frac{cosTheta_O}{v} \cdot cosTheta_i}{v}} \]

   2. associate-/l*98.5%

      \[\leadsto \frac{e^{-\color{blue}{\frac{sinTheta_i}{\frac{v}{sinTheta_O}}}}}{\sinh \left(\frac{1}{v}\right) \cdot 2} \cdot \frac{\frac{cosTheta_O}{v} \cdot cosTheta_i}{v} \]

   3. associate-*l/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i}{\frac{v}{sinTheta_O}}}}{\sinh \left(\frac{1}{v}\right) \cdot 2} \cdot \frac{\color{blue}{\frac{cosTheta_O \cdot cosTheta_i}{v}}}{v} \]

5. Applied egg-rr98.5%

   \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i}{\frac{v}{sinTheta_O}}}}{\sinh \left(\frac{1}{v}\right) \cdot 2} \cdot \frac{\frac{cosTheta_O \cdot cosTheta_i}{v}}{v}} \]

6. Final simplification98.5%

   \[\leadsto \frac{e^{\frac{-sinTheta_i}{\frac{v}{sinTheta_O}}}}{\sinh \left(\frac{1}{v}\right) \cdot 2} \cdot \frac{\frac{cosTheta_O \cdot cosTheta_i}{v}}{v} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

3. Applied egg-rr98.5%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

4. Final simplification98.5%

   \[\leadsto \frac{e^{\frac{sinTheta_i \cdot \left(-sinTheta_O\right)}{v}} \cdot \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. *-commutative98.5%

      \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. associate-*r/98.6%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

   3. associate-/l*98.6%

      \[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   4. associate-/r/98.5%

      \[\leadsto \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   5. *-commutative98.5%

      \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   6. *-commutative98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

   7. associate-*r*98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

   8. associate-/l/98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   9. exp-neg98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   10. associate-/l/98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   11. associate-/r*98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   12. metadata-eval98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   13. associate-*l/98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   14. *-commutative98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   15. exp-prod98.5%

       \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

4. Taylor expanded in sinTheta_O around 0 98.3%

   \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
5. Step-by-step derivation

   1. rec-exp98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

   2. distribute-neg-frac98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

   3. metadata-eval98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

6. Simplified98.3%

   \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]
7. Step-by-step derivation

   1. *-un-lft-identity98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(1 \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}\right)} \]

8. Applied egg-rr98.3%

   \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(1 \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}\right)} \]
9. Step-by-step derivation

   1. *-lft-identity98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   2. associate-/r*98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}}} \]

10. Simplified98.5%

    \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}}} \]

11. Final simplification98.5%

    \[\leadsto \frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}} \cdot \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. *-commutative98.5%

      \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. associate-*r/98.6%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

   3. *-commutative98.6%

      \[\leadsto \frac{\color{blue}{cosTheta_O \cdot cosTheta_i}}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   5. *-commutative98.5%

      \[\leadsto \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   6. *-commutative98.5%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

   7. associate-*r*98.5%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

   8. associate-/l/98.5%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   9. exp-neg98.5%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   10. associate-/l/98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   11. associate-/r*98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   12. metadata-eval98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   13. associate-*l/98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   14. *-commutative98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   15. exp-prod98.5%

       \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

4. Taylor expanded in sinTheta_O around 0 98.3%

   \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
5. Step-by-step derivation

   1. rec-exp98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

   2. distribute-neg-frac98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

   3. metadata-eval98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

6. Simplified98.3%

   \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]
7. Step-by-step derivation

   1. *-un-lft-identity98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(1 \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}\right)} \]

8. Applied egg-rr98.3%

   \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\left(1 \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}\right)} \]
9. Step-by-step derivation

   1. *-lft-identity98.3%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   2. associate-/r*98.5%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}}} \]

10. Simplified98.5%

    \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}}} \]

11. Final simplification98.5%

    \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{1}{v}}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

3. Applied egg-rr98.5%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

4. Taylor expanded in sinTheta_i around 0 98.3%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{{v}^{2} \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
5. Step-by-step derivation

   1. *-commutative98.3%

      \[\leadsto \frac{\color{blue}{cosTheta_O \cdot cosTheta_i}}{{v}^{2} \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)} \]

   2. times-frac98.3%

      \[\leadsto \color{blue}{\frac{cosTheta_O}{{v}^{2}} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}}} \]

   3. unpow298.3%

      \[\leadsto \frac{cosTheta_O}{\color{blue}{v \cdot v}} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}} \]

   4. rec-exp98.4%

      \[\leadsto \frac{cosTheta_O}{v \cdot v} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}} \]

   5. distribute-neg-frac98.4%

      \[\leadsto \frac{cosTheta_O}{v \cdot v} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}} \]

   6. metadata-eval98.4%

      \[\leadsto \frac{cosTheta_O}{v \cdot v} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}} \]

6. Simplified98.4%

   \[\leadsto \color{blue}{\frac{cosTheta_O}{v \cdot v} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}}} \]

7. Final simplification98.4%

   \[\leadsto \frac{cosTheta_O}{v \cdot v} \cdot \frac{cosTheta_i}{e^{\frac{1}{v}} - e^{\frac{-1}{v}}} \]

1. Split input into 2 regimes

2. if v < 0.50999999

   1. Initial program 98.2%

      \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
   2. Step-by-step derivation

      1. *-commutative98.2%

         \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      2. associate-*r/98.3%

         \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

      3. associate-/l*98.3%

         \[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      4. associate-/r/98.3%

         \[\leadsto \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      5. *-commutative98.3%

         \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      6. *-commutative98.3%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

      7. associate-*r*98.3%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

      8. associate-/l/98.3%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

      9. exp-neg98.3%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      10. associate-/l/98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      11. associate-/r*98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      12. metadata-eval98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      13. associate-*l/98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      14. *-commutative98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      15. exp-prod98.3%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   3. Simplified98.3%

      \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   4. Taylor expanded in sinTheta_O around 0 97.9%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
   5. Step-by-step derivation

      1. rec-exp97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

      2. distribute-neg-frac97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

      3. metadata-eval97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

   6. Simplified97.9%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   7. Taylor expanded in v around inf 69.4%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{\left(1 - \frac{1}{v}\right)}\right)} \]

   if 0.50999999 < v

   1. Initial program 99.1%

      \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
   2. Step-by-step derivation

      1. *-commutative99.1%

         \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      2. associate-*r/99.1%

         \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

      3. associate-/l*99.1%

         \[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      4. associate-/r/99.0%

         \[\leadsto \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      5. *-commutative99.0%

         \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      6. *-commutative99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

      7. associate-*r*99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

      8. associate-/l/99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

      9. exp-neg99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      10. associate-/l/99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      11. associate-/r*99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      12. metadata-eval99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      13. associate-*l/99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      14. *-commutative99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      15. exp-prod99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   3. Simplified99.0%

      \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   4. Taylor expanded in sinTheta_O around 0 98.8%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
   5. Step-by-step derivation

      1. rec-exp98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

      2. distribute-neg-frac98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

      3. metadata-eval98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

   6. Simplified98.9%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   7. Taylor expanded in v around inf 75.1%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(\left(0.5 + 0.009722222222222222 \cdot \frac{1}{{v}^{4}}\right) - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]
   8. Step-by-step derivation

      1. associate--l+75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(0.5 + \left(0.009722222222222222 \cdot \frac{1}{{v}^{4}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right)} \]

      2. associate-*r/75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\color{blue}{\frac{0.009722222222222222 \cdot 1}{{v}^{4}}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right) \]

      3. metadata-eval75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{\color{blue}{0.009722222222222222}}{{v}^{4}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right) \]

      4. associate-*r/75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \color{blue}{\frac{0.08333333333333333 \cdot 1}{{v}^{2}}}\right)\right) \]

      5. metadata-eval75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{\color{blue}{0.08333333333333333}}{{v}^{2}}\right)\right) \]

      6. unpow275.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{\color{blue}{v \cdot v}}\right)\right) \]

   9. Simplified75.1%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{v \cdot v}\right)\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification71.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;v \leq 0.5099999904632568:\\ \;\;\;\;\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} + \left(\frac{1}{v} + -1\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{v \cdot v}\right)\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if v < 0.50999999

   1. Initial program 98.2%

      \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
   2. Step-by-step derivation

      1. *-commutative98.2%

         \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      2. associate-*r/98.3%

         \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

      3. *-commutative98.3%

         \[\leadsto \frac{\color{blue}{cosTheta_O \cdot cosTheta_i}}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      4. associate-*l/98.2%

         \[\leadsto \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      5. *-commutative98.2%

         \[\leadsto \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      6. *-commutative98.2%

         \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

      7. associate-*r*98.2%

         \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

      8. associate-/l/98.2%

         \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

      9. exp-neg98.2%

         \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      10. associate-/l/98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      11. associate-/r*98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      12. metadata-eval98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      13. associate-*l/98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      14. *-commutative98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      15. exp-prod98.2%

          \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   3. Simplified98.2%

      \[\leadsto \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   4. Taylor expanded in sinTheta_O around 0 97.8%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
   5. Step-by-step derivation

      1. rec-exp97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

      2. distribute-neg-frac97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

      3. metadata-eval97.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

   6. Simplified97.8%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   7. Taylor expanded in v around inf 69.4%

      \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{\left(1 - \frac{1}{v}\right)}\right)} \]

   if 0.50999999 < v

   1. Initial program 99.1%

      \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
   2. Step-by-step derivation

      1. *-commutative99.1%

         \[\leadsto \frac{\color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      2. associate-*r/99.1%

         \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v}} \]

      3. associate-/l*99.1%

         \[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      4. associate-/r/99.0%

         \[\leadsto \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      5. *-commutative99.0%

         \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right)} \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

      6. *-commutative99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{v \cdot \left(\sinh \left(\frac{1}{v}\right) \cdot 2\right)}} \]

      7. associate-*r*99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\color{blue}{\left(v \cdot \sinh \left(\frac{1}{v}\right)\right) \cdot 2}} \]

      8. associate-/l/99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

      9. exp-neg99.0%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{2}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      10. associate-/l/99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{1}{2 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      11. associate-/r*99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\color{blue}{\frac{\frac{1}{2}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      12. metadata-eval99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{\color{blue}{0.5}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      13. associate-*l/99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      14. *-commutative99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{e^{\color{blue}{sinTheta_O \cdot \frac{sinTheta_i}{v}}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

      15. exp-prod99.0%

          \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{\color{blue}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}}{v \cdot \sinh \left(\frac{1}{v}\right)} \]

   3. Simplified99.0%

      \[\leadsto \color{blue}{\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{v \cdot \sinh \left(\frac{1}{v}\right)}} \]

   4. Taylor expanded in sinTheta_O around 0 98.8%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - \frac{1}{e^{\frac{1}{v}}}\right)}} \]
   5. Step-by-step derivation

      1. rec-exp98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - \color{blue}{e^{-\frac{1}{v}}}\right)} \]

      2. distribute-neg-frac98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\color{blue}{\frac{-1}{v}}}\right)} \]

      3. metadata-eval98.9%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{\color{blue}{-1}}{v}}\right)} \]

   6. Simplified98.9%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\frac{1}{v \cdot \left(e^{\frac{1}{v}} - e^{\frac{-1}{v}}\right)}} \]

   7. Taylor expanded in v around inf 75.1%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(\left(0.5 + 0.009722222222222222 \cdot \frac{1}{{v}^{4}}\right) - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]
   8. Step-by-step derivation

      1. associate--l+75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(0.5 + \left(0.009722222222222222 \cdot \frac{1}{{v}^{4}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right)} \]

      2. associate-*r/75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\color{blue}{\frac{0.009722222222222222 \cdot 1}{{v}^{4}}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right) \]

      3. metadata-eval75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{\color{blue}{0.009722222222222222}}{{v}^{4}} - 0.08333333333333333 \cdot \frac{1}{{v}^{2}}\right)\right) \]

      4. associate-*r/75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \color{blue}{\frac{0.08333333333333333 \cdot 1}{{v}^{2}}}\right)\right) \]

      5. metadata-eval75.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{\color{blue}{0.08333333333333333}}{{v}^{2}}\right)\right) \]

      6. unpow275.1%

         \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{\color{blue}{v \cdot v}}\right)\right) \]

   9. Simplified75.1%

      \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \color{blue}{\left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{v \cdot v}\right)\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification71.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;v \leq 0.5099999904632568:\\ \;\;\;\;\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{1}{v \cdot \left(e^{\frac{1}{v}} + \left(\frac{1}{v} + -1\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot \left(0.5 + \left(\frac{0.009722222222222222}{{v}^{4}} - \frac{0.08333333333333333}{v \cdot v}\right)\right)\\ \end{array} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*l/98.6%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]

   2. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v}} \]

   3. exp-neg98.5%

      \[\leadsto \frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \frac{\color{blue}{\frac{1 \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   5. *-lft-identity98.5%

      \[\leadsto \frac{\frac{\color{blue}{cosTheta_i \cdot cosTheta_O}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   6. associate-/l/98.5%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \]

   7. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(2 \cdot v\right)\right)} \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   8. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(2 \cdot v\right) \cdot v\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   9. *-commutative98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\color{blue}{\left(v \cdot 2\right)} \cdot v\right)\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   10. *-commutative98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{\color{blue}{sinTheta_O \cdot sinTheta_i}}{v}}} \]

   11. associate-*l/98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\color{blue}{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

4. Taylor expanded in v around inf 63.9%

   \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v\right)} \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}} \]

5. Taylor expanded in cosTheta_i around 0 63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v\right)}} \]
6. Step-by-step derivation

   1. times-frac63.9%

      \[\leadsto \color{blue}{\frac{cosTheta_i}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \cdot \frac{cosTheta_O}{0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v}} \]

   2. associate-/l*63.9%

      \[\leadsto \frac{cosTheta_i}{e^{\color{blue}{\frac{sinTheta_i}{\frac{v}{sinTheta_O}}}}} \cdot \frac{cosTheta_O}{0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v} \]

   3. associate-/r/63.9%

      \[\leadsto \frac{cosTheta_i}{e^{\color{blue}{\frac{sinTheta_i}{v} \cdot sinTheta_O}}} \cdot \frac{cosTheta_O}{0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v} \]

   4. associate-*r/63.9%

      \[\leadsto \frac{cosTheta_i}{e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}} \cdot \frac{cosTheta_O}{\color{blue}{\frac{0.3333333333333333 \cdot 1}{v}} + 2 \cdot v} \]

   5. metadata-eval63.9%

      \[\leadsto \frac{cosTheta_i}{e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}} \cdot \frac{cosTheta_O}{\frac{\color{blue}{0.3333333333333333}}{v} + 2 \cdot v} \]

   6. *-commutative63.9%

      \[\leadsto \frac{cosTheta_i}{e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}} \cdot \frac{cosTheta_O}{\frac{0.3333333333333333}{v} + \color{blue}{v \cdot 2}} \]

7. Simplified63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i}{e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}} \cdot \frac{cosTheta_O}{\frac{0.3333333333333333}{v} + v \cdot 2}} \]

8. Final simplification63.9%

   \[\leadsto \frac{cosTheta_i}{e^{sinTheta_O \cdot \frac{sinTheta_i}{v}}} \cdot \frac{cosTheta_O}{\frac{0.3333333333333333}{v} + v \cdot 2} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*l/98.6%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]

   2. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v}} \]

   3. exp-neg98.5%

      \[\leadsto \frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \frac{\color{blue}{\frac{1 \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   5. *-lft-identity98.5%

      \[\leadsto \frac{\frac{\color{blue}{cosTheta_i \cdot cosTheta_O}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   6. associate-/l/98.5%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \]

   7. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(2 \cdot v\right)\right)} \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   8. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(2 \cdot v\right) \cdot v\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   9. *-commutative98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\color{blue}{\left(v \cdot 2\right)} \cdot v\right)\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   10. *-commutative98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{\color{blue}{sinTheta_O \cdot sinTheta_i}}{v}}} \]

   11. associate-*l/98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\color{blue}{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

4. Taylor expanded in v around inf 63.9%

   \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v\right)} \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}} \]

5. Taylor expanded in sinTheta_O around 0 63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v}} \]
6. Step-by-step derivation

   1. associate-*r/63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\frac{0.3333333333333333 \cdot 1}{v}} + 2 \cdot v} \]

   2. metadata-eval63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\frac{\color{blue}{0.3333333333333333}}{v} + 2 \cdot v} \]

   3. *-commutative63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\frac{0.3333333333333333}{v} + \color{blue}{v \cdot 2}} \]

   4. associate-*l/63.9%

      \[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{0.3333333333333333}{v} + v \cdot 2} \cdot cosTheta_O} \]

   5. +-commutative63.9%

      \[\leadsto \frac{cosTheta_i}{\color{blue}{v \cdot 2 + \frac{0.3333333333333333}{v}}} \cdot cosTheta_O \]

   6. fma-def63.9%

      \[\leadsto \frac{cosTheta_i}{\color{blue}{\mathsf{fma}\left(v, 2, \frac{0.3333333333333333}{v}\right)}} \cdot cosTheta_O \]

7. Simplified63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i}{\mathsf{fma}\left(v, 2, \frac{0.3333333333333333}{v}\right)} \cdot cosTheta_O} \]

8. Final simplification63.9%

   \[\leadsto cosTheta_O \cdot \frac{cosTheta_i}{\mathsf{fma}\left(v, 2, \frac{0.3333333333333333}{v}\right)} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

2. Taylor expanded in v around inf 63.9%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\color{blue}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} \]
3. Step-by-step derivation

   1. associate-*r/63.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \color{blue}{\frac{0.3333333333333333 \cdot 1}{{v}^{2}}}} \]

   2. metadata-eval63.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \frac{\color{blue}{0.3333333333333333}}{{v}^{2}}} \]

   3. unpow263.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \frac{0.3333333333333333}{\color{blue}{v \cdot v}}} \]

4. Simplified63.9%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\color{blue}{2 + \frac{0.3333333333333333}{v \cdot v}}} \]

5. Taylor expanded in sinTheta_i around 0 63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)}} \]
6. Step-by-step derivation

   1. times-frac63.9%

      \[\leadsto \color{blue}{\frac{cosTheta_i}{v} \cdot \frac{cosTheta_O}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]

   2. associate-*r/63.9%

      \[\leadsto \color{blue}{\frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]

   3. associate-*r/63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \color{blue}{\frac{0.3333333333333333 \cdot 1}{{v}^{2}}}} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]

   4. metadata-eval63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{\color{blue}{0.3333333333333333}}{{v}^{2}}} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]

   5. unpow263.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{\color{blue}{v \cdot v}}} + -1 \cdot \frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)} \]

   6. mul-1-neg63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \color{blue}{\left(-\frac{sinTheta_i \cdot \left(cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)\right)}{{v}^{2} \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)}\right)} \]

   7. times-frac63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\color{blue}{\frac{sinTheta_i}{{v}^{2}} \cdot \frac{cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}}\right) \]

   8. unpow263.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{\color{blue}{v \cdot v}} \cdot \frac{cosTheta_i \cdot \left(sinTheta_O \cdot cosTheta_O\right)}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}\right) \]

   9. associate-*r*63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{v \cdot v} \cdot \frac{\color{blue}{\left(cosTheta_i \cdot sinTheta_O\right) \cdot cosTheta_O}}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}\right) \]

   10. associate-*r/63.9%

       \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{v \cdot v} \cdot \frac{\left(cosTheta_i \cdot sinTheta_O\right) \cdot cosTheta_O}{2 + \color{blue}{\frac{0.3333333333333333 \cdot 1}{{v}^{2}}}}\right) \]

   11. metadata-eval63.9%

       \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{v \cdot v} \cdot \frac{\left(cosTheta_i \cdot sinTheta_O\right) \cdot cosTheta_O}{2 + \frac{\color{blue}{0.3333333333333333}}{{v}^{2}}}\right) \]

   12. unpow263.9%

       \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{v \cdot v} \cdot \frac{\left(cosTheta_i \cdot sinTheta_O\right) \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{\color{blue}{v \cdot v}}}\right) \]

7. Simplified63.9%

   \[\leadsto \color{blue}{\frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}} + \left(-\frac{sinTheta_i}{v \cdot v} \cdot \frac{\left(cosTheta_i \cdot sinTheta_O\right) \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}}\right)} \]

8. Final simplification63.9%

   \[\leadsto \frac{cosTheta_O \cdot \frac{cosTheta_i}{v}}{2 + \frac{0.3333333333333333}{v \cdot v}} - \frac{sinTheta_i}{v \cdot v} \cdot \frac{cosTheta_O \cdot \left(sinTheta_O \cdot cosTheta_i\right)}{2 + \frac{0.3333333333333333}{v \cdot v}} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

2. Taylor expanded in v around inf 63.9%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\color{blue}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} \]
3. Step-by-step derivation

   1. associate-*r/63.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \color{blue}{\frac{0.3333333333333333 \cdot 1}{{v}^{2}}}} \]

   2. metadata-eval63.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \frac{\color{blue}{0.3333333333333333}}{{v}^{2}}} \]

   3. unpow263.9%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{2 + \frac{0.3333333333333333}{\color{blue}{v \cdot v}}} \]

4. Simplified63.9%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\color{blue}{2 + \frac{0.3333333333333333}{v \cdot v}}} \]

5. Taylor expanded in sinTheta_i around 0 63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{v \cdot \left(2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}\right)}} \]
6. Step-by-step derivation

   1. times-frac63.9%

      \[\leadsto \color{blue}{\frac{cosTheta_i}{v} \cdot \frac{cosTheta_O}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} \]

   2. associate-*r/63.9%

      \[\leadsto \color{blue}{\frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + 0.3333333333333333 \cdot \frac{1}{{v}^{2}}}} \]

   3. associate-*r/63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \color{blue}{\frac{0.3333333333333333 \cdot 1}{{v}^{2}}}} \]

   4. metadata-eval63.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{\color{blue}{0.3333333333333333}}{{v}^{2}}} \]

   5. unpow263.9%

      \[\leadsto \frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{\color{blue}{v \cdot v}}} \]

7. Simplified63.9%

   \[\leadsto \color{blue}{\frac{\frac{cosTheta_i}{v} \cdot cosTheta_O}{2 + \frac{0.3333333333333333}{v \cdot v}}} \]

8. Final simplification63.9%

   \[\leadsto \frac{cosTheta_O \cdot \frac{cosTheta_i}{v}}{2 + \frac{0.3333333333333333}{v \cdot v}} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*l/98.6%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]

   2. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v}} \]

   3. exp-neg98.5%

      \[\leadsto \frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \frac{\color{blue}{\frac{1 \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   5. *-lft-identity98.5%

      \[\leadsto \frac{\frac{\color{blue}{cosTheta_i \cdot cosTheta_O}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   6. associate-/l/98.5%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \]

   7. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(2 \cdot v\right)\right)} \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   8. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(2 \cdot v\right) \cdot v\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   9. *-commutative98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\color{blue}{\left(v \cdot 2\right)} \cdot v\right)\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   10. *-commutative98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{\color{blue}{sinTheta_O \cdot sinTheta_i}}{v}}} \]

   11. associate-*l/98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\color{blue}{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

4. Taylor expanded in v around inf 63.9%

   \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v\right)} \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}} \]

5. Taylor expanded in sinTheta_O around 0 63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{0.3333333333333333 \cdot \frac{1}{v} + 2 \cdot v}} \]
6. Step-by-step derivation

   1. associate-*r/63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\frac{0.3333333333333333 \cdot 1}{v}} + 2 \cdot v} \]

   2. metadata-eval63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\frac{\color{blue}{0.3333333333333333}}{v} + 2 \cdot v} \]

   3. *-commutative63.9%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\frac{0.3333333333333333}{v} + \color{blue}{v \cdot 2}} \]

7. Simplified63.9%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\frac{0.3333333333333333}{v} + v \cdot 2}} \]

8. Final simplification63.9%

   \[\leadsto \frac{cosTheta_O \cdot cosTheta_i}{\frac{0.3333333333333333}{v} + v \cdot 2} \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*l/98.6%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]

   2. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v}} \]

   3. exp-neg98.5%

      \[\leadsto \frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \frac{\color{blue}{\frac{1 \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   5. *-lft-identity98.5%

      \[\leadsto \frac{\frac{\color{blue}{cosTheta_i \cdot cosTheta_O}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   6. associate-/l/98.5%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \]

   7. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(2 \cdot v\right)\right)} \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   8. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(2 \cdot v\right) \cdot v\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   9. *-commutative98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\color{blue}{\left(v \cdot 2\right)} \cdot v\right)\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   10. *-commutative98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{\color{blue}{sinTheta_O \cdot sinTheta_i}}{v}}} \]

   11. associate-*l/98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\color{blue}{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

4. Taylor expanded in v around inf 58.2%

   \[\leadsto \color{blue}{0.5 \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]
5. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

6. Applied egg-rr58.2%

   \[\leadsto 0.5 \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)} \]

7. Final simplification58.2%

   \[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot 0.5 \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*r/98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

   2. *-commutative98.5%

      \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

3. Applied egg-rr98.5%

   \[\leadsto \frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \color{blue}{\left(\frac{cosTheta_O}{v} \cdot cosTheta_i\right)}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]

4. Taylor expanded in v around inf 58.2%

   \[\leadsto \color{blue}{0.5 \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]
5. Step-by-step derivation

   1. associate-/l*58.2%

      \[\leadsto 0.5 \cdot \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \]

6. Simplified58.2%

   \[\leadsto \color{blue}{0.5 \cdot \frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \]
7. Step-by-step derivation

   1. associate-/r/58.2%

      \[\leadsto 0.5 \cdot \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \]

8. Applied egg-rr58.2%

   \[\leadsto 0.5 \cdot \color{blue}{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O\right)} \]

9. Final simplification58.2%

   \[\leadsto \left(cosTheta_O \cdot \frac{cosTheta_i}{v}\right) \cdot 0.5 \]

1. Initial program 98.5%

   \[\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \]
2. Step-by-step derivation

   1. associate-*l/98.6%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}}}{\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v} \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]

   2. times-frac98.5%

      \[\leadsto \color{blue}{\frac{e^{-\frac{sinTheta_i \cdot sinTheta_O}{v}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v}} \]

   3. exp-neg98.5%

      \[\leadsto \frac{\color{blue}{\frac{1}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   4. associate-*l/98.5%

      \[\leadsto \frac{\color{blue}{\frac{1 \cdot \left(cosTheta_i \cdot cosTheta_O\right)}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   5. *-lft-identity98.5%

      \[\leadsto \frac{\frac{\color{blue}{cosTheta_i \cdot cosTheta_O}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}{\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v} \]

   6. associate-/l/98.5%

      \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot v\right) \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}} \]

   7. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(2 \cdot v\right)\right)} \cdot v\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   8. associate-*l*98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\color{blue}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(2 \cdot v\right) \cdot v\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   9. *-commutative98.5%

      \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\color{blue}{\left(v \cdot 2\right)} \cdot v\right)\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}} \]

   10. *-commutative98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{\color{blue}{sinTheta_O \cdot sinTheta_i}}{v}}} \]

   11. associate-*l/98.5%

       \[\leadsto \frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\color{blue}{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

3. Simplified98.5%

   \[\leadsto \color{blue}{\frac{cosTheta_i \cdot cosTheta_O}{\left(\sinh \left(\frac{1}{v}\right) \cdot \left(\left(v \cdot 2\right) \cdot v\right)\right) \cdot e^{\frac{sinTheta_O}{v} \cdot sinTheta_i}}} \]

4. Taylor expanded in v around inf 58.2%

   \[\leadsto \color{blue}{0.5 \cdot \frac{cosTheta_i \cdot cosTheta_O}{v}} \]
5. Step-by-step derivation

   1. clear-num58.8%

      \[\leadsto 0.5 \cdot \color{blue}{\frac{1}{\frac{v}{cosTheta_i \cdot cosTheta_O}}} \]

   2. un-div-inv58.8%

      \[\leadsto \color{blue}{\frac{0.5}{\frac{v}{cosTheta_i \cdot cosTheta_O}}} \]

6. Applied egg-rr58.8%

   \[\leadsto \color{blue}{\frac{0.5}{\frac{v}{cosTheta_i \cdot cosTheta_O}}} \]

7. Final simplification58.8%

   \[\leadsto \frac{0.5}{\frac{v}{cosTheta_O \cdot cosTheta_i}} \]

herbie shell --seed 2023167 
(FPCore (cosTheta_i cosTheta_O sinTheta_i sinTheta_O v)
  :name "HairBSDF, Mp, upper"
  :precision binary32
  :pre (and (and (and (and (and (and (<= -1.0 cosTheta_i) (<= cosTheta_i 1.0)) (and (<= -1.0 cosTheta_O) (<= cosTheta_O 1.0))) (and (<= -1.0 sinTheta_i) (<= sinTheta_i 1.0))) (and (<= -1.0 sinTheta_O) (<= sinTheta_O 1.0))) (< 0.1 v)) (<= v 1.5707964))
  (/ (* (exp (- (/ (* sinTheta_i sinTheta_O) v))) (/ (* cosTheta_i cosTheta_O) v)) (* (* (sinh (/ 1.0 v)) 2.0) v)))