		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate->transactions

List of transactions of (the proposal in) a certificate.

Signature
(certificate->transactions cert) → transactions
Arguments: cert — Guard (certificatep cert).
Returns: transactions — Type (transaction-listp transactions).

Definitions and Theorems

Function: certificate->transactions

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

Theorem: transaction-listp-of-certificate->transactions

(defthm transaction-listp-of-certificate->transactions
  (b* ((transactions (certificate->transactions cert)))
    (transaction-listp transactions))
  :rule-classes :rewrite)

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

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

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

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