Lift message->certificate to sets.
(message-set->certificate-set msgs) → certs
Function:
(defun message-set->certificate-set (msgs) (declare (xargs :guard (message-setp msgs))) (let ((__function__ 'message-set->certificate-set)) (declare (ignorable __function__)) (cond ((emptyp msgs) nil) (t (insert (message->certificate (head msgs)) (message-set->certificate-set (tail msgs)))))))
Theorem:
(defthm certificate-setp-of-message-set->certificate-set (b* ((certs (message-set->certificate-set msgs))) (certificate-setp certs)) :rule-classes :rewrite)
Theorem:
(defthm message->certificate-in-message-set->certificate-set (implies (in msg msgs) (in (message->certificate msg) (message-set->certificate-set msgs))))
Theorem:
(defthm message-set->certificate-set-of-insert (equal (message-set->certificate-set (insert msg msgs)) (insert (message->certificate msg) (message-set->certificate-set msgs))))
Theorem:
(defthm message-set->certificate-set-of-union (equal (message-set->certificate-set (union msgs1 msgs2)) (union (message-set->certificate-set msgs1) (message-set->certificate-set (sfix msgs2)))))
Theorem:
(defthm message-set->certificate-set-monotone (implies (subset msgs1 msgs2) (subset (message-set->certificate-set msgs1) (message-set->certificate-set msgs2))))
Theorem:
(defthm in-of-message-set->certificate-set-of-delete (implies (and (certificatep cert) (message-setp msgs) (in cert (message-set->certificate-set msgs)) (not (equal (message->certificate msg) cert))) (in cert (message-set->certificate-set (delete msg msgs)))))