Dag-omni-paths-round-p-of-next-round
Preservation of dag-omni-paths-round-p
from one round to the next.
Having proved the base case in dag-omni-paths-round-p-base-case,
we need to prove the step case, which is done via this theorem first.
This theorem says that
if every certificate in round r' has a path to A),
then every certificate in round @($r'+1 has a path to A;
here cert is A.
The reason is that every certificate in round r'+1
has a path to its predecessors,
and each such predecessor has a path to A by the induction hypothesis
(which is stated as an explicit hypothesis in this theorem).
We use the transitivity of DAG paths,
to compose the path from round r'+1 to r'
with the path from round r' to certificate A.
We need to choose a specific predecessor,
and we pick the first one (i.e. head);
its existence is guaranteed by dag-predecessor-quorum-p,
and the fact that the quorum stake is always positive.
Although our proof by induction involves two DAGs,
this theorem only involves one,
because the induction step only involves paths in dag2.
Note that we use a weaker assumption on cert
than the fact that it is in the DAG,
namely just that it is non-nil.
This facilitates the final proof by induction,
which will just have the hypothesis that A is in dag1,
but not in dag2 as required for this theorem to apply.
We know that A is in dag2 as well
by path-from-cert2-to-cert1-in-dag2,
but that theorem has hypotheses about cert2 (i.e. C)
which are not readily available in the proof by induction.
Indeed, note that A is also in dag2
only if there is some certificate at round r+2 or later;
otherwise, A may not be in dag2 at all.
But by using the weaker hypothesis that cert is not nil,
we can easily relieve this hypothesis from the fact that
the anchor is in dag1, as available in the proof by induciton,
which implies that it is not nil.
Definitions and Theorems
Theorem: dag-omni-paths-round-p-of-next-round
(defthm dag-omni-paths-round-p-of-next-round
(implies (and (certificate-setp dag)
(certificate-set-unequivocalp dag)
(dag-closedp dag)
(dag-predecessor-quorum-p dag blockchain)
cert (posp round)
(dag-omni-paths-round-p round cert dag))
(dag-omni-paths-round-p (1+ round)
cert dag)))
