		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate->previous

Set of references to previous certificates of (the proposal in) a certificate.

Signature
(certificate->previous cert) → previous
Arguments: cert — Guard (certificatep cert).
Returns: previous — Type (address-setp previous).

Definitions and Theorems

Function: certificate->previous

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

Theorem: address-setp-of-certificate->previous

(defthm address-setp-of-certificate->previous
  (b* ((previous (certificate->previous cert)))
    (address-setp previous))
  :rule-classes :rewrite)

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

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

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

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