Initial program 2.81
\[\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
\]
Simplified2.24
\[\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]2.81 | \[ \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 [=>]2.78 | \[ \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/ [=>]2.55 | \[ \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 [=>]2.55 | \[ \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/ [=>]2.24 | \[ \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 [=>]2.24 | \[ \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 2.16
\[\leadsto \color{blue}{n1_i \cdot u + \left(1 - u\right) \cdot n0_i}
\]
Simplified2.04
\[\leadsto \color{blue}{\mathsf{fma}\left(u, n1_i, \left(1 - u\right) \cdot n0_i\right)}
\]
Proof
[Start]2.16 | \[ n1_i \cdot u + \left(1 - u\right) \cdot n0_i
\] |
|---|
*-commutative [=>]2.16 | \[ \color{blue}{u \cdot n1_i} + \left(1 - u\right) \cdot n0_i
\] |
|---|
fma-def [=>]2.04 | \[ \color{blue}{\mathsf{fma}\left(u, n1_i, \left(1 - u\right) \cdot n0_i\right)}
\] |
|---|
Applied egg-rr1.91
\[\leadsto \mathsf{fma}\left(u, n1_i, \color{blue}{n0_i \cdot \left(-u\right) + n0_i}\right)
\]
Taylor expanded in n0_i around 0 2.04
\[\leadsto \mathsf{fma}\left(u, n1_i, \color{blue}{\left(1 + -1 \cdot u\right) \cdot n0_i}\right)
\]
Simplified1.91
\[\leadsto \mathsf{fma}\left(u, n1_i, \color{blue}{n0_i - u \cdot n0_i}\right)
\]
Proof
[Start]2.04 | \[ \mathsf{fma}\left(u, n1_i, \left(1 + -1 \cdot u\right) \cdot n0_i\right)
\] |
|---|
+-commutative [=>]2.04 | \[ \mathsf{fma}\left(u, n1_i, \color{blue}{\left(-1 \cdot u + 1\right)} \cdot n0_i\right)
\] |
|---|
mul-1-neg [=>]2.04 | \[ \mathsf{fma}\left(u, n1_i, \left(\color{blue}{\left(-u\right)} + 1\right) \cdot n0_i\right)
\] |
|---|
distribute-rgt1-in [<=]1.91 | \[ \mathsf{fma}\left(u, n1_i, \color{blue}{n0_i + \left(-u\right) \cdot n0_i}\right)
\] |
|---|
cancel-sign-sub-inv [<=]1.91 | \[ \mathsf{fma}\left(u, n1_i, \color{blue}{n0_i - u \cdot n0_i}\right)
\] |
|---|
Final simplification1.91
\[\leadsto \mathsf{fma}\left(u, n1_i, n0_i - u \cdot n0_i\right)
\]