Simplified51.9
\[\leadsto \color{blue}{1 + \frac{x - hi}{lo} \cdot \left(-1 - \frac{hi}{lo}\right)}
\]
Proof
(+.f64 1 (*.f64 (/.f64 (-.f64 x hi) lo) (-.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo))))): 13 points increase in error, 13 points decrease in error
(+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))))): 256 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 x hi) hi)) (*.f64 lo lo)))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (neg.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 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) (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x lo) (/.f64 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<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 x lo)) (*.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