Initial program 0.9
\[\left(\sin \left(\left(1 - u\right) \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}\right) \cdot n0_i + \left(\sin \left(u \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}\right) \cdot n1_i
\]
Simplified0.7
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\sin \left(\left(1 - u\right) \cdot normAngle\right)}{\sin normAngle}, n0_i, \frac{\sin \left(u \cdot normAngle\right)}{\sin normAngle} \cdot n1_i\right)}
\]
Proof
(fma.f32 (/.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) (sin.f32 normAngle)) n0_i (*.f32 (/.f32 (sin.f32 (*.f32 u normAngle)) (sin.f32 normAngle)) n1_i)): 0 points increase in error, 0 points decrease in error
(fma.f32 (/.f32 (Rewrite<= *-rgt-identity_binary32 (*.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) 1)) (sin.f32 normAngle)) n0_i (*.f32 (/.f32 (sin.f32 (*.f32 u normAngle)) (sin.f32 normAngle)) n1_i)): 0 points increase in error, 0 points decrease in error
(fma.f32 (Rewrite<= associate-*r/_binary32 (*.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) (/.f32 1 (sin.f32 normAngle)))) n0_i (*.f32 (/.f32 (sin.f32 (*.f32 u normAngle)) (sin.f32 normAngle)) n1_i)): 26 points increase in error, 7 points decrease in error
(fma.f32 (*.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) (/.f32 1 (sin.f32 normAngle))) n0_i (*.f32 (/.f32 (Rewrite<= *-rgt-identity_binary32 (*.f32 (sin.f32 (*.f32 u normAngle)) 1)) (sin.f32 normAngle)) n1_i)): 0 points increase in error, 0 points decrease in error
(fma.f32 (*.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) (/.f32 1 (sin.f32 normAngle))) n0_i (*.f32 (Rewrite<= associate-*r/_binary32 (*.f32 (sin.f32 (*.f32 u normAngle)) (/.f32 1 (sin.f32 normAngle)))) n1_i)): 20 points increase in error, 8 points decrease in error
(Rewrite<= fma-def_binary32 (+.f32 (*.f32 (*.f32 (sin.f32 (*.f32 (-.f32 1 u) normAngle)) (/.f32 1 (sin.f32 normAngle))) n0_i) (*.f32 (*.f32 (sin.f32 (*.f32 u normAngle)) (/.f32 1 (sin.f32 normAngle))) n1_i))): 5 points increase in error, 2 points decrease in error
Taylor expanded in normAngle around 0 0.7
\[\leadsto \color{blue}{n1_i \cdot u + \left(1 - u\right) \cdot n0_i}
\]
Simplified0.7
\[\leadsto \color{blue}{\mathsf{fma}\left(n1_i, u, \left(1 - u\right) \cdot n0_i\right)}
\]
Proof
(fma.f32 n1_i u (*.f32 (-.f32 1 u) n0_i)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary32 (+.f32 (*.f32 n1_i u) (*.f32 (-.f32 1 u) n0_i))): 14 points increase in error, 2 points decrease in error
Taylor expanded in u around 0 0.6
\[\leadsto \color{blue}{\left(n1_i + -1 \cdot n0_i\right) \cdot u + n0_i}
\]
Taylor expanded in n1_i around 0 0.7
\[\leadsto \color{blue}{-1 \cdot \left(u \cdot n0_i\right) + \left(n1_i \cdot u + n0_i\right)}
\]
Simplified0.6
\[\leadsto \color{blue}{n0_i + u \cdot \left(n1_i - n0_i\right)}
\]
Proof
(+.f32 n0_i (*.f32 u (-.f32 n1_i n0_i))): 0 points increase in error, 0 points decrease in error
(+.f32 n0_i (Rewrite<= distribute-lft-out--_binary32 (-.f32 (*.f32 u n1_i) (*.f32 u n0_i)))): 6 points increase in error, 2 points decrease in error
(+.f32 n0_i (-.f32 (Rewrite<= *-commutative_binary32 (*.f32 n1_i u)) (*.f32 u n0_i))): 0 points increase in error, 0 points decrease in error
(+.f32 n0_i (Rewrite<= unsub-neg_binary32 (+.f32 (*.f32 n1_i u) (neg.f32 (*.f32 u n0_i))))): 0 points increase in error, 0 points decrease in error
(+.f32 n0_i (+.f32 (*.f32 n1_i u) (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (*.f32 u n0_i))))): 0 points increase in error, 0 points decrease in error
(+.f32 n0_i (Rewrite<= +-commutative_binary32 (+.f32 (*.f32 -1 (*.f32 u n0_i)) (*.f32 n1_i u)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary32 (+.f32 (+.f32 (*.f32 -1 (*.f32 u n0_i)) (*.f32 n1_i u)) n0_i)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary32 (+.f32 (*.f32 -1 (*.f32 u n0_i)) (+.f32 (*.f32 n1_i u) n0_i))): 12 points increase in error, 2 points decrease in error
Final simplification0.6
\[\leadsto n0_i + u \cdot \left(n1_i - n0_i\right)
\]