		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-author+round

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

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

Definitions and Theorems

Function: certs-with-author+round

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

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

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

Theorem: cert-set->author-set-of-certs-with-author+round

(defthm cert-set->author-set-of-certs-with-author+round
  (equal (cert-set->author-set
              (certs-with-author+round author round certs))
         (if (emptyp (certs-with-author+round author round certs))
             nil
           (insert (address-fix author) nil))))

Theorem: cert-set->round-set-of-certs-with-author+round

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

Theorem: certs-with-author+round-of-address-fix-author

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

Theorem: certs-with-author+round-address-equiv-congruence-on-author

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

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

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

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

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

Theorem: certs-with-author+round-of-certificate-set-fix-certs

(defthm certs-with-author+round-of-certificate-set-fix-certs
  (equal (certs-with-author+round author
                                  round (certificate-set-fix certs))
         (certs-with-author+round author round certs)))

Theorem: certs-with-author+round-certificate-set-equiv-congruence-on-certs

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