Simplified52.3
\[\leadsto \color{blue}{1 + \left(\frac{hi - x}{lo} + \frac{hi - x}{\frac{lo}{\frac{hi}{lo}}}\right)}
\]
Proof
(+.f64 1 (+.f64 (/.f64 (-.f64 hi x) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 hi (neg.f64 x))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (+.f64 hi (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 x) hi)) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (+.f64 (*.f64 -1 x) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) hi)) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (/.f64 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 x hi))) lo) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) lo))) (/.f64 (-.f64 hi x) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 hi (neg.f64 x))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 hi (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 x) hi)) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (+.f64 (*.f64 -1 x) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) hi)) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite=> distribute-lft-out--_binary64 (*.f64 -1 (-.f64 x hi))) (/.f64 lo (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 -1 (-.f64 x hi)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 lo lo) hi))))): 191 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 -1 (-.f64 x hi)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 lo 2)) hi)))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) (/.f64 (pow.f64 lo 2) hi)))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 -1 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 256 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (*.f64 (-.f64 x hi) hi)) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 -1 (-.f64 x hi)) hi)) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (/.f64 (*.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi)))) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1)) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 x hi)) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) lo)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 -1 x) lo) (/.f64 (*.f64 -1 hi) lo)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 x lo))) (/.f64 (*.f64 -1 hi) lo))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (-.f64 (*.f64 -1 (/.f64 x lo)) (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (*.f64 -1 (/.f64 x lo))) (*.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x lo)) (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1))) (*.f64 -1 (/.f64 hi lo))): 0 points increase in error, 0 points decrease in error
Simplified48.4
\[\leadsto 1 + \color{blue}{\frac{{\left(\frac{hi - x}{lo}\right)}^{4} - {\left(hi \cdot \left(\left(hi - x\right) \cdot {lo}^{-2}\right)\right)}^{4}}{{\left(\frac{hi - x}{lo}\right)}^{2} \cdot \left(1 + {\left(\frac{hi}{lo}\right)}^{2}\right)}} \cdot \frac{1}{\left(hi - x\right) \cdot \left(\frac{1}{lo} - \frac{hi}{lo \cdot lo}\right)}
\]
Proof
(/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 hi (*.f64 (-.f64 hi x) (pow.f64 lo -2))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2))) 4)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 256 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1)) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (+.f64 1 (pow.f64 (/.f64 hi lo) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1) (*.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 2) (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) 1) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1) (pow.f64 (/.f64 (-.f64 hi x) lo) 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (pow.f64 (/.f64 (-.f64 hi x) lo) 4) (pow.f64 (*.f64 (*.f64 hi (-.f64 hi x)) (pow.f64 lo -2)) 4)) (/.f64 1 (*.f64 (+.f64 (pow.f64 (/.f64 hi lo) 2) 1) (pow.f64 (/.f64 (-.f64 hi x) lo) 2))))): 0 points increase in error, 0 points decrease in error