		Search-engine friendly clone of the ACL2 documentation.

Certificates

Cert-set->author-set

Lift certificate->author to sets.

Signature
(cert-set->author-set certs) → addrs
Arguments: certs — Guard (certificate-setp certs).
Returns: addrs — Type (address-setp addrs).

Definitions and Theorems

Function: cert-set->author-set

(defun cert-set->author-set (certs)
  (declare (xargs :guard (certificate-setp certs)))
  (let ((__function__ 'cert-set->author-set))
    (declare (ignorable __function__))
    (cond ((emptyp (certificate-set-fix certs))
           nil)
          (t (insert (certificate->author (head certs))
                     (cert-set->author-set (tail certs)))))))

Theorem: address-setp-of-cert-set->author-set

(defthm address-setp-of-cert-set->author-set
  (b* ((addrs (cert-set->author-set certs)))
    (address-setp addrs))
  :rule-classes :rewrite)

Theorem: emptyp-of-cert-set->author-set

(defthm emptyp-of-cert-set->author-set
  (equal (emptyp (cert-set->author-set certs))
         (emptyp (certificate-set-fix certs))))

Theorem: certificate->author-in-cert-set->author-set

(defthm certificate->author-in-cert-set->author-set
  (implies (in (certificate-fix cert)
               (certificate-set-fix certs))
           (in (certificate->author cert)
               (cert-set->author-set certs))))

Theorem: cert-set->author-set-monotone

(defthm cert-set->author-set-monotone
  (implies (subset certs1 (certificate-set-fix certs2))
           (subset (cert-set->author-set certs1)
                   (cert-set->author-set certs2))))

Theorem: cert-set->author-set-of-insert

(defthm cert-set->author-set-of-insert
  (implies (and (certificatep cert)
                (certificate-setp certs))
           (equal (cert-set->author-set (insert cert certs))
                  (insert (certificate->author cert)
                          (cert-set->author-set certs)))))

Theorem: cert-set->author-set-of-union

(defthm cert-set->author-set-of-union
  (implies (and (certificate-setp certs1)
                (certificate-setp certs2))
           (equal (cert-set->author-set (union certs1 certs2))
                  (union (cert-set->author-set certs1)
                         (cert-set->author-set certs2)))))

Theorem: same-certificate-author-when-cardinality-leq-1

(defthm same-certificate-author-when-cardinality-leq-1
  (implies (and (<= (cardinality (cert-set->author-set certs))
                    1)
                (in cert1 (certificate-set-fix certs))
                (in cert2 (certificate-set-fix certs)))
           (equal (certificate->author cert1)
                  (certificate->author cert2))))

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

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

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

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