		Search-engine friendly clone of the ACL2 documentation.

Committed-anchor-sequences

Sequences of anchors committed by validators.

We introduce an operation to collect all the anchors committed by a validator so far, and we prove properties of it.

Committed-anchors-of-next: How the sequence of committed anchors in a validator state changes (or not) for each transition.
Committed-anchors: Sequence of anchors committed by a validator.
Committed-anchors-of-commit-next-to-collect-all-anchors: Rewriting of committed-anchors after commit to collect-all-anchors on the old system state.
Committed-anchors-when-init: Initially, a validator has no committed anchors.