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
Theorem:
(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))))))