		Search-engine friendly clone of the ACL2 documentation.

Simultaneous-induction

Invariants-of-events-next

Preservation of a number of invariants by any sequence of zero or more events.

This is proved by simultaneous induction, involving all of the invariants.

A critical assumption is fault tolerance: all the committees that arise during the execution must be fault-tolerant.

Definitions and Theorems

Theorem: invariants-of-events-next

(defthm invariants-of-events-next
 (implies
      (and (all-system-committees-fault-tolerant-p systate events)
           (backward-closed-p systate)
           (last-blockchain-round-p systate)
           (ordered-even-p systate)
           (signed-previous-quorum-p systate)
           (no-self-endorsed-p systate)
           (signer-records-p systate)
           (unequivocal-signed-certs-p systate)
           (signer-quorum-p systate)
           (unequivocal-dags-p systate)
           (nonforking-blockchains-p systate)
           (same-committees-p systate)
           (dag-previous-quorum-p systate)
           (last-anchor-present-p systate)
           (last-anchor-voters-p systate)
           (omni-paths-p systate)
           (nonforking-anchors-p systate)
           (committed-redundant-p systate)
           (blockchain-redundant-p systate)
           (events-possiblep events systate))
      (and (backward-closed-p (events-next events systate))
           (last-blockchain-round-p (events-next events systate))
           (ordered-even-p (events-next events systate))
           (signed-previous-quorum-p (events-next events systate))
           (no-self-endorsed-p (events-next events systate))
           (signer-records-p (events-next events systate))
           (unequivocal-signed-certs-p (events-next events systate))
           (signer-quorum-p (events-next events systate))
           (unequivocal-dags-p (events-next events systate))
           (nonforking-blockchains-p (events-next events systate))
           (same-committees-p (events-next events systate))
           (dag-previous-quorum-p (events-next events systate))
           (last-anchor-present-p (events-next events systate))
           (last-anchor-voters-p (events-next events systate))
           (omni-paths-p (events-next events systate))
           (nonforking-anchors-p (events-next events systate))
           (committed-redundant-p (events-next events systate))
           (blockchain-redundant-p (events-next events systate)))))