Simplified0.4
\[\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, 1 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)): 1 points increase in error, 1 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)))): 20 points increase in error, 10 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)))): 16 points increase in error, 22 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))): 18 points increase in error, 18 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))): 33 points increase in error, 20 points decrease in error