When a state change is made, we implicitly check first the invariants of all updated objects (in parallel), then all unupdated non-\claim objects (in parallel), then all \claims (in parallel). However, in some cases, such an ordering doesn't work with only first-order deduction available. This particularly occurs when you try to write an object invariant using model fields (i.e., state expressions) rather than ghost fields. For example, if you have a tree of objects, and the invariant of each depends on the invariants of its children, and there is an update onboundedly far down the tree, you can't prove that your invariant is preserved. (This is reflected in a failed admissibility proof.) Note that you cannot get around the problem using recursive pure functions,because their specs don't tell you anything about their behavior when the state is not \full_stop().

One way to handle this is to extend termination measures to objects, so that instead of all invariant checks proceeding in parallel, they proceed in order of the measure on objects. (I'm not sure whether this measure should be based on the prestate or poststate measure; the former has the advantage that you could use recursive pure functions to define the measure function, since the prestate is already assumed to be \full_stop.) In other words, when proving admissibility of an object invariant, you get a free assumption of the (2-state) invariants of all objects of lesser measure.