		Search-engine friendly clone of the ACL2 documentation.

Dags

In-of-certificate-causal-history

Characterization of the members of a certificate's causal history.

Given an unequivocal DAG and a certificate in it, the elements of the causal history of the certificate in the DAG consist exactly of the certificates reachable from the certificate.

Definitions and Theorems

Theorem: in-of-certificate-causal-history

(defthm in-of-certificate-causal-history
 (implies
  (and (certificate-setp dag)
       (certificate-set-unequivocalp dag)
       (in cert dag))
  (equal
   (in cert0
       (certificate-causal-history cert dag))
   (and
       cert0
       (equal (path-to-author+round cert (certificate->author cert0)
                                    (certificate->round cert0)
                                    dag)
              cert0)))))

Theorem: in-of-certificate-set-causal-history

(defthm in-of-certificate-set-causal-history
 (implies
  (and (certificate-setp dag)
       (certificate-set-unequivocalp dag)
       (subset certs dag))
  (equal
   (in cert0
       (certificate-set-causal-history certs dag))
   (and
    cert0
    (equal
         (path-to-author+round-set certs (certificate->author cert0)
                                   (certificate->round cert0)
                                   dag)
         cert0)))))