Anchors-extension
Extension of anchor sequences.
We show that all the anchors in a DAG from a later anchor
are an extension of all the anchors from an earlier anchor.
This relies on the property, proved in dag-omni-paths,
that if an anchor has at least f+1 successors,
there are paths to it from all the certificates
at least two rounds ahead in the same or different DAG.
Under this condition, which is expressed by dag-omni-paths-p,
given two anchors anchor and anchor1,
the latter at a later round than the former,
all the anchors collected starting from anchor1
are an extension of all the anchors collected starting from anchor.
The reason is that there must be a path from anchor1 to anchor.
The extra anchors are exactly the ones collected
starting from anchor1 down to the round of anchor.
Subtopics
- Collect-anchors-to-append-of-collect-anchors
- Extension theorem for collect-anchors, for a single DAG.
- Collect-all-anchors-to-append-of-collect-anchors-dags
- Extension theorem for collect-all-anchors, for two DAGs.
- Collect-all-anchors-to-append-of-collect-anchors
- Extension theorem for collect-all-anchors, for a single DAG.
