		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificates-with-round

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

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 (pos-fix 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-of-pos-fix-round

(defthm certificates-with-round-of-pos-fix-round
  (equal (certificates-with-round (pos-fix round)
                                  certs)
         (certificates-with-round round certs)))

Theorem: certificates-with-round-pos-equiv-congruence-on-round

(defthm certificates-with-round-pos-equiv-congruence-on-round
  (implies (acl2::pos-equiv round round-equiv)
           (equal (certificates-with-round round certs)
                  (certificates-with-round round-equiv certs)))
  :rule-classes :congruence)

Theorem: certificates-with-round-subset

(defthm certificates-with-round-subset
 (implies
     (certificate-setp certs)
     (b* ((?certs-with-round (certificates-with-round round 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)
                              (pos-fix round))))))

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-set->round-set-of-certificates-with-round

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

Theorem: emptyp-of-certificates-with-round-to-no-round

(defthm emptyp-of-certificates-with-round-to-no-round
  (equal (emptyp (certificates-with-round round certs))
         (not (in (pos-fix round)
                  (certificate-set->round-set certs)))))

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)

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

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