		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Path-from-common-to-cert1-in-dag2

There is a path in dag2 from the common certificate in the intersection to cert1 in dag1, which is also in dag2.

Since the common certificate is a successor of cert1 in dag1, there is a path in dag1 from the common certificate to cert1. But since the common certificate is also in dag2, and the two DAGs are (individually and mutually) unequivocal, the result of path-to-author+round applied to the common certificate (as source) must be the same in the two DAGs, namely cert1. So we have that cert1 is also in dag2 besides dag1.

Definitions and Theorems

Theorem: path-from-common-to-cert1-in-dag2

(defthm path-from-common-to-cert1-in-dag2
 (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)
   (in cert1 dag1)
   (in cert2 dag2)
   (equal (certificate->round cert2)
          (+ 2 (certificate->round cert1)))
   (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)
   (>
     (committee-members-stake
          (cert-set->author-set (successors cert1 dag1))
          (active-committee-at-round (1+ (certificate->round cert1))
                                     blockchain1))
     (committee-max-faulty-stake
          (active-committee-at-round (1+ (certificate->round cert1))
                                     blockchain1))))
  (and
      (equal (path-to-author+round
                  (pick-successor/predecessor dag1 dag2 cert1 cert2)
                  (certificate->author cert1)
                  (certificate->round cert1)
                  dag2)
             cert1)
      (in cert1 dag2))))