		Search-engine friendly clone of the ACL2 documentation.

Message-certs-with-dest-of-make-certificate-messages

Relation between message extraction and message creation.

Definitions and Theorems

Theorem: message-certs-with-dest-of-make-certificate-messages

(defthm message-certs-with-dest-of-make-certificate-messages
 (implies
  (address-setp dests)
  (equal
    (message-certs-with-dest dest
                             (make-certificate-messages cert dests))
    (if (in (address-fix dest) dests)
        (insert (certificate-fix cert) nil)
      nil))))