Initial program 0.1
\[\cosh x \cdot \frac{\sin y}{y}
\]
Simplified0.3
\[\leadsto \color{blue}{\sin y \cdot \frac{\cosh x}{y}}
\]
Proof
(*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (sin.f64 y) (cosh.f64 x)) y)): 8 points increase in error, 43 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (sin.f64 y) y) (cosh.f64 x))): 1 points increase in error, 1 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (cosh.f64 x) (/.f64 (sin.f64 y) y))): 0 points increase in error, 0 points decrease in error
Applied egg-rr29.2
\[\leadsto \color{blue}{\left(1 + \sin y \cdot \frac{\cosh x}{y}\right) - 1}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{\sin y}{\frac{y}{\cosh x}}}
\]
Proof
(/.f64 (sin.f64 y) (/.f64 y (cosh.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sin.f64 y) (cosh.f64 x)) y)): 2 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y))): 43 points increase in error, 8 points decrease in error
(Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y)) 0)): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y)) (Rewrite<= metadata-eval (-.f64 1 1))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y)) 1) 1)): 133 points increase in error, 20 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (sin.f64 y) (/.f64 (cosh.f64 x) y)))) 1): 0 points increase in error, 0 points decrease in error
Final simplification0.2
\[\leadsto \frac{\sin y}{\frac{y}{\cosh x}}
\]