		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-author+round-set-to-path-to-author+round

In an unequivocal DAG, if a certificate has a path to an author and round, then any set including the certificate has a path to that author and round, and it results in the same certificate.

The function path-to-author+round-set is the mutually recursive companion of path-to-author+round. It is defined by going through every element in the set, and calling path-to-author+round on each element. Thus, if path-to-author+round returns some certificate when called on cert, if we put cert in a set certs and call path-to-author+round-set, we must certainly reach a certificate, which must be the same because of non-equivocation.

Definitions and Theorems

Theorem: path-to-author+round-set-to-path-to-author+round

(defthm path-to-author+round-set-to-path-to-author+round
  (implies (and (certificate-setp dag)
                (certificate-set-unequivocalp dag)
                (certificate-setp certs)
                (subset certs dag)
                (in cert certs)
                (path-to-author+round cert author round dag))
           (equal (path-to-author+round-set certs author round dag)
                  (path-to-author+round cert author round dag))))