		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-previous

In an unequivocal DAG, there is always a path between a certificate and each of its predecessors.

This should be intuitive, since paths arise precisely from the edges of the DAG.

Here cert1 is a generic certificate and cert is one of its predecessors, as characterized by being in the immediately preceding round and by being authored by one of the authors referenced in cert1.

We use path-to-author+round-set-to-path-to-author+round to prove this theorem, because when path-to-author+round is opened, it exposes path-to-author+round-set. We also need path-to-author+round-of-self, applied to the certificate in the set of predecessors.

Definitions and Theorems

Theorem: path-to-previous

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