		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-voters-def-and-init-and-next

Last-anchor-voters-p

Definition of the invariant: for each correct validator, if the last committed round is not 0, the last committed anchor has at least f+1 successors, where f is the maximum number of faulty validators in the committee active at the round just after the last committed one.

Definitions and Theorems

Theorem: last-anchor-voters-p-necc

(defthm last-anchor-voters-p-necc
  (implies (last-anchor-voters-p systate)
           (implies (in val (correct-addresses systate))
                    (validator-last-anchor-voters-p
                         (get-validator-state val systate)))))

Theorem: booleanp-of-last-anchor-voters-p

(defthm booleanp-of-last-anchor-voters-p
  (b* ((yes/no (last-anchor-voters-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: last-anchor-voters-p-of-system-state-fix-systate

(defthm last-anchor-voters-p-of-system-state-fix-systate
  (equal (last-anchor-voters-p (system-state-fix systate))
         (last-anchor-voters-p systate)))

Theorem: last-anchor-voters-p-system-state-equiv-congruence-on-systate

(defthm
      last-anchor-voters-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (last-anchor-voters-p systate)
                  (last-anchor-voters-p systate-equiv)))
  :rule-classes :congruence)