Not-empty-successor-predecessor-author-intersection
Non-empty intersection of successor and predecessor authors.
Here n and f in this theorem are
the n and f mentioned in max-faulty-for-total.
With reference to successor-predecessor-intersection,
here successor-vals represents
the authors of the successors of A,
while predecessor-vals represents
the authors of the predecessors of C.
If (i) the total stake of successor and predecessor authors
is bounded by n,
(ii) the total stake of the successor authors
is more than f,
and (iii) the total stake of the predecessor authors
is at least n - f,
then in order for the two sets to have no intersection
their total stake would have to be more than n,
which contradicts the first hypothesis.
So there must be at least one in the intersection.
Definitions and Theorems
Theorem: not-empty-successor-predecessor-author-intersection
(defthm not-empty-successor-predecessor-author-intersection
(implies
(and
(address-setp successor-vals)
(address-setp predecessor-vals)
(<=
(committee-members-stake (union successor-vals predecessor-vals)
commtt)
n)
(> (committee-members-stake successor-vals commtt)
f)
(>= (committee-members-stake predecessor-vals commtt)
(- n f)))
(not (emptyp (intersect successor-vals predecessor-vals)))))
