		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate->round

Round number of (the proposal in) a certificate.

Signature
(certificate->round cert) → round
Arguments: cert — Guard (certificatep cert).
Returns: round — Type (posp round).

Definitions and Theorems

Function: certificate->round

(defun certificate->round (cert)
  (declare (xargs :guard (certificatep cert)))
  (let ((__function__ 'certificate->round))
    (declare (ignorable __function__))
    (proposal->round (certificate->proposal cert))))

Theorem: posp-of-certificate->round

(defthm posp-of-certificate->round
  (b* ((round (certificate->round cert)))
    (posp round))
  :rule-classes :rewrite)

Theorem: certificate->round-of-certificate-fix-cert

(defthm certificate->round-of-certificate-fix-cert
  (equal (certificate->round (certificate-fix cert))
         (certificate->round cert)))

Theorem: certificate->round-certificate-equiv-congruence-on-cert

(defthm certificate->round-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (certificate->round cert)
                  (certificate->round cert-equiv)))
  :rule-classes :congruence)