		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-predecessor

There is a path from a certificate to each of its predecessors.

This should be intuitive, since predecessors 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-to-predecessor

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