		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate->author

Author of (the proposal in) a certificate.

Signature
(certificate->author cert) → author
Arguments: cert — Guard (certificatep cert).
Returns: author — Type (addressp author).

Definitions and Theorems

Function: certificate->author

(defun certificate->author (cert)
  (declare (xargs :guard (certificatep cert)))
  (let ((__function__ 'certificate->author))
    (declare (ignorable __function__))
    (proposal->author (certificate->proposal cert))))

Theorem: addressp-of-certificate->author

(defthm addressp-of-certificate->author
  (b* ((author (certificate->author cert)))
    (addressp author))
  :rule-classes :rewrite)

Theorem: certificate->author-of-certificate-fix-cert

(defthm certificate->author-of-certificate-fix-cert
  (equal (certificate->author (certificate-fix cert))
         (certificate->author cert)))

Theorem: certificate->author-certificate-equiv-congruence-on-cert

(defthm certificate->author-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (certificate->author cert)
                  (certificate->author cert-equiv)))
  :rule-classes :congruence)