Simplified0.1
\[\leadsto \color{blue}{e^{\mathsf{fma}\left(cosTheta_i, \frac{cosTheta_O}{v}, 0.6931\right) - \mathsf{fma}\left(sinTheta_i, \frac{sinTheta_O}{v}, \frac{1}{v}\right)} \cdot \frac{0.5}{v}}
\]
Proof
(*.f32 (exp.f32 (-.f32 (fma.f32 cosTheta_i (/.f32 cosTheta_O v) 6931/10000) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (Rewrite<= fma-def_binary32 (+.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) 6931/10000)) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 (/.f32 cosTheta_O v) cosTheta_i)) 6931/10000) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 cosTheta_O cosTheta_i) v)) 6931/10000) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 (/.f32 (Rewrite<= *-commutative_binary32 (*.f32 cosTheta_i cosTheta_O)) v) 6931/10000) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (Rewrite<= +-commutative_binary32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v))) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (fma.f32 sinTheta_i (/.f32 sinTheta_O v) (Rewrite<= remove-double-neg_binary32 (neg.f32 (neg.f32 (/.f32 1 v))))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (Rewrite<= fma-neg_binary32 (-.f32 (*.f32 sinTheta_i (/.f32 sinTheta_O v)) (neg.f32 (/.f32 1 v)))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (-.f32 (Rewrite=> associate-*r/_binary32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (neg.f32 (/.f32 1 v))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (Rewrite<= associate-+r-_binary32 (+.f32 6931/10000 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (-.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (neg.f32 (/.f32 1 v))))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 6931/10000 (Rewrite<= associate-+l-_binary32 (+.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (neg.f32 (/.f32 1 v)))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 6931/10000 (Rewrite<= sub-neg_binary32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 6931/10000 (Rewrite=> associate--l-_binary32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (Rewrite=> associate-+r-_binary32 (-.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (Rewrite<= +-rgt-identity_binary32 (+.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) 0)) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (Rewrite<= metadata-eval (log.f32 1))) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (+.f32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (Rewrite=> metadata-eval 0)) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (-.f32 (Rewrite=> +-rgt-identity_binary32 (+.f32 6931/10000 (/.f32 (*.f32 cosTheta_i cosTheta_O) v))) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (Rewrite<= associate-+r-_binary32 (+.f32 6931/10000 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (+.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 1 v)))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 6931/10000 (Rewrite<= associate--l-_binary32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (Rewrite<= +-commutative_binary32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (/.f32 (Rewrite<= metadata-eval (/.f32 1 2)) v)): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (Rewrite<= associate-/r*_binary32 (/.f32 1 (*.f32 2 v)))): 0 points increase in error, 0 points decrease in error
(*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (Rewrite<= rem-exp-log_binary32 (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v)))))): 5 points increase in error, 3 points decrease in error
(Rewrite<= exp-sum_binary32 (exp.f32 (+.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000) (log.f32 (/.f32 1 (*.f32 2 v)))))): 8 points increase in error, 3 points decrease in error
Simplified0.1
\[\leadsto \color{blue}{\frac{e^{0.6931 + \frac{-1}{v}}}{v} \cdot \left(0.5 + -0.5 \cdot \left(sinTheta_O \cdot \frac{sinTheta_i}{v}\right)\right)}
\]
Proof
(*.f32 (/.f32 (exp.f32 (+.f32 6931/10000 (/.f32 -1 v))) v) (+.f32 1/2 (*.f32 -1/2 (*.f32 sinTheta_O (/.f32 sinTheta_i v))))): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (+.f32 6931/10000 (/.f32 (Rewrite<= metadata-eval (neg.f32 1)) v))) v) (+.f32 1/2 (*.f32 -1/2 (*.f32 sinTheta_O (/.f32 sinTheta_i v))))): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (+.f32 6931/10000 (Rewrite<= distribute-neg-frac_binary32 (neg.f32 (/.f32 1 v))))) v) (+.f32 1/2 (*.f32 -1/2 (*.f32 sinTheta_O (/.f32 sinTheta_i v))))): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (Rewrite<= sub-neg_binary32 (-.f32 6931/10000 (/.f32 1 v)))) v) (+.f32 1/2 (*.f32 -1/2 (*.f32 sinTheta_O (/.f32 sinTheta_i v))))): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v) (+.f32 1/2 (*.f32 -1/2 (Rewrite<= *-commutative_binary32 (*.f32 (/.f32 sinTheta_i v) sinTheta_O))))): 0 points increase in error, 0 points decrease in error
(*.f32 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v) (+.f32 1/2 (*.f32 -1/2 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (*.f32 (*.f32 -1/2 (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (Rewrite<= associate-*r*_binary32 (*.f32 -1/2 (*.f32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v))))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (*.f32 -1/2 (Rewrite<= times-frac_binary32 (/.f32 (*.f32 (*.f32 sinTheta_i sinTheta_O) (exp.f32 (-.f32 6931/10000 (/.f32 1 v)))) (*.f32 v v))))): 109 points increase in error, 0 points decrease in error
(+.f32 (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (*.f32 -1/2 (/.f32 (Rewrite<= associate-*r*_binary32 (*.f32 sinTheta_i (*.f32 sinTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v)))))) (*.f32 v v)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (*.f32 -1/2 (/.f32 (*.f32 sinTheta_i (*.f32 sinTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v))))) (Rewrite<= unpow2_binary32 (pow.f32 v 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary32 (+.f32 (*.f32 -1/2 (/.f32 (*.f32 sinTheta_i (*.f32 sinTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v))))) (pow.f32 v 2))) (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)))): 0 points increase in error, 0 points decrease in error