|
|
|---|
|
|
|
|---|
Certificates signed by validators.
All the certificates in the system are associated to some validator, as formalized in associated-certificates. As proved in same-associated-certificates, all the validators have the same associated certificates, so all the certificates in the system can be obtained as the certificates associated to any validator in the system.
We define an operation to return all the certificates in the system signed by a given validator. We prove theorems about its initial value, and about how its value changes in response to events.