		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-from-successor

In an unequivocal DAG, there is a path to a certificate from each of its successors.

This should be intuitive, since successors is based on the DAG edges, which define the paths.

We use the path-to-previous theorem to prove this, unsurprisingly.

Definitions and Theorems

Theorem: path-from-successor

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