Simplified20.8
\[\leadsto \color{blue}{\frac{\cos \left(2 \cdot x\right)}{x \cdot \left(x \cdot \left(\left(c \cdot s\right) \cdot \left(c \cdot s\right)\right)\right)}}
\]
Proof
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (*.f64 x (*.f64 c s)) (*.f64 x (*.f64 c s)))): 0 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 x x) (*.f64 (*.f64 c s) (*.f64 c s))))): 0 points increase in error, 9 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (*.f64 x x) (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 s s))))): 7 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (*.f64 x x) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 s s)))): 2 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (*.f64 x x) (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 s 2))))): 1 points increase in error, 8 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 s 2)) (*.f64 x x)))): 8 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 c 2) (*.f64 (pow.f64 s 2) (*.f64 x x))))): 0 points increase in error, 9 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (pow.f64 c 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 s 2) x) x)))): 9 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (*.f64 (pow.f64 c 2) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 x (pow.f64 s 2))) x))): 0 points increase in error, 9 points decrease in error
Simplified3.5
\[\leadsto \color{blue}{\frac{\cos \left(x + x\right)}{{\left(c \cdot \left(s \cdot x\right)\right)}^{2}}}
\]
Proof
(/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (*.f64 c (*.f64 s x)) 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c s) x)) 2)): 0 points increase in error, 17 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 x (*.f64 c s))) 2)): 8 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (Rewrite=> unpow2_binary64 (*.f64 (*.f64 x (*.f64 c s)) (*.f64 x (*.f64 c s))))): 10 points increase in error, 1 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 x x) (*.f64 (*.f64 c s) (*.f64 c s))))): 4 points increase in error, 14 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (*.f64 (*.f64 c s) (*.f64 c s)))): 14 points increase in error, 1 points decrease in error
(/.f64 (cos.f64 (+.f64 x x)) (*.f64 (pow.f64 x 2) (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 c s) 2)))): 0 points increase in error, 17 points decrease in error
(Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (*.f64 c s) 2)) (pow.f64 x 2))): 18 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (*.f64 c s) 2)))) (pow.f64 x 2)): 0 points increase in error, 18 points decrease in error
(/.f64 (Rewrite=> *-lft-identity_binary64 (/.f64 (cos.f64 (+.f64 x x)) (pow.f64 (*.f64 c s) 2))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (cos.f64 (+.f64 x x)) (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c s) (*.f64 c s)))) (pow.f64 x 2)): 14 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (cos.f64 (+.f64 x x)) (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 s s)))) (pow.f64 x 2)): 4 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (cos.f64 (+.f64 x x)) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 s s))) (pow.f64 x 2)): 4 points increase in error, 11 points decrease in error
(/.f64 (/.f64 (cos.f64 (+.f64 x x)) (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 s 2)))) (pow.f64 x 2)): 0 points increase in error, 15 points decrease in error
(/.f64 (/.f64 (cos.f64 (+.f64 x x)) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 s 2) (pow.f64 c 2)))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (cos.f64 (+.f64 x x)) (*.f64 (*.f64 (pow.f64 s 2) (pow.f64 c 2)) (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (Rewrite=> count-2_binary64 (*.f64 2 x))) (*.f64 (*.f64 (pow.f64 s 2) (pow.f64 c 2)) (pow.f64 x 2))): 14 points increase in error, 0 points decrease in error
(/.f64 (cos.f64 (*.f64 2 x)) (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 s 2) (*.f64 (pow.f64 c 2) (pow.f64 x 2))))): 4 points increase in error, 0 points decrease in error