Initial program 63.1
\[\frac{x - \sin x}{x - \tan x}
\]
Simplified63.1
\[\leadsto \color{blue}{\frac{\sin x - x}{\tan x - x}}
\]
Proof
(/.f64 (-.f64 (sin.f64 x) x) (-.f64 (tan.f64 x) x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 (sin.f64 x) x) (-.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (-.f64 (sin.f64 x) x) (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 (sin.f64 x) x)) (*.f64 -1 (-.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (sin.f64 x) x))) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (sin.f64 x) x))) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (sin.f64 x)) x)) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (sin.f64 x))) x) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 (sin.f64 x)))) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 x (sin.f64 x))) (*.f64 -1 (-.f64 (tan.f64 x) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (tan.f64 x)) x))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (tan.f64 x))) x)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (Rewrite<= +-commutative_binary64 (+.f64 x (neg.f64 (tan.f64 x))))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (sin.f64 x)) (Rewrite<= sub-neg_binary64 (-.f64 x (tan.f64 x)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in x around 0 0.0
\[\leadsto \color{blue}{\left(0.225 \cdot {x}^{2} + \left(-0.009642857142857142 \cdot {x}^{4} + 0.00024107142857142857 \cdot {x}^{6}\right)\right) - 0.5}
\]
Applied egg-rr0.0
\[\leadsto \left(\color{blue}{\left(0 + x \cdot \left(x \cdot 0.225\right)\right)} + \left(-0.009642857142857142 \cdot {x}^{4} + 0.00024107142857142857 \cdot {x}^{6}\right)\right) - 0.5
\]
Simplified0.0
\[\leadsto \left(\color{blue}{\left(x \cdot x\right) \cdot 0.225} + \left(-0.009642857142857142 \cdot {x}^{4} + 0.00024107142857142857 \cdot {x}^{6}\right)\right) - 0.5
\]
Proof
(*.f64 (*.f64 x x) 9/40): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 x (*.f64 x 9/40))): 18 points increase in error, 20 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 x (*.f64 x 9/40)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.0
\[\leadsto \left(\left(x \cdot x\right) \cdot 0.225 + \color{blue}{\left(e^{\mathsf{log1p}\left(\mathsf{fma}\left(-0.009642857142857142, {x}^{4}, 0.00024107142857142857 \cdot {x}^{6}\right)\right)} - 1\right)}\right) - 0.5
\]
Simplified0.0
\[\leadsto \left(\left(x \cdot x\right) \cdot 0.225 + \color{blue}{{x}^{4} \cdot \mathsf{fma}\left(0.00024107142857142857, x \cdot x, -0.009642857142857142\right)}\right) - 0.5
\]
Proof
(*.f64 (pow.f64 x 4) (fma.f64 27/112000 (*.f64 x x) -27/2800)): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 x 4) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 27/112000 (*.f64 x x)) -27/2800))): 1 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 x 4) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 x x) 27/112000)) -27/2800)): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (pow.f64 x 4) (*.f64 (*.f64 x x) 27/112000)) (*.f64 (pow.f64 x 4) -27/2800))): 0 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (pow.f64 x 4) (*.f64 (*.f64 x x) 27/112000)) (Rewrite<= *-commutative_binary64 (*.f64 -27/2800 (pow.f64 x 4)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 (pow.f64 x 4) (*.f64 x x)) 27/112000)) (*.f64 -27/2800 (pow.f64 x 4))): 5 points increase in error, 6 points decrease in error
(+.f64 (*.f64 (*.f64 (pow.f64 x (Rewrite<= metadata-eval (+.f64 3 1))) (*.f64 x x)) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (*.f64 (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 x 3) x)) (*.f64 x x)) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 2 points increase in error, 5 points decrease in error
(+.f64 (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 x 3) (*.f64 x (*.f64 x x)))) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 6 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (*.f64 (pow.f64 x 3) (Rewrite<= cube-mult_binary64 (pow.f64 x 3))) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 1 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 x (*.f64 2 3))) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 3 points increase in error, 8 points decrease in error
(+.f64 (*.f64 (pow.f64 x (Rewrite=> metadata-eval 6)) 27/112000) (*.f64 -27/2800 (pow.f64 x 4))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 27/112000 (pow.f64 x 6))) (*.f64 -27/2800 (pow.f64 x 4))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -27/2800 (pow.f64 x 4)) (*.f64 27/112000 (pow.f64 x 6)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-udef_binary64 (fma.f64 -27/2800 (pow.f64 x 4) (*.f64 27/112000 (pow.f64 x 6)))): 1 points increase in error, 1 points decrease in error
(Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (fma.f64 -27/2800 (pow.f64 x 4) (*.f64 27/112000 (pow.f64 x 6)))))): 10 points increase in error, 9 points decrease in error
(Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (fma.f64 -27/2800 (pow.f64 x 4) (*.f64 27/112000 (pow.f64 x 6))))) 1)): 38 points increase in error, 4 points decrease in error