		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-round

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

Signature
(certs-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: certs-with-round

(defun certs-with-round (round certs)
  (declare (xargs :guard (and (posp round)
                              (certificate-setp certs))))
  (let ((__function__ 'certs-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)
                  (certs-with-round round (tail certs)))
        (certs-with-round round (tail certs))))))

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

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

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

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

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

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

Theorem: certs-with-round-subset

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

Theorem: certs-with-round-of-nil

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

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

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

Theorem: in-of-certs-with-round

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

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

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

Theorem: certs-with-round-monotone

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

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

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

Theorem: cardinality-of-round-set-of-certs-with-round-leq-1

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

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

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

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

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