  In other words, as long as we can nonvacuously close the stage we are working on under an applicable default, we do so; otherwise, we do nothing. A theorem of Reiter’s says that, under these circumstances: 