Initial program 99.1%
\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
\]
Applied egg-rr99.1%
\[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right)}
\]
Proof
[Start]99.1 | \[ \cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)
\] |
|---|
expm1-log1p-u [=>]99.1 | \[ \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)\right)}
\] |
|---|
sub-neg [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{1 + \left(-5 \cdot \left(v \cdot v\right)\right)}}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
+-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{\left(-5 \cdot \left(v \cdot v\right)\right) + 1}}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
*-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\left(-\color{blue}{\left(v \cdot v\right) \cdot 5}\right) + 1}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
distribute-rgt-neg-in [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{\left(v \cdot v\right) \cdot \left(-5\right)} + 1}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
fma-def [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{\mathsf{fma}\left(v \cdot v, -5, 1\right)}}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
metadata-eval [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, \color{blue}{-5}, 1\right)}{v \cdot v - 1}\right)\right)\right)
\] |
|---|
fma-neg [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\color{blue}{\mathsf{fma}\left(v, v, -1\right)}}\right)\right)\right)
\] |
|---|
metadata-eval [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, \color{blue}{-1}\right)}\right)\right)\right)
\] |
|---|
Applied egg-rr99.1%
\[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2} - 1}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right) + 1}}\right)\right)
\]
Proof
[Start]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right)
\] |
|---|
expm1-log1p-u [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right)}\right)\right)
\] |
|---|
expm1-udef [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{e^{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} - 1}\right)\right)
\] |
|---|
flip-- [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{e^{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} \cdot e^{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} - 1 \cdot 1}{e^{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v \cdot v, -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} + 1}}\right)\right)
\] |
|---|
Simplified99.1%
\[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}\right)\right)
\]
Proof
[Start]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2} - 1}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right) + 1}\right)\right)
\] |
|---|
sub-neg [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\color{blue}{{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2} + \left(-1\right)}}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right) + 1}\right)\right)
\] |
|---|
metadata-eval [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2} + \color{blue}{-1}}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right) + 1}\right)\right)
\] |
|---|
+-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\color{blue}{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right) + 1}\right)\right)
\] |
|---|
+-commutative [<=]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\color{blue}{1 + \left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}}\right)\right)
\] |
|---|
associate-+r+ [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\color{blue}{\left(1 + 1\right) + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}\right)\right)
\] |
|---|
metadata-eval [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\color{blue}{2} + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right)\right)
\] |
|---|
Applied egg-rr99.1%
\[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{1}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}} \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}}\right)\right)
\]
Proof
[Start]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right)\right)
\] |
|---|
*-un-lft-identity [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\color{blue}{1 \cdot \left(-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}\right)}}{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right)\right)
\] |
|---|
add-cube-cbrt [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1 \cdot \left(-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}\right)}{\color{blue}{\left(\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)} \cdot \sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right) \cdot \sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}}\right)\right)
\] |
|---|
times-frac [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{1}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)} \cdot \sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}} \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}}\right)\right)
\] |
|---|
pow2 [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\color{blue}{{\left(\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right)}^{2}}} \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}\right)\right)
\] |
|---|
+-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{{\left(\sqrt[3]{\color{blue}{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}\right)}^{2}} \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}\right)\right)
\] |
|---|
Simplified99.1%
\[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}}{{\left(\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}\right)}^{2}}}\right)\right)
\]
Proof
[Start]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}} \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}\right)\right)
\] |
|---|
associate-*l/ [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\color{blue}{\frac{1 \cdot \frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}}}\right)\right)
\] |
|---|
*-lft-identity [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\color{blue}{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}}}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}}\right)\right)
\] |
|---|
+-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\color{blue}{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}}}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}}\right)\right)
\] |
|---|
+-commutative [=>]99.1 | \[ \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}}{{\left(\sqrt[3]{\color{blue}{2 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)}}\right)}^{2}}\right)\right)
\] |
|---|
Final simplification99.1%
\[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\frac{-1 + {\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}^{2}}{\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}}}{{\left(\sqrt[3]{\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2}\right)}^{2}}\right)\right)
\]