		Search-engine friendly clone of the ACL2 documentation.

Certificates

Cert-with-author+round

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

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

If there is no certificate with the given author and round, or if there is more thatn one, nil is returned, for no certificate. Otherwise, if there is exactly one certificate with that author and round, the certificate is returned.

Definitions and Theorems

Function: cert-with-author+round

(defun cert-with-author+round (author round certs)
  (declare (xargs :guard (and (addressp author)
                              (posp round)
                              (certificate-setp certs))))
  (let ((__function__ 'cert-with-author+round))
    (declare (ignorable __function__))
    (b* ((certs-ar (certs-with-author+round author round certs))
         ((unless (= (cardinality certs-ar) 1))
          nil))
      (certificate-fix (head certs-ar)))))

Theorem: certificate-optionp-of-cert-with-author+round

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

Theorem: certificate->author-of-cert-with-author+round

(defthm certificate->author-of-cert-with-author+round
 (implies
  (cert-with-author+round author round certs)
  (equal
   (certificate->author (cert-with-author+round author round certs))
   (address-fix author))))

Theorem: certificate->round-of-cert-with-author+round

(defthm certificate->round-of-cert-with-author+round
 (implies
  (cert-with-author+round author round certs)
  (equal
    (certificate->round (cert-with-author+round author round certs))
    (pos-fix round))))

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

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

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

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

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

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

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

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

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

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

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

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