|
|
|---|
|
|
|
|---|
Invariant that the last committed anchor in a validator is also present and reachable from later certificates in any validator: definition, and proof that it is implied by other invariants.
This lifts dag-omni-paths to the system level,
and ties it with the invariant that
the last committed anchor of each validator, if present,
has more than
We define the invariant, and we prove that it is implied by other invariants. Elsewhere we prove that this invariant holds in every reachable state.