		Search-engine friendly clone of the ACL2 documentation.

Omni-paths-def-and-implied

Omni-paths-p-implied

Proof of the invariant from other invariants.

The key theorem that we use is dag-omni-paths-p-holds. We use already proved invariant to establish its hypotheses.

Definitions and Theorems

Theorem: omni-paths-p-implied

(defthm omni-paths-p-implied
  (implies (and (backward-closed-p systate)
                (signer-quorum-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (dag-previous-quorum-p systate)
                (last-anchor-voters-p systate))
           (omni-paths-p systate)))