|
|
|---|
|
|
|
|---|
Equivalence between two ways to phrase list extensions.
As explained in same-committees-def-and-implied, the interesting case of the proof is that of a longer blockchain extending a shorter blockchain. In lists-noforkp, the extension is expressed in terms of nthcdr. However, for some of our proofs, a formulation in terms of append is more convenient. Here we provide a bridge between the two formulations.
We also prove an equivalence (really, an implication) between
two ways to address the rightmost element of the extension.
The extension is the
This is really a generic theorem about lists, not specific to AleoBFT. We could consider putting it into a library, ideally in some more general form. Or perhaps there is a way to use more general list theorems in the proofs of this invariant.
Theorem:
(defthm same-committees-list-extension-equivalences (implies (and (< (len list1) (len list2)) (equal list1 (nthcdr (- (len list2) (len list1)) list2))) (and (equal (append (take (- (len list2) (len list1)) list2) list1) list2) (equal (nth (1- (- (len list2) (len list1))) list2) (car (last (take (- (len list2) (len list1)) list2)))))))