		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-authors+round

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

Signature
(certs-with-authors+round authors round certs) → certs-with-authors-and-round
Arguments: authors — Guard (address-setp authors).; round — Guard (posp round).; certs — Guard (certificate-setp certs).
Returns: certs-with-authors-and-round — Type (certificate-setp certs-with-authors-and-round).

Definitions and Theorems

Function: certs-with-authors+round

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

Theorem: certificate-setp-of-certs-with-authors+round

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

Theorem: certs-with-authors+round-of-address-set-fix-authors

(defthm certs-with-authors+round-of-address-set-fix-authors
  (equal (certs-with-authors+round (address-set-fix authors)
                                   round certs)
         (certs-with-authors+round authors round certs)))

Theorem: certs-with-authors+round-address-set-equiv-congruence-on-authors

(defthm
   certs-with-authors+round-address-set-equiv-congruence-on-authors
  (implies
       (address-set-equiv authors authors-equiv)
       (equal (certs-with-authors+round authors round certs)
              (certs-with-authors+round authors-equiv round certs)))
  :rule-classes :congruence)

Theorem: certs-with-authors+round-of-pos-fix-round

(defthm certs-with-authors+round-of-pos-fix-round
  (equal (certs-with-authors+round authors (pos-fix round)
                                   certs)
         (certs-with-authors+round authors round certs)))

Theorem: certs-with-authors+round-pos-equiv-congruence-on-round

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

Theorem: certs-with-authors+round-subset

(defthm certs-with-authors+round-subset
 (implies (certificate-setp certs)
          (b* ((?certs-with-authors-and-round
                    (certs-with-authors+round authors round certs)))
            (subset certs-with-authors-and-round certs))))

Theorem: certs-with-authors+round-of-nil-certs

(defthm certs-with-authors+round-of-nil-certs
  (equal (certs-with-authors+round authors round nil)
         nil))

Theorem: certs-with-authors+round-when-emptyp-authors

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

Theorem: in-of-certs-with-authors+round

(defthm in-of-certs-with-authors+round
 (implies (certificate-setp certs)
          (equal (in cert
                     (certs-with-authors+round authors round certs))
                 (and (in cert certs)
                      (equal (certificate->round cert)
                             (pos-fix round))
                      (in (certificate->author cert)
                          (address-set-fix authors))))))

Theorem: certs-with-authors+round-to-authors-of-round

(defthm certs-with-authors+round-to-authors-of-round
  (implies
       (certificate-setp certs)
       (equal (certs-with-authors+round authors round certs)
              (certs-with-authors authors
                                  (certs-with-round round certs)))))

Theorem: certs-with-authors+round-to-round-of-authors

(defthm certs-with-authors+round-to-round-of-authors
 (implies
     (certificate-setp certs)
     (equal (certs-with-authors+round authors round certs)
            (certs-with-round round
                              (certs-with-authors authors certs)))))

Theorem: certificate-set->round-set-of-certs-with-authors+round

(defthm certificate-set->round-set-of-certs-with-authors+round
  (equal (certificate-set->round-set
              (certs-with-authors+round authors round certs))
         (if (emptyp (certs-with-authors+round authors round certs))
             nil
           (insert (pos-fix round) nil))))

Theorem: certificate-set->round-set-of-certs-with-authors+round-not-empty

(defthm
   certificate-set->round-set-of-certs-with-authors+round-not-empty
 (b* ((rounds (certificate-set->round-set
                   (certs-with-authors+round authors round certs))))
   (implies (not (emptyp rounds))
            (equal rounds (insert (pos-fix round) nil)))))