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.5
\[\leadsto \color{blue}{\frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{\sinh \left(\frac{1}{v}\right)} \cdot \left(\frac{cosTheta_i}{v \cdot v} \cdot cosTheta_O\right)}
\]
Proof
(*.f32 (/.f32 (/.f32 1/2 (pow.f32 (exp.f32 sinTheta_O) (/.f32 sinTheta_i v))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (/.f32 (Rewrite<= metadata-eval (/.f32 1 2)) (pow.f32 (exp.f32 sinTheta_O) (/.f32 sinTheta_i v))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (/.f32 (/.f32 1 2) (Rewrite<= exp-prod_binary32 (exp.f32 (*.f32 sinTheta_O (/.f32 sinTheta_i v))))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (/.f32 (/.f32 1 2) (exp.f32 (Rewrite<= *-commutative_binary32 (*.f32 (/.f32 sinTheta_i v) sinTheta_O)))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (/.f32 (/.f32 1 2) (exp.f32 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (Rewrite<= associate-/r*_binary32 (/.f32 1 (*.f32 2 (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))))) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (Rewrite<= associate-/l/_binary32 (/.f32 (/.f32 1 (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) 2)) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (/.f32 (Rewrite<= exp-neg_binary32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) 2) (sinh.f32 (/.f32 1 v))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (Rewrite=> associate-/l/_binary32 (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (sinh.f32 (/.f32 1 v)) 2))) (*.f32 (/.f32 cosTheta_i (*.f32 v v)) cosTheta_O)): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (sinh.f32 (/.f32 1 v)) 2)) (Rewrite<= associate-/r/_binary32 (/.f32 cosTheta_i (/.f32 (*.f32 v v) cosTheta_O)))): 17 points increase in error, 25 points decrease in error
(*.f32 (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (sinh.f32 (/.f32 1 v)) 2)) (Rewrite<= associate-/l*_binary32 (/.f32 (*.f32 cosTheta_i cosTheta_O) (*.f32 v v)))): 26 points increase in error, 17 points decrease in error
(*.f32 (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (sinh.f32 (/.f32 1 v)) 2)) (Rewrite<= associate-/l/_binary32 (/.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) v))): 19 points increase in error, 21 points decrease in error
(Rewrite<= times-frac_binary32 (/.f32 (*.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (*.f32 (*.f32 (sinh.f32 (/.f32 1 v)) 2) v))): 31 points increase in error, 33 points decrease in error
Applied egg-rr0.5
\[\leadsto \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{\sinh \left(\frac{1}{v}\right)} \cdot \left(\color{blue}{\left(\left(-cosTheta_i\right) \cdot \frac{1}{v \cdot \left(-v\right)}\right)} \cdot cosTheta_O\right)
\]
Taylor expanded in v around 0 0.5
\[\leadsto \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{\sinh \left(\frac{1}{v}\right)} \cdot \left(\left(\left(-cosTheta_i\right) \cdot \color{blue}{\frac{-1}{{v}^{2}}}\right) \cdot cosTheta_O\right)
\]
Simplified0.4
\[\leadsto \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{\sinh \left(\frac{1}{v}\right)} \cdot \left(\left(\left(-cosTheta_i\right) \cdot \color{blue}{\frac{\frac{-1}{v}}{v}}\right) \cdot cosTheta_O\right)
\]
Proof
(/.f32 (/.f32 -1 v) v): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary32 (/.f32 -1 (*.f32 v v))): 48 points increase in error, 49 points decrease in error
(/.f32 -1 (Rewrite<= unpow2_binary32 (pow.f32 v 2))): 0 points increase in error, 0 points decrease in error
Final simplification0.4
\[\leadsto \frac{\frac{0.5}{{\left(e^{sinTheta_O}\right)}^{\left(\frac{sinTheta_i}{v}\right)}}}{\sinh \left(\frac{1}{v}\right)} \cdot \left(\left(cosTheta_i \cdot \frac{\frac{1}{v}}{v}\right) \cdot cosTheta_O\right)
\]