Initial program 77.8%
\[20 - \left(e^{\pi} - \pi\right)
\]
Step-by-step derivation
lift--.f64N/A
\[\leadsto \color{blue}{20 - \left(e^{\pi} - \pi\right)}
\]
sub-to-multN/A
\[\leadsto \color{blue}{\left(1 - \frac{e^{\pi} - \pi}{20}\right) \cdot 20}
\]
lower-unsound-*.f64N/A
\[\leadsto \color{blue}{\left(1 - \frac{e^{\pi} - \pi}{20}\right) \cdot 20}
\]
lower-unsound--.f64N/A
\[\leadsto \color{blue}{\left(1 - \frac{e^{\pi} - \pi}{20}\right)} \cdot 20
\]
lower-unsound-/.f6478.3%
\[\leadsto \left(1 - \color{blue}{\frac{e^{\pi} - \pi}{20}}\right) \cdot 20
\]
Applied rewrites78.3%
\[\leadsto \color{blue}{\left(1 - \frac{e^{\pi} - \pi}{20}\right) \cdot 20}
\]
Step-by-step derivation
lift-/.f64N/A
\[\leadsto \left(1 - \color{blue}{\frac{e^{\pi} - \pi}{20}}\right) \cdot 20
\]
lift--.f64N/A
\[\leadsto \left(1 - \frac{\color{blue}{e^{\pi} - \pi}}{20}\right) \cdot 20
\]
div-subN/A
\[\leadsto \left(1 - \color{blue}{\left(\frac{e^{\pi}}{20} - \frac{\pi}{20}\right)}\right) \cdot 20
\]
lower--.f64N/A
\[\leadsto \left(1 - \color{blue}{\left(\frac{e^{\pi}}{20} - \frac{\pi}{20}\right)}\right) \cdot 20
\]
mult-flipN/A
\[\leadsto \left(1 - \left(\color{blue}{e^{\pi} \cdot \frac{1}{20}} - \frac{\pi}{20}\right)\right) \cdot 20
\]
lower-*.f64N/A
\[\leadsto \left(1 - \left(\color{blue}{e^{\pi} \cdot \frac{1}{20}} - \frac{\pi}{20}\right)\right) \cdot 20
\]
metadata-evalN/A
\[\leadsto \left(1 - \left(e^{\pi} \cdot \color{blue}{\frac{1}{20}} - \frac{\pi}{20}\right)\right) \cdot 20
\]
mult-flipN/A
\[\leadsto \left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \color{blue}{\pi \cdot \frac{1}{20}}\right)\right) \cdot 20
\]
lower-*.f64N/A
\[\leadsto \left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \color{blue}{\pi \cdot \frac{1}{20}}\right)\right) \cdot 20
\]
metadata-eval80.6%
\[\leadsto \left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \color{blue}{\frac{1}{20}}\right)\right) \cdot 20
\]
Applied rewrites80.6%
\[\leadsto \left(1 - \color{blue}{\left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \frac{1}{20}\right)}\right) \cdot 20
\]
Step-by-step derivation
lift-*.f64N/A
\[\leadsto \color{blue}{\left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \frac{1}{20}\right)\right) \cdot 20}
\]
*-commutativeN/A
\[\leadsto \color{blue}{20 \cdot \left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \frac{1}{20}\right)\right)}
\]
lift--.f64N/A
\[\leadsto 20 \cdot \color{blue}{\left(1 - \left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \frac{1}{20}\right)\right)}
\]
lift--.f64N/A
\[\leadsto 20 \cdot \left(1 - \color{blue}{\left(e^{\pi} \cdot \frac{1}{20} - \pi \cdot \frac{1}{20}\right)}\right)
\]
associate--r-N/A
\[\leadsto 20 \cdot \color{blue}{\left(\left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \pi \cdot \frac{1}{20}\right)}
\]
distribute-lft-inN/A
\[\leadsto \color{blue}{20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + 20 \cdot \left(\pi \cdot \frac{1}{20}\right)}
\]
lift-*.f64N/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + 20 \cdot \color{blue}{\left(\pi \cdot \frac{1}{20}\right)}
\]
*-commutativeN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + 20 \cdot \color{blue}{\left(\frac{1}{20} \cdot \pi\right)}
\]
associate-*r*N/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \color{blue}{\left(20 \cdot \frac{1}{20}\right) \cdot \pi}
\]
metadata-evalN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \color{blue}{1} \cdot \pi
\]
rem-log-expN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + 1 \cdot \color{blue}{\log \left(e^{\pi}\right)}
\]
lift-exp.f64N/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + 1 \cdot \log \color{blue}{\left(e^{\pi}\right)}
\]
log-pow-revN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \color{blue}{\log \left({\left(e^{\pi}\right)}^{1}\right)}
\]
metadata-evalN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \log \left({\left(e^{\pi}\right)}^{\color{blue}{\left(\mathsf{neg}\left(-1\right)\right)}}\right)
\]
pow-flipN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \log \color{blue}{\left(\frac{1}{{\left(e^{\pi}\right)}^{-1}}\right)}
\]
inv-powN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \log \left(\frac{1}{\color{blue}{\frac{1}{e^{\pi}}}}\right)
\]
neg-logN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \color{blue}{\left(\mathsf{neg}\left(\log \left(\frac{1}{e^{\pi}}\right)\right)\right)}
\]
neg-logN/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(\log \left(e^{\pi}\right)\right)\right)}\right)\right)
\]
lift-exp.f64N/A
\[\leadsto 20 \cdot \left(1 - e^{\pi} \cdot \frac{1}{20}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\log \color{blue}{\left(e^{\pi}\right)}\right)\right)\right)\right)
\]
Applied rewrites80.6%
\[\leadsto \color{blue}{\left(1 - \frac{1}{20} \cdot e^{\pi}\right) \cdot 20 + \pi}
\]
Step-by-step derivation
lift--.f64N/A
\[\leadsto \color{blue}{\left(1 - \frac{1}{20} \cdot e^{\pi}\right)} \cdot 20 + \pi
\]
lift-*.f64N/A
\[\leadsto \left(1 - \color{blue}{\frac{1}{20} \cdot e^{\pi}}\right) \cdot 20 + \pi
\]
fp-cancel-sub-sign-invN/A
\[\leadsto \color{blue}{\left(1 + \left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)} \cdot 20 + \pi
\]
+-commutativeN/A
\[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi} + 1\right)} \cdot 20 + \pi
\]
sum-to-multN/A
\[\leadsto \color{blue}{\left(\left(1 + \frac{1}{\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}}\right) \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right)} \cdot 20 + \pi
\]
lower-unsound-*.f64N/A
\[\leadsto \color{blue}{\left(\left(1 + \frac{1}{\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}}\right) \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right)} \cdot 20 + \pi
\]
lower-unsound-+.f64N/A
\[\leadsto \left(\color{blue}{\left(1 + \frac{1}{\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}}\right)} \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right) \cdot 20 + \pi
\]
lower-unsound-/.f64N/A
\[\leadsto \left(\left(1 + \color{blue}{\frac{1}{\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}}}\right) \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right) \cdot 20 + \pi
\]
lower-*.f64N/A
\[\leadsto \left(\left(1 + \frac{1}{\color{blue}{\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}}}\right) \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right) \cdot 20 + \pi
\]
metadata-evalN/A
\[\leadsto \left(\left(1 + \frac{1}{\color{blue}{\frac{-1}{20}} \cdot e^{\pi}}\right) \cdot \left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)\right) \cdot 20 + \pi
\]
lower-*.f64N/A
\[\leadsto \left(\left(1 + \frac{1}{\frac{-1}{20} \cdot e^{\pi}}\right) \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{1}{20}\right)\right) \cdot e^{\pi}\right)}\right) \cdot 20 + \pi
\]
metadata-eval83.9%
\[\leadsto \left(\left(1 + \frac{1}{\frac{-1}{20} \cdot e^{\pi}}\right) \cdot \left(\color{blue}{\frac{-1}{20}} \cdot e^{\pi}\right)\right) \cdot 20 + \pi
\]
Applied rewrites83.9%
\[\leadsto \color{blue}{\left(\left(1 + \frac{1}{\frac{-1}{20} \cdot e^{\pi}}\right) \cdot \left(\frac{-1}{20} \cdot e^{\pi}\right)\right)} \cdot 20 + \pi
\]
- Add Preprocessing