		Search-engine friendly clone of the ACL2 documentation.

Operations-certificate-retrieval

Certificates-with-round

Retrieve the set of certificates with a given round from a set.

Signature
(certificates-with-round round certs) → certs-with-round
Arguments: round — Guard (posp round).; certs — Guard (certificate-setp certs).
Returns: certs-with-round — Type (certificate-setp certs-with-round).

Definitions and Theorems

Function: certificates-with-round

(defun certificates-with-round (round certs)
  (declare (xargs :guard (and (posp round)
                              (certificate-setp certs))))
  (let ((__function__ 'certificates-with-round))
    (declare (ignorable __function__))
    (b* (((when (emptyp certs)) nil)
         ((certificate cert) (head certs)))
      (if (equal round cert.round)
          (insert (certificate-fix cert)
                  (certificates-with-round round (tail certs)))
        (certificates-with-round round (tail certs))))))

Theorem: certificate-setp-of-certificates-with-round

(defthm certificate-setp-of-certificates-with-round
  (b* ((certs-with-round (certificates-with-round round certs)))
    (certificate-setp certs-with-round))
  :rule-classes :rewrite)

Theorem: certificates-with-round-subset

(defthm certificates-with-round-subset
  (b* ((?certs-with-round (certificates-with-round round certs)))
    (implies (certificate-setp certs)
             (subset certs-with-round certs))))

Theorem: in-of-certificates-with-round

(defthm in-of-certificates-with-round
  (implies (certificate-setp certs)
           (equal (in cert
                      (certificates-with-round round certs))
                  (and (in cert certs)
                       (equal (certificate->round cert)
                              round)))))

Theorem: certificates-with-round-when-emptyp

(defthm certificates-with-round-when-emptyp
  (implies (emptyp certs)
           (equal (certificates-with-round round certs)
                  nil)))

Theorem: certificates-with-round-of-insert

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

Theorem: certificates-with-round-monotone

(defthm certificates-with-round-monotone
  (implies (and (certificate-setp certs1)
                (certificate-setp certs2)
                (subset certs1 certs2))
           (subset (certificates-with-round round certs1)
                   (certificates-with-round round certs2))))

Theorem: certificate-with-author+round-when-author-in-round

(defthm certificate-with-author+round-when-author-in-round
  (implies (and (certificate-setp certs)
                (in author
                    (certificate-set->author-set
                         (certificates-with-round round certs))))
           (certificate-with-author+round author round certs)))

Theorem: certificates-with-round-of-intersect

(defthm certificates-with-round-of-intersect
 (implies
    (and (certificate-setp certs1)
         (certificate-setp certs2))
    (equal (certificates-with-round round (intersect certs1 certs2))
           (intersect (certificates-with-round round certs1)
                      (certificates-with-round round certs2)))))

Theorem: round-set-of-certificates-with-round

(defthm round-set-of-certificates-with-round
 (equal
  (certificate-set->round-set (certificates-with-round round certs))
  (if (emptyp (certificates-with-round round certs))
      nil
    (insert round nil))))

Theorem: round-set-of-certificates-with-round-possibilities

(defthm round-set-of-certificates-with-round-possibilities
  (or (equal (certificate-set->round-set
                  (certificates-with-round round certs))
             nil)
      (equal (certificate-set->round-set
                  (certificates-with-round round certs))
             (insert round nil))))

Theorem: cardinality-of-round-set-of-certificates-with-round

(defthm cardinality-of-round-set-of-certificates-with-round
  (<= (cardinality (certificate-set->round-set
                        (certificates-with-round round certs)))
      1)
  :rule-classes :linear)

Theorem: cardinality-of-subset-of-round-set-of-round

(defthm cardinality-of-subset-of-round-set-of-round
  (implies (subset certs0
                   (certificates-with-round round certs))
           (<= (cardinality (certificate-set->round-set certs0))
               1))
  :rule-classes :linear)