Initial program 0.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}
\]
Simplified0.4
\[\leadsto \color{blue}{cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{v \cdot \left(\left(\sinh \left(\frac{1}{v}\right) \cdot 2\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}\right)}}
\]
Applied add-exp-log_binary320.4
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{v \cdot \left(\left(\sinh \left(\frac{1}{v}\right) \cdot \color{blue}{e^{\log 2}}\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}\right)}
\]
Applied add-exp-log_binary320.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{v \cdot \left(\left(\color{blue}{e^{\log \sinh \left(\frac{1}{v}\right)}} \cdot e^{\log 2}\right) \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}\right)}
\]
Applied prod-exp_binary320.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{v \cdot \left(\color{blue}{e^{\log \sinh \left(\frac{1}{v}\right) + \log 2}} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}\right)}
\]
Applied prod-exp_binary320.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{v \cdot \color{blue}{e^{\left(\log \sinh \left(\frac{1}{v}\right) + \log 2\right) + \frac{sinTheta_i \cdot sinTheta_O}{v}}}}
\]
Applied add-exp-log_binary320.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{\color{blue}{e^{\log v}} \cdot e^{\left(\log \sinh \left(\frac{1}{v}\right) + \log 2\right) + \frac{sinTheta_i \cdot sinTheta_O}{v}}}
\]
Applied prod-exp_binary320.6
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{\color{blue}{e^{\log v + \left(\left(\log \sinh \left(\frac{1}{v}\right) + \log 2\right) + \frac{sinTheta_i \cdot sinTheta_O}{v}\right)}}}
\]
Simplified0.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{e^{\color{blue}{\log \left(v \cdot \left(2 \cdot \sinh \left(\frac{1}{v}\right)\right)\right) + \frac{sinTheta_i \cdot sinTheta_O}{v}}}}
\]
Applied exp-sum_binary320.5
\[\leadsto cosTheta_O \cdot \frac{\frac{cosTheta_i}{v}}{\color{blue}{e^{\log \left(v \cdot \left(2 \cdot \sinh \left(\frac{1}{v}\right)\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}
\]
Applied div-inv_binary320.4
\[\leadsto cosTheta_O \cdot \frac{\color{blue}{cosTheta_i \cdot \frac{1}{v}}}{e^{\log \left(v \cdot \left(2 \cdot \sinh \left(\frac{1}{v}\right)\right)\right)} \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}
\]
Applied times-frac_binary320.4
\[\leadsto cosTheta_O \cdot \color{blue}{\left(\frac{cosTheta_i}{e^{\log \left(v \cdot \left(2 \cdot \sinh \left(\frac{1}{v}\right)\right)\right)}} \cdot \frac{\frac{1}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)}
\]
Simplified0.4
\[\leadsto cosTheta_O \cdot \left(\color{blue}{\frac{cosTheta_i}{2 \cdot \left(v \cdot \sinh \left(\frac{1}{v}\right)\right)}} \cdot \frac{\frac{1}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Taylor expanded in cosTheta_i around inf 0.4
\[\leadsto cosTheta_O \cdot \left(\color{blue}{\left(0.5 \cdot \frac{cosTheta_i}{0.5 \cdot \left(v \cdot e^{\frac{1}{v}}\right) - 0.5 \cdot \frac{v}{e^{\frac{1}{v}}}}\right)} \cdot \frac{\frac{1}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Simplified0.4
\[\leadsto cosTheta_O \cdot \left(\color{blue}{\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right)} \cdot \frac{\frac{1}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Applied *-un-lft-identity_binary320.4
\[\leadsto cosTheta_O \cdot \left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \frac{\frac{1}{v}}{\color{blue}{1 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}}\right)
\]
Applied *-un-lft-identity_binary320.4
\[\leadsto cosTheta_O \cdot \left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \frac{\frac{1}{\color{blue}{1 \cdot v}}}{1 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Applied add-cube-cbrt_binary320.4
\[\leadsto cosTheta_O \cdot \left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \frac{\frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{1 \cdot v}}{1 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Applied times-frac_binary320.4
\[\leadsto cosTheta_O \cdot \left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \frac{\color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{1} \cdot \frac{\sqrt[3]{1}}{v}}}{1 \cdot e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Applied times-frac_binary320.4
\[\leadsto cosTheta_O \cdot \left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \color{blue}{\left(\frac{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{1}}{1} \cdot \frac{\frac{\sqrt[3]{1}}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)}\right)
\]
Applied associate-*r*_binary320.4
\[\leadsto cosTheta_O \cdot \color{blue}{\left(\left(\left(1 \cdot \frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}\right) \cdot \frac{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{1}}{1}\right) \cdot \frac{\frac{\sqrt[3]{1}}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)}
\]
Simplified0.4
\[\leadsto cosTheta_O \cdot \left(\color{blue}{\frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}}} \cdot \frac{\frac{\sqrt[3]{1}}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]
Final simplification0.4
\[\leadsto cosTheta_O \cdot \left(\frac{cosTheta_i}{v \cdot e^{\frac{1}{v}} - \frac{v}{e^{\frac{1}{v}}}} \cdot \frac{\frac{1}{v}}{e^{\frac{sinTheta_i \cdot sinTheta_O}{v}}}\right)
\]