		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Trim-blocks-for-round-no-change

Trimming a blockchain to a round after the last one causes no change.

Note that we use blocks-last-round, so we allow the blockchain to be empty, in which case we consider its last round to be 0. Given the way trim-blocks-for-round is defined, if the round is after the last one, no block is removed.

With reference to the explanation in same-committees-def-and-implied, this theorem will be used to show that trimming the shorter blockchain does not change it.

Definitions and Theorems

Theorem: trim-blocks-for-round-no-change

(defthm trim-blocks-for-round-no-change
  (implies (> (pos-fix round)
              (blocks-last-round blocks))
           (equal (trim-blocks-for-round round blocks)
                  (block-list-fix blocks))))