		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-author+round-transitive

Transitivity of DAG paths.

If there is a path from cert to cert1, and a there is a path from cert1 to cert2, then there is a path from cert and cert2. The property is quite intuitive, but note that we have the hypothesis that the DAG is unequivocal. If the DAG were not unequivocal, paths to the same author and round from different certificates could potentially return different certificates.

Definitions and Theorems

Theorem: path-to-author+round-transitive

(defthm path-to-author+round-transitive
 (implies
  (and
      (certificate-setp dag)
      (certificate-set-unequivocalp dag)
      (in cert dag)
      (in cert1 dag)
      (in cert2 dag)
      (equal (path-to-author+round cert (certificate->author cert1)
                                   (certificate->round cert1)
                                   dag)
             cert1)
      (equal (path-to-author+round cert1 (certificate->author cert2)
                                   (certificate->round cert2)
                                   dag)
             cert2))
  (equal (path-to-author+round cert (certificate->author cert2)
                               (certificate->round cert2)
                               dag)
         cert2)))