Simplified38.7
\[\leadsto \color{blue}{\frac{2}{\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \left(\tan k \cdot \left({\left(\frac{k}{t}\right)}^{2} + 0\right)\right)}}
\]
Proof
(/.f64 2 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (*.f64 (tan.f64 k) (+.f64 (pow.f64 (/.f64 k t) 2) 0)))): 0 points increase in error, 0 points decrease in error
(/.f64 2 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (*.f64 (tan.f64 k) (+.f64 (pow.f64 (/.f64 k t) 2) (Rewrite<= metadata-eval (-.f64 1 1)))))): 0 points increase in error, 0 points decrease in error
(/.f64 2 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (*.f64 (tan.f64 k) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (pow.f64 (/.f64 k t) 2) 1) 1))))): 27 points increase in error, 0 points decrease in error
(/.f64 2 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (*.f64 (tan.f64 k) (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (pow.f64 (/.f64 k t) 2))) 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 2 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 (tan.f64 k) (-.f64 (+.f64 1 (pow.f64 (/.f64 k t) 2)) 1)) 0)))): 0 points increase in error, 0 points decrease in error
(/.f64 2 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (*.f64 (tan.f64 k) (-.f64 (+.f64 1 (pow.f64 (/.f64 k t) 2)) 1))) (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) 0)))): 39 points increase in error, 0 points decrease in error
(/.f64 2 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (tan.f64 k)) (-.f64 (+.f64 1 (pow.f64 (/.f64 k t) 2)) 1))) (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) 0))): 1 points increase in error, 1 points decrease in error
(/.f64 2 (+.f64 (*.f64 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (tan.f64 k)) (-.f64 (+.f64 1 (pow.f64 (/.f64 k t) 2)) 1)) (Rewrite=> mul0-rgt_binary64 0))): 0 points increase in error, 39 points decrease in error
(/.f64 2 (Rewrite=> +-rgt-identity_binary64 (*.f64 (*.f64 (*.f64 (/.f64 (pow.f64 t 3) (*.f64 l l)) (sin.f64 k)) (tan.f64 k)) (-.f64 (+.f64 1 (pow.f64 (/.f64 k t) 2)) 1)))): 0 points increase in error, 0 points decrease in error
Simplified1.0
\[\leadsto 2 \cdot \color{blue}{\left(\frac{\ell}{k} \cdot \frac{\cos k \cdot \frac{\ell}{k}}{t \cdot {\sin k}^{2}}\right)}
\]
Proof
(*.f64 (/.f64 l k) (/.f64 (*.f64 (cos.f64 k) (/.f64 l k)) (*.f64 t (pow.f64 (sin.f64 k) 2)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 l k) (cos.f64 k))) (*.f64 t (pow.f64 (sin.f64 k) 2)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 l (cos.f64 k)) k)) (*.f64 t (pow.f64 (sin.f64 k) 2)))): 10 points increase in error, 13 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 k) l)) k) (*.f64 t (pow.f64 (sin.f64 k) 2)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (cos.f64 k) (/.f64 k l))) (*.f64 t (pow.f64 (sin.f64 k) 2)))): 12 points increase in error, 21 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (sin.f64 k) 2) t)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (Rewrite<= associate-/r*_binary64 (/.f64 (cos.f64 k) (*.f64 (/.f64 k l) (*.f64 (pow.f64 (sin.f64 k) 2) t))))): 26 points increase in error, 19 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (cos.f64 k) (*.f64 (/.f64 k l) (Rewrite=> *-commutative_binary64 (*.f64 t (pow.f64 (sin.f64 k) 2)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (cos.f64 k) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 k l) t) (pow.f64 (sin.f64 k) 2))))): 18 points increase in error, 32 points decrease in error
(*.f64 (/.f64 l k) (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (cos.f64 k) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2)))): 15 points increase in error, 14 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (Rewrite<= unpow1_binary64 (pow.f64 (cos.f64 k) 1)) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (cos.f64 k) (/.f64 1 2)) (pow.f64 (cos.f64 k) (/.f64 1 2)))) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 104 points increase in error, 10 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (*.f64 (pow.f64 (cos.f64 k) (Rewrite=> metadata-eval 1/2)) (pow.f64 (cos.f64 k) (/.f64 1 2))) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (*.f64 (Rewrite=> unpow1/2_binary64 (sqrt.f64 (cos.f64 k))) (pow.f64 (cos.f64 k) (/.f64 1 2))) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (*.f64 (sqrt.f64 (cos.f64 k)) (pow.f64 (cos.f64 k) (Rewrite=> metadata-eval 1/2))) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (/.f64 (*.f64 (sqrt.f64 (cos.f64 k)) (Rewrite=> unpow1/2_binary64 (sqrt.f64 (cos.f64 k)))) (*.f64 (/.f64 k l) t)) (pow.f64 (sin.f64 k) 2))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (*.f64 (/.f64 k l) t)) (sqrt.f64 (cos.f64 k)))) (pow.f64 (sin.f64 k) 2))): 7 points increase in error, 6 points decrease in error
(*.f64 (/.f64 l k) (/.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (*.f64 (/.f64 k l) t)) (sqrt.f64 (cos.f64 k))) (Rewrite=> unpow2_binary64 (*.f64 (sin.f64 k) (sin.f64 k))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (*.f64 (/.f64 k l) t)) (sin.f64 k)) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k))))): 18 points increase in error, 21 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (sqrt.f64 (cos.f64 k)) (*.f64 (*.f64 (/.f64 k l) t) (sin.f64 k)))) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 18 points increase in error, 19 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (*.f64 (/.f64 k l) t))) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 17 points increase in error, 10 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (/.f64 k l)) t)) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 13 points increase in error, 12 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (/.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) k) l)) t) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 22 points increase in error, 10 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) l) k)) t) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 12 points increase in error, 22 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (/.f64 l k))) t) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 15 points increase in error, 9 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 l k) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))) t) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (/.f64 l k) t) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))): 13 points increase in error, 19 points decrease in error
(*.f64 (/.f64 l k) (Rewrite=> associate-*l*_binary64 (*.f64 (/.f64 (/.f64 l k) t) (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)))))): 27 points increase in error, 12 points decrease in error
(*.f64 (/.f64 l k) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k))) (/.f64 (/.f64 l k) t)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 l k) (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k))) (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (/.f64 (/.f64 l k) t)) (sqrt.f64 (/.f64 (/.f64 l k) t)))))): 67 points increase in error, 7 points decrease in error
(*.f64 (/.f64 l k) (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t))) (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t)))))): 5 points increase in error, 15 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 l k) (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t)))) (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t))))): 6 points increase in error, 10 points decrease in error
(*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t))) (/.f64 l k))) (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t))) (*.f64 (*.f64 (/.f64 (sqrt.f64 (cos.f64 k)) (sin.f64 k)) (sqrt.f64 (/.f64 (/.f64 l k) t))) (/.f64 l k)))): 0 points increase in error, 0 points decrease in error