		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Dag-omni-paths-p-holds

Proof that dag-omni-paths-p holds.

This is the proof of our desired property. We rewrite dag-omni-paths-p to its alternative definition dag-omni-paths-rounds-p, we expand the latter, and we use dag-omni-paths-round-p-holds to prove that dag-omni-paths-round-p holds on the generic witness.

Definitions and Theorems

Theorem: dag-omni-paths-p-holds

(defthm dag-omni-paths-p-holds
 (implies
  (and
   (certificate-setp dag1)
   (certificate-setp dag2)
   (certificate-set-unequivocalp dag1)
   (certificate-set-unequivocalp dag2)
   (certificate-sets-unequivocalp dag1 dag2)
   (dag-closedp dag1)
   (dag-closedp dag2)
   (dag-has-committees-p dag1 blockchain1)
   (dag-has-committees-p dag2 blockchain2)
   (dag-in-committees-p dag1 blockchain1)
   (dag-in-committees-p dag2 blockchain2)
   (same-active-committees-p blockchain1 blockchain2)
   (dag-predecessor-quorum-p dag2 blockchain2)
   (in cert dag1)
   (> (committee-members-stake
           (cert-set->author-set (successors cert dag1))
           (active-committee-at-round (1+ (certificate->round cert))
                                      blockchain1))
      (committee-max-faulty-stake
           (active-committee-at-round (1+ (certificate->round cert))
                                      blockchain1))))
  (dag-omni-paths-p cert dag2)))