		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-head-of-predecessors

There is a path from a certificate to the first of its predecessors, assuming that it has predecessors.

This is a specialized version of path-to-predecessor, which we use to prove this theorem.

Definitions and Theorems

Theorem: path-to-head-of-predecessors

(defthm path-to-head-of-predecessors
 (implies
    (and (certificate-setp dag)
         (certificate-set-unequivocalp dag)
         (in cert dag)
         (not (emptyp (predecessors cert dag))))
    (equal (path-to-author+round
                cert
                (certificate->author (head (predecessors cert dag)))
                (certificate->round (head (predecessors cert dag)))
                dag)
           (head (predecessors cert dag)))))