|
|
|---|
|
|
|
|---|
Invariant that each certificate in a DAG has references to previous certificates that form a non-zero quorum in the committee for the previous round, unless the round is 1, in which case there are no references to previous certificates: proof that it holds in every reachable state.
This completes previous-quorum-def-and-init-and-next by showing that the invariant holds in every reachable state.