|
|
|---|
|
|
|
|---|
Check if the round numbers of all the certificates in a list are even.
(certificate-list-evenp x) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun certificate-list-evenp (x) (declare (xargs :guard (certificate-listp x))) (let ((__function__ 'certificate-list-evenp)) (declare (ignorable __function__)) (if (consp x) (and (evenp (certificate->round (car x))) (certificate-list-evenp (cdr x))) t)))
Theorem:
(defthm certificate-list-evenp-of-certificate-list-fix-x (equal (certificate-list-evenp (certificate-list-fix x)) (certificate-list-evenp x)))
Theorem:
(defthm certificate-list-evenp-certificate-list-equiv-congruence-on-x (implies (certificate-list-equiv x x-equiv) (equal (certificate-list-evenp x) (certificate-list-evenp x-equiv))) :rule-classes :congruence)