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 (-.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, 0 points decrease in error
(*.f64 (-.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 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 a (/.f64 1 3)) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 9 (-.f64 a (/.f64 1 3)))))) rand))): 0 points increase in error, 0 points decrease in error
(*.f64 (-.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, 0 points decrease in error
(*.f64 (-.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))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 1 (-.f64 a (/.f64 1 3))) (*.f64 (neg.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand)) (-.f64 a (/.f64 1 3))))): 1 points increase in error, 5 points decrease in error
(-.f64 (Rewrite=> *-lft-identity_binary64 (-.f64 a (/.f64 1 3))) (*.f64 (neg.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand)) (-.f64 a (/.f64 1 3)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub_binary64 (+.f64 (-.f64 a (/.f64 1 3)) (*.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand) (-.f64 a (/.f64 1 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 a (/.f64 1 3)))) (*.f64 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand) (-.f64 a (/.f64 1 3)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-in_binary64 (*.f64 (-.f64 a (/.f64 1 3)) (+.f64 1 (*.f64 (/.f64 1 (sqrt.f64 (*.f64 9 (-.f64 a (/.f64 1 3))))) rand)))): 5 points increase in error, 1 points decrease in error
Applied egg-rr0.1
\[\leadsto \left(a + -0.3333333333333333\right) \cdot \left(1 + \color{blue}{\frac{-rand}{\sqrt{a + -0.3333333333333333} \cdot -3}}\right)
\]
Simplified0.1
\[\leadsto \left(a + -0.3333333333333333\right) \cdot \left(1 + \color{blue}{\frac{\frac{rand}{3}}{\sqrt{a + -0.3333333333333333}}}\right)
\]
Proof
(/.f64 (/.f64 rand 3) (sqrt.f64 (+.f64 a -1/3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 rand (*.f64 3 (sqrt.f64 (+.f64 a -1/3))))): 38 points increase in error, 37 points decrease in error
(/.f64 rand (*.f64 (Rewrite<= metadata-eval (/.f64 1 1/3)) (sqrt.f64 (+.f64 a -1/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 rand (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 1/3 (sqrt.f64 (+.f64 a -1/3)))))): 56 points increase in error, 23 points decrease in error
(/.f64 rand (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 1 (sqrt.f64 (+.f64 a -1/3))) 1/3))): 21 points increase in error, 31 points decrease in error
(/.f64 rand (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 (+.f64 a -1/3)) 1)) 1/3)): 0 points increase in error, 0 points decrease in error
(/.f64 rand (/.f64 (Rewrite=> *-rgt-identity_binary64 (sqrt.f64 (+.f64 a -1/3))) 1/3)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 rand (sqrt.f64 (+.f64 a -1/3))) 1/3)): 39 points increase in error, 40 points decrease in error
(*.f64 (/.f64 rand (sqrt.f64 (+.f64 a -1/3))) (Rewrite<= metadata-eval (/.f64 -1 -3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 rand -1) (*.f64 (sqrt.f64 (+.f64 a -1/3)) -3))): 32 points increase in error, 58 points decrease in error
(/.f64 (Rewrite=> *-commutative_binary64 (*.f64 -1 rand)) (*.f64 (sqrt.f64 (+.f64 a -1/3)) -3)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 rand)) (*.f64 (sqrt.f64 (+.f64 a -1/3)) -3)): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto \left(1 + \frac{\frac{rand}{3}}{\sqrt{a + -0.3333333333333333}}\right) \cdot \left(a + -0.3333333333333333\right)
\]