Initial program 0.0
\[1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}\]
- Using strategy
rm Applied log1p-expm1-u0.0
\[\leadsto 1 - \color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}\right)\right)}\]
- Using strategy
rm Applied *-un-lft-identity0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{\color{blue}{1 \cdot \left(1 + \frac{1}{t}\right)}}\right)}\right)\right)\]
Applied add-cube-cbrt0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\color{blue}{\left(\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}\right) \cdot \sqrt[3]{\frac{2}{t}}}}{1 \cdot \left(1 + \frac{1}{t}\right)}\right)}\right)\right)\]
Applied times-frac0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \color{blue}{\frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1} \cdot \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}}\right)}\right)\right)\]
Applied add-sqr-sqrt0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\color{blue}{\sqrt{2} \cdot \sqrt{2}} - \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1} \cdot \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}\right)}\right)\right)\]
Applied prod-diff0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\sqrt{2}, \sqrt{2}, -\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right) + \mathsf{fma}\left(-\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}, \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}, \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right)\right)}}\right)\right)\]
Applied distribute-lft-in0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \color{blue}{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(\sqrt{2}, \sqrt{2}, -\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right) + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(-\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}, \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}, \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right)\right)}}\right)\right)\]
Simplified0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(1, 2, -\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right)} + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(-\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}, \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}, \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right)\right)}\right)\right)\]
Final simplification0.0
\[\leadsto 1 - \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{1}{2 + \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(1, 2, -\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right) + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \mathsf{fma}\left(-\frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}}, \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}, \frac{\sqrt[3]{\frac{2}{t}}}{1 + \frac{1}{t}} \cdot \frac{\sqrt[3]{\frac{2}{t}} \cdot \sqrt[3]{\frac{2}{t}}}{1}\right)\right)}\right)\right)\]