normal distribution

1. Initial program 99.3%

   \[\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]
2. Step-by-step derivation

   1. add-sqr-sqrt99.0%

      \[\leadsto \color{blue}{\left(\sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}} \cdot \sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. sqrt-unprod99.3%

      \[\leadsto \color{blue}{\sqrt{\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. pow1/299.3%

      \[\leadsto \sqrt{\left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   4. *-commutative99.3%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)} \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   5. pow1/299.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   6. *-commutative99.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   7. swap-sqr99.4%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \sqrt{-2 \cdot \log u1}\right) \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   8. add-sqr-sqrt99.6%

      \[\leadsto \sqrt{\color{blue}{\left(-2 \cdot \log u1\right)} \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   9. metadata-eval99.6%

      \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(\color{blue}{0.16666666666666666} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   10. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(0.16666666666666666 \cdot \color{blue}{0.16666666666666666}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   11. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \color{blue}{0.027777777777777776}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

3. Applied egg-rr99.6%

   \[\leadsto \color{blue}{\sqrt{\left(-2 \cdot \log u1\right) \cdot 0.027777777777777776}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]
4. Step-by-step derivation

   1. *-commutative99.6%

      \[\leadsto \sqrt{\color{blue}{\left(\log u1 \cdot -2\right)} \cdot 0.027777777777777776} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. associate-*l*99.6%

      \[\leadsto \sqrt{\color{blue}{\log u1 \cdot \left(-2 \cdot 0.027777777777777776\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. metadata-eval99.6%

      \[\leadsto \sqrt{\log u1 \cdot \color{blue}{-0.05555555555555555}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

5. Simplified99.6%

   \[\leadsto \color{blue}{\sqrt{\log u1 \cdot -0.05555555555555555}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

6. Final simplification99.6%

   \[\leadsto \sqrt{\log u1 \cdot -0.05555555555555555} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

1. Initial program 99.3%

   \[\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

2. Taylor expanded in u2 around 0 98.6%

   \[\leadsto \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \color{blue}{1} + 0.5 \]
3. Step-by-step derivation

   1. add-sqr-sqrt99.0%

      \[\leadsto \color{blue}{\left(\sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}} \cdot \sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. sqrt-unprod99.3%

      \[\leadsto \color{blue}{\sqrt{\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. pow1/299.3%

      \[\leadsto \sqrt{\left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   4. *-commutative99.3%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)} \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   5. pow1/299.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   6. *-commutative99.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   7. swap-sqr99.4%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \sqrt{-2 \cdot \log u1}\right) \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   8. add-sqr-sqrt99.6%

      \[\leadsto \sqrt{\color{blue}{\left(-2 \cdot \log u1\right)} \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   9. metadata-eval99.6%

      \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(\color{blue}{0.16666666666666666} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   10. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(0.16666666666666666 \cdot \color{blue}{0.16666666666666666}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   11. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \color{blue}{0.027777777777777776}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

4. Applied egg-rr98.9%

   \[\leadsto \color{blue}{\sqrt{\left(-2 \cdot \log u1\right) \cdot 0.027777777777777776}} \cdot 1 + 0.5 \]
5. Step-by-step derivation

   1. *-commutative99.6%

      \[\leadsto \sqrt{\color{blue}{\left(\log u1 \cdot -2\right)} \cdot 0.027777777777777776} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. associate-*l*99.6%

      \[\leadsto \sqrt{\color{blue}{\log u1 \cdot \left(-2 \cdot 0.027777777777777776\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. metadata-eval99.6%

      \[\leadsto \sqrt{\log u1 \cdot \color{blue}{-0.05555555555555555}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

6. Simplified98.9%

   \[\leadsto \color{blue}{\sqrt{\log u1 \cdot -0.05555555555555555}} \cdot 1 + 0.5 \]
7. Step-by-step derivation

   1. add-log-exp98.9%

      \[\leadsto \sqrt{\color{blue}{\log \left(e^{\log u1 \cdot -0.05555555555555555}\right)}} \cdot 1 + 0.5 \]

   2. exp-to-pow98.9%

      \[\leadsto \sqrt{\log \color{blue}{\left({u1}^{-0.05555555555555555}\right)}} \cdot 1 + 0.5 \]

8. Applied egg-rr98.9%

   \[\leadsto \sqrt{\color{blue}{\log \left({u1}^{-0.05555555555555555}\right)}} \cdot 1 + 0.5 \]

9. Taylor expanded in u1 around 0 98.9%

   \[\leadsto \color{blue}{0.5 + \sqrt{\log \left({u1}^{-0.05555555555555555}\right)}} \]

10. Final simplification98.9%

    \[\leadsto 0.5 + \sqrt{\log \left({u1}^{-0.05555555555555555}\right)} \]

1. Initial program 99.3%

   \[\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

2. Taylor expanded in u2 around 0 98.6%

   \[\leadsto \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \color{blue}{1} + 0.5 \]
3. Step-by-step derivation

   1. add-sqr-sqrt99.0%

      \[\leadsto \color{blue}{\left(\sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}} \cdot \sqrt{\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. sqrt-unprod99.3%

      \[\leadsto \color{blue}{\sqrt{\left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. pow1/299.3%

      \[\leadsto \sqrt{\left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right) \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   4. *-commutative99.3%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)} \cdot \left(\frac{1}{6} \cdot {\left(-2 \cdot \log u1\right)}^{0.5}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   5. pow1/299.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \left(\frac{1}{6} \cdot \color{blue}{\sqrt{-2 \cdot \log u1}}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   6. *-commutative99.3%

      \[\leadsto \sqrt{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right) \cdot \color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   7. swap-sqr99.4%

      \[\leadsto \sqrt{\color{blue}{\left(\sqrt{-2 \cdot \log u1} \cdot \sqrt{-2 \cdot \log u1}\right) \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   8. add-sqr-sqrt99.6%

      \[\leadsto \sqrt{\color{blue}{\left(-2 \cdot \log u1\right)} \cdot \left(\frac{1}{6} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   9. metadata-eval99.6%

      \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(\color{blue}{0.16666666666666666} \cdot \frac{1}{6}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   10. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \left(0.16666666666666666 \cdot \color{blue}{0.16666666666666666}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   11. metadata-eval99.6%

       \[\leadsto \sqrt{\left(-2 \cdot \log u1\right) \cdot \color{blue}{0.027777777777777776}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

4. Applied egg-rr98.9%

   \[\leadsto \color{blue}{\sqrt{\left(-2 \cdot \log u1\right) \cdot 0.027777777777777776}} \cdot 1 + 0.5 \]
5. Step-by-step derivation

   1. *-commutative99.6%

      \[\leadsto \sqrt{\color{blue}{\left(\log u1 \cdot -2\right)} \cdot 0.027777777777777776} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   2. associate-*l*99.6%

      \[\leadsto \sqrt{\color{blue}{\log u1 \cdot \left(-2 \cdot 0.027777777777777776\right)}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

   3. metadata-eval99.6%

      \[\leadsto \sqrt{\log u1 \cdot \color{blue}{-0.05555555555555555}} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) + 0.5 \]

6. Simplified98.9%

   \[\leadsto \color{blue}{\sqrt{\log u1 \cdot -0.05555555555555555}} \cdot 1 + 0.5 \]
7. Step-by-step derivation

   1. *-un-lft-identity98.9%

      \[\leadsto \color{blue}{1 \cdot \left(\sqrt{\log u1 \cdot -0.05555555555555555} \cdot 1\right)} + 0.5 \]

   2. fma-def98.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(1, \sqrt{\log u1 \cdot -0.05555555555555555} \cdot 1, 0.5\right)} \]

   3. *-rgt-identity98.9%

      \[\leadsto \mathsf{fma}\left(1, \color{blue}{\sqrt{\log u1 \cdot -0.05555555555555555}}, 0.5\right) \]

   4. add-log-exp98.9%

      \[\leadsto \mathsf{fma}\left(1, \sqrt{\color{blue}{\log \left(e^{\log u1 \cdot -0.05555555555555555}\right)}}, 0.5\right) \]

   5. exp-to-pow98.9%

      \[\leadsto \mathsf{fma}\left(1, \sqrt{\log \color{blue}{\left({u1}^{-0.05555555555555555}\right)}}, 0.5\right) \]

8. Applied egg-rr98.9%

   \[\leadsto \color{blue}{\mathsf{fma}\left(1, \sqrt{\log \left({u1}^{-0.05555555555555555}\right)}, 0.5\right)} \]
9. Step-by-step derivation

   1. fma-udef98.9%

      \[\leadsto \color{blue}{1 \cdot \sqrt{\log \left({u1}^{-0.05555555555555555}\right)} + 0.5} \]

   2. *-lft-identity98.9%

      \[\leadsto \color{blue}{\sqrt{\log \left({u1}^{-0.05555555555555555}\right)}} + 0.5 \]

   3. +-commutative98.9%

      \[\leadsto \color{blue}{0.5 + \sqrt{\log \left({u1}^{-0.05555555555555555}\right)}} \]

   4. log-pow98.9%

      \[\leadsto 0.5 + \sqrt{\color{blue}{-0.05555555555555555 \cdot \log u1}} \]

   5. *-commutative98.9%

      \[\leadsto 0.5 + \sqrt{\color{blue}{\log u1 \cdot -0.05555555555555555}} \]

10. Simplified98.9%

    \[\leadsto \color{blue}{0.5 + \sqrt{\log u1 \cdot -0.05555555555555555}} \]

11. Final simplification98.9%

    \[\leadsto \sqrt{\log u1 \cdot -0.05555555555555555} + 0.5 \]

herbie shell --seed 2023166 
(FPCore (u1 u2)
  :name "normal distribution"
  :precision binary64
  :pre (and (and (<= 0.0 u1) (<= u1 1.0)) (and (<= 0.0 u2) (<= u2 1.0)))
  (+ (* (* (/ 1.0 6.0) (pow (* -2.0 (log u1)) 0.5)) (cos (* (* 2.0 PI) u2))) 0.5))