		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Trim-blocks-for-round-of-longer

Result of trimming the longer blockchain.

This is one of the main reasoning steps in our overall proof. As mentioned earlier, we expand the two committee calculations to include calls of trim-blocks-for-round, which we then simplify to the same thing. This theorem simplifies the call for the longer blockchain. The relation between longer and shorter blockchains is expressed in terms of nthcdr, but the core theorem trim-blocks-for-round-of-append-yields-first uses the append formulation, so we use the theorem about list equivalences.

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

Definitions and Theorems

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

(defthm trim-blocks-for-round-of-longer
 (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))
             blocks2)
        (block-list-fix blocks1))))