|
|
|---|
|
|
|
|---|
In an unequivocal DAG, if there is a path between two certificates, the causal history of the destination of the path is a subset of the causal history of the source of the path.
Theorem:
(defthm certificate-causal-history-subset-when-path (implies (and (certificate-setp dag) (certificate-set-unequivocalp dag) (in cert dag) (addressp author) (posp round) (path-to-author+round cert author round dag)) (subset (certificate-causal-history (path-to-author+round cert author round dag) dag) (certificate-causal-history cert dag))))