|
|
|---|
|
|
|
|---|
Invariant that the last committed anchor in a validator is also present and reachable from later certificates in any validator: proof that it holds in every reachable state.
This completes omni-paths-def-and-implied by showing that the invariant holds in every reachable state.