Initial program 0.0
\[e^{-\left(1 - x \cdot x\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{e^{x \cdot x + -1}}
\]
Proof
(exp.f64 (+.f64 (*.f64 x x) -1)): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= +-commutative_binary64 (+.f64 -1 (*.f64 x x)))): 0 points increase in error, 0 points decrease in error
(exp.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) (*.f64 x x))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 (*.f64 x x))))): 0 points increase in error, 0 points decrease in error
(exp.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 1 (*.f64 x x))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \color{blue}{{\left(e^{x + 1}\right)}^{\left(x + -1\right)}}
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{\left({\left(e^{x}\right)}^{\left(\left(x + -1\right) \cdot 0.5\right)} \cdot {\left(e^{x}\right)}^{\left(\left(x + -1\right) \cdot 0.5\right)}\right) \cdot \left({e}^{\left(\left(x + -1\right) \cdot 0.5\right)} \cdot {e}^{\left(\left(x + -1\right) \cdot 0.5\right)}\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{{\left(e^{x}\right)}^{\left(-1 + x\right)} \cdot {e}^{\left(-1 + x\right)}}
\]
Proof
(*.f64 (pow.f64 (exp.f64 x) (+.f64 -1 x)) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) (Rewrite<= +-commutative_binary64 (+.f64 x -1))) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 x -1)))) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) (*.f64 (Rewrite<= metadata-eval (*.f64 2 1/2)) (+.f64 x -1))) (pow.f64 (E.f64) (+.f64 -1 x))): 6 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 1/2 (+.f64 x -1))))) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 6 points decrease in error
(*.f64 (pow.f64 (exp.f64 x) (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x -1) 1/2)))) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)))) (pow.f64 (E.f64) (+.f64 -1 x))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (pow.f64 (E.f64) (Rewrite<= +-commutative_binary64 (+.f64 x -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (pow.f64 (E.f64) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (+.f64 x -1))))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (pow.f64 (E.f64) (*.f64 (Rewrite<= metadata-eval (*.f64 2 1/2)) (+.f64 x -1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (pow.f64 (E.f64) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 1/2 (+.f64 x -1)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (pow.f64 (E.f64) (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x -1) 1/2))))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (exp.f64 x) (*.f64 (+.f64 x -1) 1/2))) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (E.f64) (*.f64 (+.f64 x -1) 1/2)) (pow.f64 (E.f64) (*.f64 (+.f64 x -1) 1/2))))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto {\left(e^{x}\right)}^{\left(x + -1\right)} \cdot {e}^{\left(x + -1\right)}
\]