|
|
|---|
|
|
|
|---|
Last anchor committed by a validator: how events change the result.
As mentioned in last-anchor-def-and-init, the theorems about the changes to the result of this operation are separate from its definition and its proof of initial result. The reason is that the theorems about changes under events need other theorems that depend on the definition, which in turn depend on the definition of last-anchor: the theorems in question are in last-anchor-present.