		Search-engine friendly clone of the ACL2 documentation.

Successor-predecessor-intersection

Not-empty-successor-predecessor-intersection

Non-empty intersection of successors and predecessors

This lifts not-empty-successor-predecessor-author-intersection from the authors, over which stake is calculated, to the certificates, which are the ones whose non-empty intersection we need to show. With reference to successor-predecessor-intersection, here cert1 is A and cert2 is C; we show that the successors of A and the predecessors of C have a non-empty intersection. The key theorem used in the proof is certs-same-round-unequiv-intersect-when-authors-intersect.

Definitions and Theorems

Theorem: not-empty-successor-predecessor-intersection

(defthm not-empty-successor-predecessor-intersection
 (implies
      (and (certificate-setp dag1)
           (certificate-setp dag2)
           (certificate-set-unequivocalp dag1)
           (certificate-set-unequivocalp dag2)
           (certificate-sets-unequivocalp dag1 dag2)
           (equal (certificate->round cert2)
                  (+ 2 (certificate->round cert1)))
           (subset (cert-set->author-set (successors cert1 dag1))
                   (committee-members commtt))
           (subset (cert-set->author-set (predecessors cert2 dag2))
                   (committee-members commtt))
           (> (committee-members-stake
                   (cert-set->author-set (successors cert1 dag1))
                   commtt)
              (committee-max-faulty-stake commtt))
           (>= (committee-members-stake
                    (cert-set->author-set (predecessors cert2 dag2))
                    commtt)
               (committee-quorum-stake commtt)))
      (not (emptyp (intersect (successors cert1 dag1)
                              (predecessors cert2 dag2))))))