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
[Start]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
\] |
|---|
fma-def [=>]0.9 | \[ \color{blue}{\mathsf{fma}\left(\sin \left(\left(1 - u\right) \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}, n0_i, \left(\sin \left(u \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}\right) \cdot n1_i\right)}
\] |
|---|
associate-*r/ [=>]0.8 | \[ \mathsf{fma}\left(\color{blue}{\frac{\sin \left(\left(1 - u\right) \cdot normAngle\right) \cdot 1}{\sin normAngle}}, n0_i, \left(\sin \left(u \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}\right) \cdot n1_i\right)
\] |
|---|
*-rgt-identity [=>]0.8 | \[ \mathsf{fma}\left(\frac{\color{blue}{\sin \left(\left(1 - u\right) \cdot normAngle\right)}}{\sin normAngle}, n0_i, \left(\sin \left(u \cdot normAngle\right) \cdot \frac{1}{\sin normAngle}\right) \cdot n1_i\right)
\] |
|---|
associate-*r/ [=>]0.7 | \[ \mathsf{fma}\left(\frac{\sin \left(\left(1 - u\right) \cdot normAngle\right)}{\sin normAngle}, n0_i, \color{blue}{\frac{\sin \left(u \cdot normAngle\right) \cdot 1}{\sin normAngle}} \cdot n1_i\right)
\] |
|---|
*-rgt-identity [=>]0.7 | \[ \mathsf{fma}\left(\frac{\sin \left(\left(1 - u\right) \cdot normAngle\right)}{\sin normAngle}, n0_i, \frac{\color{blue}{\sin \left(u \cdot normAngle\right)}}{\sin normAngle} \cdot n1_i\right)
\] |
|---|
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(u, n1_i, \left(1 - u\right) \cdot n0_i\right)}
\]
Proof
[Start]0.7 | \[ n1_i \cdot u + \left(1 - u\right) \cdot n0_i
\] |
|---|
*-commutative [=>]0.7 | \[ \color{blue}{u \cdot n1_i} + \left(1 - u\right) \cdot n0_i
\] |
|---|
fma-def [=>]0.7 | \[ \color{blue}{\mathsf{fma}\left(u, n1_i, \left(1 - u\right) \cdot n0_i\right)}
\] |
|---|
Taylor expanded in u around 0 0.6
\[\leadsto \color{blue}{\left(n1_i + -1 \cdot n0_i\right) \cdot u + n0_i}
\]
Simplified0.6
\[\leadsto \color{blue}{\mathsf{fma}\left(u, n1_i - n0_i, n0_i\right)}
\]
Proof
[Start]0.6 | \[ \left(n1_i + -1 \cdot n0_i\right) \cdot u + n0_i
\] |
|---|
*-commutative [=>]0.6 | \[ \color{blue}{u \cdot \left(n1_i + -1 \cdot n0_i\right)} + n0_i
\] |
|---|
fma-def [=>]0.6 | \[ \color{blue}{\mathsf{fma}\left(u, n1_i + -1 \cdot n0_i, n0_i\right)}
\] |
|---|
mul-1-neg [=>]0.6 | \[ \mathsf{fma}\left(u, n1_i + \color{blue}{\left(-n0_i\right)}, n0_i\right)
\] |
|---|
unsub-neg [=>]0.6 | \[ \mathsf{fma}\left(u, \color{blue}{n1_i - n0_i}, n0_i\right)
\] |
|---|
Final simplification0.6
\[\leadsto \mathsf{fma}\left(u, n1_i - n0_i, n0_i\right)
\]