		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Trim-blocks-for-round-of-append-yields-first

Trimming an extended blockchain to the smallest round of the extension yields the shorter blockchain.

This is used to show that trimming the longer blockchain yields the shorter blockchain. We use the formulation with append, where blocks2 is the shorter blockchain, blocks1 is the extension, and the append is the longer blockchain. The cutoff round is the smallest one of the extension. Here we need to assume that block rounds are ordered (in the longer blockchain, which implies that they are also ordered in the extension and in the smaller blockchain).

Definitions and Theorems

Theorem: trim-blocks-for-round-of-append-yields-first

(defthm trim-blocks-for-round-of-append-yields-first
 (implies
   (and (blocks-orderedp (append blocks1 blocks2))
        (consp blocks1))
   (equal (trim-blocks-for-round (block->round (car (last blocks1)))
                                 (append blocks1 blocks2))
          (block-list-fix blocks2))))