		Search-engine friendly clone of the ACL2 documentation.

Dag-omni-paths

Path-from-cert2-to-cert1-in-dag2

There is a path in dag2 from cert2 to cert1.

This is obtained by composing the path proved in path-from-common-to-cert1-in-dag2, from the common certificate to cert1, with the path from cert2 to the common certificate. The latter path exists because the common certificate is a predecessor of cert2.

Definitions and Theorems

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

(defthm path-from-cert2-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))))
  (equal (path-to-author+round cert2 (certificate->author cert1)
                               (certificate->round cert1)
                               dag2)
         cert1)))