Damian's comments encouraged me to take another look at the 754 spec for augmented arithmetic. As I read it, in the case of overflow, both results are the same infinity. That means, in this case, as with an exact zero result, |x.h| = |x.t}. But I still suppose that the algorithm I proposed never yields |x.h| < |x.t|.