- Split input into 2 regimes
if (* y z) < -1.00202048192943851e223 or 4.274334395903164e168 < (* y z)
Initial program 24.7
\[x \cdot \left(1 - y \cdot z\right)\]
- Using strategy
rm Applied sub-neg24.7
\[\leadsto x \cdot \color{blue}{\left(1 + \left(-y \cdot z\right)\right)}\]
Applied distribute-lft-in24.7
\[\leadsto \color{blue}{x \cdot 1 + x \cdot \left(-y \cdot z\right)}\]
Simplified24.7
\[\leadsto \color{blue}{1 \cdot x} + x \cdot \left(-y \cdot z\right)\]
- Using strategy
rm Applied distribute-lft-neg-in24.7
\[\leadsto 1 \cdot x + x \cdot \color{blue}{\left(\left(-y\right) \cdot z\right)}\]
Applied associate-*r*1.2
\[\leadsto 1 \cdot x + \color{blue}{\left(x \cdot \left(-y\right)\right) \cdot z}\]
Simplified1.2
\[\leadsto 1 \cdot x + \color{blue}{\left(\left(-x\right) \cdot y\right)} \cdot z\]
if -1.00202048192943851e223 < (* y z) < 4.274334395903164e168
Initial program 0.1
\[x \cdot \left(1 - y \cdot z\right)\]
- Using strategy
rm Applied sub-neg0.1
\[\leadsto x \cdot \color{blue}{\left(1 + \left(-y \cdot z\right)\right)}\]
Applied distribute-lft-in0.1
\[\leadsto \color{blue}{x \cdot 1 + x \cdot \left(-y \cdot z\right)}\]
Simplified0.1
\[\leadsto \color{blue}{1 \cdot x} + x \cdot \left(-y \cdot z\right)\]
- Recombined 2 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l}
\mathbf{if}\;y \cdot z \le -1.00202048192943851 \cdot 10^{223} \lor \neg \left(y \cdot z \le 4.274334395903164 \cdot 10^{168}\right):\\
\;\;\;\;1 \cdot x + \left(\left(-x\right) \cdot y\right) \cdot z\\
\mathbf{else}:\\
\;\;\;\;1 \cdot x + x \cdot \left(-y \cdot z\right)\\
\end{array}\]