Simplified26.5
\[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \color{blue}{\left(c \cdot \left(\frac{-0.6666666666666666}{t} - \left(-0.8333333333333334 - a\right)\right)\right)}}}
\]
Proof
(*.f64 c (-.f64 (/.f64 -2/3 t) (-.f64 -5/6 a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 2/3)) t) (-.f64 -5/6 a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 2/3 t))) (-.f64 -5/6 a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 2/3 1)) t)) (-.f64 -5/6 a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 2/3 (/.f64 1 t)))) (-.f64 -5/6 a))): 6 points increase in error, 9 points decrease in error
(*.f64 c (-.f64 (neg.f64 (*.f64 2/3 (/.f64 1 t))) (-.f64 (Rewrite<= metadata-eval (neg.f64 5/6)) a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (neg.f64 (*.f64 2/3 (/.f64 1 t))) (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 5/6) (neg.f64 a))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (-.f64 (neg.f64 (*.f64 2/3 (/.f64 1 t))) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 5/6 a))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (*.f64 2/3 (/.f64 1 t))) (neg.f64 (neg.f64 (+.f64 5/6 a)))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (*.f64 2/3 (/.f64 1 t)) (neg.f64 (+.f64 5/6 a)))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 2/3 (/.f64 1 t)) (+.f64 5/6 a))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite=> neg-sub0_binary64 (-.f64 0 (-.f64 (*.f64 2/3 (/.f64 1 t)) (+.f64 5/6 a))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 2/3 (/.f64 1 t))) (+.f64 5/6 a)))): 0 points increase in error, 0 points decrease in error
(*.f64 c (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 2/3 (/.f64 1 t)))) (+.f64 5/6 a))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 5/6 a) (neg.f64 (*.f64 2/3 (/.f64 1 t)))))): 0 points increase in error, 0 points decrease in error
(*.f64 c (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))): 0 points increase in error, 0 points decrease in error
Simplified34.9
\[\leadsto \frac{x}{x + \color{blue}{\left(y + y \cdot \left(\left(a + \left(0.8333333333333334 - \frac{0.6666666666666666}{t}\right)\right) \cdot \left(\left(a + \left(0.8333333333333334 - \frac{0.6666666666666666}{t}\right)\right) \cdot \left(2 \cdot \left(c \cdot c\right)\right) + c \cdot 2\right)\right)\right)}}
\]
Proof
(+.f64 y (*.f64 y (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (+.f64 a (-.f64 5/6 (/.f64 (Rewrite<= metadata-eval (*.f64 2/3 1)) t))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (+.f64 a (-.f64 5/6 (Rewrite<= associate-*r/_binary64 (*.f64 2/3 (/.f64 1 t))))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 1 points increase in error, 2 points decrease in error
(+.f64 y (*.f64 y (*.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 a 5/6) (*.f64 2/3 (/.f64 1 t)))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 1 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 5/6 a)) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 2/3 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (/.f64 (Rewrite<= metadata-eval (*.f64 2/3 1)) t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (+.f64 a (-.f64 5/6 (Rewrite<= associate-*r/_binary64 (*.f64 2/3 (/.f64 1 t))))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 2 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 a 5/6) (*.f64 2/3 (/.f64 1 t)))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 1 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 5/6 a)) (*.f64 2/3 (/.f64 1 t))) (*.f64 2 (*.f64 c c))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 c 2)))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 (pow.f64 c 2)) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))) (*.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (+.f64 (*.f64 (*.f64 2 (pow.f64 c 2)) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))) (Rewrite<= *-commutative_binary64 (*.f64 2 c)))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 (*.f64 2 (pow.f64 c 2)) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))) (*.f64 (*.f64 2 c) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 2 (pow.f64 c 2)) (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (*.f64 (*.f64 2 c) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))): 33 points increase in error, 1 points decrease in error
(+.f64 y (*.f64 y (+.f64 (*.f64 (*.f64 2 (pow.f64 c 2)) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) (*.f64 (*.f64 2 c) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2)))) (*.f64 (*.f64 2 c) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (+.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 c (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 y (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 2 (*.f64 c (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))) (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 2 (*.f64 c (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))) y) (*.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y)))): 1 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 2 c) (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))) y) (*.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 2 c) (*.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) y))) (*.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y))): 1 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 (*.f64 2 c) (Rewrite<= *-commutative_binary64 (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (*.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))) (*.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (*.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 2 (pow.f64 c 2)) (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))) y))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 2 (pow.f64 c 2)) (*.f64 (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2) y))))): 5 points increase in error, 6 points decrease in error
(+.f64 y (+.f64 (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (*.f64 (*.f64 2 (pow.f64 c 2)) (Rewrite<= *-commutative_binary64 (*.f64 y (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (+.f64 (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t)))))) (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 (pow.f64 c 2) (*.f64 y (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 y (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))) (*.f64 2 (*.f64 (pow.f64 c 2) (*.f64 y (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 (*.f64 (pow.f64 c 2) (*.f64 y (pow.f64 (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))) 2)))) (+.f64 y (*.f64 2 (*.f64 c (*.f64 y (-.f64 (+.f64 5/6 a) (*.f64 2/3 (/.f64 1 t))))))))): 0 points increase in error, 0 points decrease in error