		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Trim-blocks-for-round-of-shorter

Result of trimming the shorter blockchain.

This is the counterpart of trim-blocks-for-round-of-longer, but for the shorter blockchain. The result is the same, i.e. the shorter blockchain itself. The core theorem is trim-blocks-for-round-no-change, which is expressed in terms of append, so again we use the list equivalence theorem. We also need to appeal to the theorem that, in an ordered (append blocks1 blocks2), the oldest round of blocks1 is greater than the newest round of blocks2, where we instantiate blocks1 and blocks2 with the appropriate extension and shorter block, as blocks1 and blocks2 have a different meaning in the theorem that we prove here. The appeal to that theorem is necessary to relieve the hypothesis of trim-blocks-for-round-no-change.

The theorem says that the trimming of the shorter blockchain reduces to the shorter blockchain.

Definitions and Theorems

Theorem: trim-blocks-for-round-of-shorter

(defthm trim-blocks-for-round-of-shorter
 (implies
   (and (blocks-orderedp blocks2)
        (< (len blocks1) (len blocks2))
        (equal blocks1
               (nthcdr (- (len blocks2) (len blocks1))
                       blocks2)))
   (equal
        (trim-blocks-for-round
             (block->round (nth (1- (- (len blocks2) (len blocks1)))
                                blocks2))
             blocks1)
        (block-list-fix blocks1))))