		Search-engine friendly clone of the ACL2 documentation.

Certificates

Cert-set->round-set

Lift certificate->round to sets.

Signature
(cert-set->round-set certs) → rounds
Arguments: certs — Guard (certificate-setp certs).
Returns: rounds — Type (pos-setp rounds).

Definitions and Theorems

Function: cert-set->round-set

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

Theorem: pos-setp-of-cert-set->round-set

(defthm pos-setp-of-cert-set->round-set
  (b* ((rounds (cert-set->round-set certs)))
    (pos-setp rounds))
  :rule-classes :rewrite)

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

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

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

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

Theorem: cert-set->round-set-monotone

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

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

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

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

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

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

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

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

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

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

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