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}{\left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \frac{\frac{0.5}{\sinh \left(\frac{1}{v}\right) \cdot {\left(e^{\frac{sinTheta_i}{v}}\right)}^{sinTheta_O}}}{v}}
\]
Proof
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (/.f32 (/.f32 1/2 (*.f32 (sinh.f32 (/.f32 1 v)) (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (Rewrite<= *-commutative_binary32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i)) (/.f32 (/.f32 1/2 (*.f32 (sinh.f32 (/.f32 1 v)) (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O))) v)): 0 points increase in error, 12 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 (Rewrite<= metadata-eval (/.f32 1 2)) (*.f32 (sinh.f32 (/.f32 1 v)) (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 (/.f32 1 2) (*.f32 (sinh.f32 (/.f32 1 v)) (Rewrite<= exp-prod_binary32 (exp.f32 (*.f32 (/.f32 sinTheta_i v) sinTheta_O))))) v)): 5 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 (/.f32 1 2) (*.f32 (sinh.f32 (/.f32 1 v)) (exp.f32 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))))) v)): 0 points increase in error, 5 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (Rewrite<= associate-/r*_binary32 (/.f32 1 (*.f32 2 (*.f32 (sinh.f32 (/.f32 1 v)) (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 1 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 2 (sinh.f32 (/.f32 1 v))) (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 1 (*.f32 (Rewrite<= *-commutative_binary32 (*.f32 (sinh.f32 (/.f32 1 v)) 2)) (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (Rewrite<= associate-/l/_binary32 (/.f32 (/.f32 1 (exp.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (sinh.f32 (/.f32 1 v)) 2))) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (/.f32 (/.f32 (Rewrite<= exp-neg_binary32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) (*.f32 (sinh.f32 (/.f32 1 v)) 2)) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i) (Rewrite<= associate-/r*_binary32 (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (*.f32 (sinh.f32 (/.f32 1 v)) 2) v)))): 0 points increase in error, 0 points decrease in error
(*.f32 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 cosTheta_O cosTheta_i) v)) (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (*.f32 (sinh.f32 (/.f32 1 v)) 2) v))): 15 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (Rewrite<= *-commutative_binary32 (*.f32 cosTheta_i cosTheta_O)) v) (/.f32 (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (*.f32 (*.f32 (sinh.f32 (/.f32 1 v)) 2) v))): 0 points increase in error, 15 points decrease in error
(Rewrite=> associate-*r/_binary32 (/.f32 (*.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (exp.f32 (neg.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) (*.f32 (*.f32 (sinh.f32 (/.f32 1 v)) 2) v))): 10 points increase in error, 0 points decrease in error
(/.f32 (Rewrite<= *-commutative_binary32 (*.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)): 0 points increase in error, 10 points decrease in error
Applied egg-rr0.4
\[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\left(\frac{\frac{1}{v}}{\sinh \left(\frac{1}{v}\right) \cdot \left(-{\left(e^{\frac{sinTheta_i}{v}}\right)}^{sinTheta_O}\right)} \cdot -0.5\right)}
\]
Simplified0.4
\[\leadsto \left(cosTheta_i \cdot \frac{cosTheta_O}{v}\right) \cdot \color{blue}{\frac{\frac{\frac{-0.5}{v}}{\sinh \left(\frac{1}{v}\right)}}{-{\left(e^{\frac{sinTheta_i}{v}}\right)}^{sinTheta_O}}}
\]
Proof
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (/.f32 (/.f32 (/.f32 -1/2 v) (sinh.f32 (/.f32 1 v))) (neg.f32 (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O)))): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (/.f32 (/.f32 (/.f32 (Rewrite<= metadata-eval (*.f32 1 -1/2)) v) (sinh.f32 (/.f32 1 v))) (neg.f32 (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O)))): 0 points increase in error, 5 points decrease in error
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (/.f32 (/.f32 (Rewrite<= associate-*l/_binary32 (*.f32 (/.f32 1 v) -1/2)) (sinh.f32 (/.f32 1 v))) (neg.f32 (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O)))): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (Rewrite<= associate-/r*_binary32 (/.f32 (*.f32 (/.f32 1 v) -1/2) (*.f32 (sinh.f32 (/.f32 1 v)) (neg.f32 (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O)))))): 0 points increase in error, 0 points decrease in error
(*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (Rewrite<= associate-*l/_binary32 (*.f32 (/.f32 (/.f32 1 v) (*.f32 (sinh.f32 (/.f32 1 v)) (neg.f32 (pow.f32 (exp.f32 (/.f32 sinTheta_i v)) sinTheta_O)))) -1/2))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.4
\[\leadsto \color{blue}{\frac{cosTheta_i}{\frac{v}{cosTheta_O}}} \cdot \frac{\frac{\frac{-0.5}{v}}{\sinh \left(\frac{1}{v}\right)}}{-{\left(e^{\frac{sinTheta_i}{v}}\right)}^{sinTheta_O}}
\]
Applied egg-rr0.4
\[\leadsto \color{blue}{\frac{\frac{\frac{0.5}{v}}{\sinh \left(\frac{1}{v}\right)} \cdot cosTheta_i}{\frac{v}{cosTheta_O} \cdot e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}}}
\]
Applied egg-rr0.4
\[\leadsto \frac{\color{blue}{\frac{\frac{0.5}{v} \cdot cosTheta_i}{\sinh \left(\frac{1}{v}\right)}}}{\frac{v}{cosTheta_O} \cdot e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}}
\]
Final simplification0.4
\[\leadsto \frac{\frac{\frac{0.5}{v} \cdot cosTheta_i}{\sinh \left(\frac{1}{v}\right)}}{\frac{v}{cosTheta_O} \cdot e^{\frac{sinTheta_i}{v} \cdot sinTheta_O}}
\]