		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Same-active-committees-when-nofork

Two non-forking blockchains calculate the same active committees, when they both do.

While same-active-committees-longer-shorter takes care of the interesting case of our overall proof, we need a proof for all cases, which we do here, using lists-noforkp, whose expansion splits into three cases. The case of equal blockchains is trivial. The other two cases are symmetric, and handled by two firings of same-active-committees-longer-shorter, one with blocks1 and blocks2 as in that theorem, and one with their roles swapped.

Instead of (equal A B), we phrase this theorem as (equal (equal A B) t) so it can fire as a rewrite rule in the main theorem same-committees-p-implied.

Definitions and Theorems

Theorem: same-active-committees-when-nofork

(defthm same-active-committees-when-nofork
  (implies (and (lists-noforkp blocks1 blocks2)
                (blocks-orderedp blocks1)
                (blocks-orderedp blocks2)
                (active-committee-at-round round blocks1)
                (active-committee-at-round round blocks2))
           (equal (equal (active-committee-at-round round blocks1)
                         (active-committee-at-round round blocks2))
                  t)))