Simplified7.3
\[\leadsto \color{blue}{x \cdot \left({z}^{y} \cdot \frac{{a}^{t}}{y \cdot \left(e^{b} \cdot a\right)}\right)}
\]
Proof
(*.f64 x (*.f64 (pow.f64 z y) (/.f64 (pow.f64 a t) (*.f64 y (*.f64 (exp.f64 b) a))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 z) y))) (/.f64 (pow.f64 a t) (*.f64 y (*.f64 (exp.f64 b) a))))): 1 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 y (log.f64 z)))) (/.f64 (pow.f64 a t) (*.f64 y (*.f64 (exp.f64 b) a))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (Rewrite<= exp-to-pow_binary64 (exp.f64 (*.f64 (log.f64 a) t))) (*.f64 y (*.f64 (exp.f64 b) a))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (*.f64 (exp.f64 b) (Rewrite<= rem-exp-log_binary64 (exp.f64 (log.f64 a)))))))): 35 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (exp.f64 b) 1)) (exp.f64 (log.f64 a))))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (Rewrite<= associate-/r/_binary64 (/.f64 (exp.f64 b) (/.f64 1 (exp.f64 (log.f64 a))))))))): 3 points increase in error, 2 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (/.f64 (exp.f64 b) (Rewrite<= exp-neg_binary64 (exp.f64 (neg.f64 (log.f64 a))))))))): 3 points increase in error, 2 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (/.f64 (exp.f64 b) (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 a))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (*.f64 y (/.f64 (exp.f64 b) (exp.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) (log.f64 a)))))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (exp.f64 (*.f64 (log.f64 a) t)) (/.f64 (exp.f64 b) (exp.f64 (*.f64 (neg.f64 1) (log.f64 a))))) y)))): 8 points increase in error, 7 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (exp.f64 (*.f64 (log.f64 a) t)) (exp.f64 (*.f64 (neg.f64 1) (log.f64 a)))) (exp.f64 b))) y))): 2 points increase in error, 3 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (/.f64 (*.f64 (exp.f64 (Rewrite=> *-commutative_binary64 (*.f64 t (log.f64 a)))) (exp.f64 (*.f64 (neg.f64 1) (log.f64 a)))) (exp.f64 b)) y))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (/.f64 (Rewrite<= exp-sum_binary64 (exp.f64 (+.f64 (*.f64 t (log.f64 a)) (*.f64 (neg.f64 1) (log.f64 a))))) (exp.f64 b)) y))): 0 points increase in error, 1 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (/.f64 (exp.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (log.f64 a) (+.f64 t (neg.f64 1))))) (exp.f64 b)) y))): 1 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (/.f64 (exp.f64 (*.f64 (log.f64 a) (Rewrite<= sub-neg_binary64 (-.f64 t 1)))) (exp.f64 b)) y))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (/.f64 (exp.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 t 1) (log.f64 a)))) (exp.f64 b)) y))): 0 points increase in error, 0 points decrease in error
(*.f64 x (*.f64 (exp.f64 (*.f64 y (log.f64 z))) (/.f64 (Rewrite<= exp-diff_binary64 (exp.f64 (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b))) y))): 1 points increase in error, 29 points decrease in error
(*.f64 x (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (exp.f64 (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b)) y) (exp.f64 (*.f64 y (log.f64 z)))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= associate-/r/_binary64 (/.f64 (exp.f64 (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b)) (/.f64 y (exp.f64 (*.f64 y (log.f64 z))))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (exp.f64 (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b)) (exp.f64 (*.f64 y (log.f64 z)))) y))): 1 points increase in error, 0 points decrease in error
(*.f64 x (/.f64 (Rewrite<= exp-sum_binary64 (exp.f64 (+.f64 (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b) (*.f64 y (log.f64 z))))) y)): 3 points increase in error, 37 points decrease in error
(*.f64 x (/.f64 (exp.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y (log.f64 z)) (-.f64 (*.f64 (-.f64 t 1) (log.f64 a)) b)))) y)): 0 points increase in error, 0 points decrease in error
(*.f64 x (/.f64 (exp.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t 1) (log.f64 a))) b))) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x (exp.f64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t 1) (log.f64 a))) b))) y)): 18 points increase in error, 12 points decrease in error