		Search-engine friendly clone of the ACL2 documentation.

Anchors

Collect-all-anchors-in-unequivocal-closed-dags

Some theorems about collect-all-anchors applied on unequivocal, backward-closed DAGs.

The first theorem says that all the anchors collected, starting from an anchor, from a backward-closed subset of an unequivocal DAG are the same in the superset. This is a simple consequence of the analogous theorem about collect-anchors.

The second theorem says that all the anchors collected, starting from a common anchor, from two backward-closed, (individually and mutually) unequivocal DAGs are the same in the two DAGS. This is a simple consequence of the analogous theorem about collect-anchors.

Definitions and Theorems

Theorem: collect-all-anchors-of-unequivocal-superdag

(defthm collect-all-anchors-of-unequivocal-superdag
  (implies
       (and (certificate-setp dag0)
            (certificate-setp dag)
            (subset dag0 dag)
            (certificate-set-unequivocalp dag)
            (dag-closedp dag0)
            (in last-anchor dag0))
       (equal (collect-all-anchors last-anchor dag blockchain)
              (collect-all-anchors last-anchor dag0 blockchain))))

Theorem: collect-all-anchors-of-unequivocal-dags

(defthm collect-all-anchors-of-unequivocal-dags
  (implies
       (and (certificate-setp dag1)
            (certificate-setp dag2)
            (certificate-set-unequivocalp dag1)
            (certificate-set-unequivocalp dag2)
            (certificate-sets-unequivocalp dag1 dag2)
            (dag-closedp dag1)
            (dag-closedp dag2)
            (dag-has-committees-p dag1 blockchain1)
            (dag-has-committees-p dag2 blockchain2)
            (same-active-committees-p blockchain1 blockchain2)
            (in last-anchor dag1)
            (in last-anchor dag2))
       (equal (collect-all-anchors last-anchor dag1 blockchain1)
              (collect-all-anchors last-anchor dag2 blockchain2))))