Initial program 0.1
\[\left(a - \frac{1}{3}\right) \cdot \left(1 + \frac{1}{\sqrt{9 \cdot \left(a - \frac{1}{3}\right)}} \cdot rand\right)
\]
Simplified0.1
\[\leadsto \color{blue}{\left(a + -0.3333333333333333\right) \cdot \left(1 + \frac{1}{\sqrt{\left(a + -0.3333333333333333\right) \cdot 9}} \cdot rand\right)}
\]
Proof
(*.f64 (+.f64 a -1/3) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a -1/3) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 a (Rewrite<= metadata-eval (neg.f64 1/3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a -1/3) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 a (neg.f64 (Rewrite<= metadata-eval (/.f64 1 3)))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a -1/3) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= sub-neg_binary64 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a -1/3) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 a (/.f64 1 3)))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a -1/3) 9))) rand))): 14 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a (Rewrite<= metadata-eval (neg.f64 1/3))) 9))) rand))): 0 points increase in error, 14 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (+.f64 a (neg.f64 (Rewrite<= metadata-eval (/.f64 1 3)))) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 a (/.f64 1 3))) 9))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 9 (-.f64 a (/.f64 1 3)))))) rand))): 14 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (+.f64 1 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand)))))): 0 points increase in error, 14 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (Rewrite<= sub-neg_binary64 (-.f64 1 (neg.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand))))): 14 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (-.f64 1 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3)))))) rand)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (Rewrite=> cancel-sign-sub_binary64 (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> *-lft-identity_binary64 (-.f64 a (/.f64 1 3))) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand))): 0 points increase in error, 14 points decrease in error
Applied egg-rr0.1
\[\leadsto \left(a + -0.3333333333333333\right) \cdot \left(1 + \color{blue}{\frac{\frac{rand}{\sqrt{a + -0.3333333333333333}}}{3}}\right)
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{a + \left(-0.3333333333333333 + \frac{a + -0.3333333333333333}{\frac{3}{rand} \cdot \sqrt{a + -0.3333333333333333}}\right)}
\]
Simplified0.1
\[\leadsto \color{blue}{\left(a + -0.3333333333333333\right) + \frac{a + -0.3333333333333333}{\sqrt{a + -0.3333333333333333}} \cdot \frac{rand}{3}}
\]
Proof
(+.f64 (+.f64 a -1/3) (*.f64 (/.f64 (+.f64 a -1/3) (sqrt.f64 (+.f64 a -1/3))) (/.f64 rand 3))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 a -1/3) (/.f64 (sqrt.f64 (+.f64 a -1/3)) (/.f64 rand 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (/.f64 (+.f64 a -1/3) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (+.f64 a -1/3)) 3) rand)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (/.f64 (+.f64 a -1/3) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 3 (sqrt.f64 (+.f64 a -1/3)))) rand))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (/.f64 (+.f64 a -1/3) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 3 rand) (sqrt.f64 (+.f64 a -1/3)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 (+.f64 a -1/3) (*.f64 (/.f64 3 rand) (sqrt.f64 (+.f64 a -1/3)))) 1))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 a -1/3) (Rewrite=> *-rgt-identity_binary64 (/.f64 (+.f64 a -1/3) (*.f64 (/.f64 3 rand) (sqrt.f64 (+.f64 a -1/3)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 a (+.f64 -1/3 (/.f64 (+.f64 a -1/3) (*.f64 (/.f64 3 rand) (sqrt.f64 (+.f64 a -1/3))))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.2
\[\leadsto \left(a + -0.3333333333333333\right) + \color{blue}{\frac{\sqrt{a + -0.3333333333333333} \cdot rand}{3}}
\]
Final simplification0.2
\[\leadsto \left(a + -0.3333333333333333\right) + \frac{\sqrt{a + -0.3333333333333333} \cdot rand}{3}
\]