|
|
|---|
|
|
|
|---|
Last anchor committed by a validator: definition and initial result.
We introduce an operation, and theorems about it, to obtain the last anchor committed by a validator.
We prove theorems expressing the initial result of this operation.
Elsewhere, we prove how the events change the result. We separate that because it needs theorems that depend on the definition of the operation.