The replicas holding a slot in this counter. On the mutator path that is exactly the replicas that have ever incremented, since inc must be positive — but of can seed a slot at 0, and such a replica is listed. The set is "has a slot", not "has a positive count"; take count if you need the latter.