		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Same-committees-p-implied

Proof of the invariant from other invariants.

This is the proof of our invariant, from the other two invariants. The rewrite rules enabled in the hints take care of everything; also see the observation in same-active-committees-when-nofork about the particular form of that rewrite rule.

Definitions and Theorems

Theorem: same-committees-p-implied

(defthm same-committees-p-implied
  (implies (and (nonforking-blockchains-p systate)
                (ordered-blockchain-p systate))
           (same-committees-p systate)))