		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Same-active-committees-longer-shorter

The longer and shorter blockchains calculate the same active committees, when they both do.

So far we have dealt with bonded committees, because those have a more direct correspondence with the rounds of the blocks. But the validators really use active committees.

Transferring the proof to active committees is easy, because those are defined in terms of bonded committees. The theorem formulation is the same.

Definitions and Theorems

Theorem: same-active-committees-longer-shorter

(defthm same-active-committees-longer-shorter
  (implies (and (blocks-orderedp blocks2)
                (< (len blocks1) (len blocks2))
                (equal blocks1
                       (nthcdr (- (len blocks2) (len blocks1))
                               blocks2))
                (active-committee-at-round round blocks1)
                (active-committee-at-round round blocks2))
           (equal (active-committee-at-round round blocks1)
                  (active-committee-at-round round blocks2))))