		Search-engine friendly clone of the ACL2 documentation.

Successor-predecessor-intersection

Successors+predecessors-same-round

Successors and predecessors have all the same round.

This is used to establish a hypothesis of not-empty-successor-predecessor-intersection. If (again with reference to successor-predecessor-intersection) A and C are two rounds apart, then the successors of A and the predecessors of C are all in the round between those two rounds.

Definitions and Theorems

Theorem: successors+predecessors-same-round

(defthm successors+predecessors-same-round
 (implies
   (and (certificate-setp dag1)
        (certificate-setp dag2)
        (equal (certificate->round cert2)
               (+ 2 (certificate->round cert1))))
   (<= (cardinality
            (cert-set->round-set (union (successors cert1 dag1)
                                        (predecessors cert2 dag2))))
       1))
 :rule-classes :linear)