Lift certificate->author to sets.
(cert-set->author-set certs) → addrs
Function:
(defun cert-set->author-set (certs) (declare (xargs :guard (certificate-setp certs))) (let ((__function__ 'cert-set->author-set)) (declare (ignorable __function__)) (cond ((emptyp (certificate-set-fix certs)) nil) (t (insert (certificate->author (head certs)) (cert-set->author-set (tail certs)))))))
Theorem:
(defthm address-setp-of-cert-set->author-set (b* ((addrs (cert-set->author-set certs))) (address-setp addrs)) :rule-classes :rewrite)
Theorem:
(defthm emptyp-of-cert-set->author-set (equal (emptyp (cert-set->author-set certs)) (emptyp (certificate-set-fix certs))))
Theorem:
(defthm certificate->author-in-cert-set->author-set (implies (in (certificate-fix cert) (certificate-set-fix certs)) (in (certificate->author cert) (cert-set->author-set certs))))
Theorem:
(defthm cert-set->author-set-monotone (implies (subset certs1 (certificate-set-fix certs2)) (subset (cert-set->author-set certs1) (cert-set->author-set certs2))))
Theorem:
(defthm cert-set->author-set-of-insert (implies (and (certificatep cert) (certificate-setp certs)) (equal (cert-set->author-set (insert cert certs)) (insert (certificate->author cert) (cert-set->author-set certs)))))
Theorem:
(defthm cert-set->author-set-of-union (implies (and (certificate-setp certs1) (certificate-setp certs2)) (equal (cert-set->author-set (union certs1 certs2)) (union (cert-set->author-set certs1) (cert-set->author-set certs2)))))
Theorem:
(defthm same-certificate-author-when-cardinality-leq-1 (implies (and (<= (cardinality (cert-set->author-set certs)) 1) (in cert1 (certificate-set-fix certs)) (in cert2 (certificate-set-fix certs))) (equal (certificate->author cert1) (certificate->author cert2))))
Theorem:
(defthm cert-set->author-set-of-certificate-set-fix-certs (equal (cert-set->author-set (certificate-set-fix certs)) (cert-set->author-set certs)))
Theorem:
(defthm cert-set->author-set-certificate-set-equiv-congruence-on-certs (implies (certificate-set-equiv certs certs-equiv) (equal (cert-set->author-set certs) (cert-set->author-set certs-equiv))) :rule-classes :congruence)