		Search-engine friendly clone of the ACL2 documentation.

Anchors-extension

Collect-all-anchors-to-append-of-collect-anchors

Extension theorem for collect-all-anchors, for a single DAG.

This follows from collect-anchors-to-append-of-collect-anchors, since collect-all-anchors is essentially a wrapper of collect-anchors.

Definitions and Theorems

Theorem: collect-all-anchors-to-append-of-collect-anchors

(defthm collect-all-anchors-to-append-of-collect-anchors
 (implies
  (and
    (certificate-setp dag)
    (dag-has-committees-p dag blockchain)
    (dag-in-committees-p dag blockchain)
    (in anchor dag)
    (evenp (certificate->round anchor))
    (equal
         (certificate->author anchor)
         (leader-at-round
              (certificate->round anchor)
              (active-committee-at-round (certificate->round anchor)
                                         blockchain)))
    (dag-omni-paths-p anchor dag)
    (in anchor1 dag)
    (evenp (certificate->round anchor1))
    (< (certificate->round anchor)
       (certificate->round anchor1)))
  (equal (collect-all-anchors anchor1 dag blockchain)
         (append (collect-anchors anchor1
                                  (- (certificate->round anchor1) 2)
                                  (certificate->round anchor)
                                  dag blockchain)
                 (collect-all-anchors anchor dag blockchain)))))