Negation of the param->rate-then-capacity-p parameter.
Function:
(defun param->capacity-then-rate-p (param) (declare (xargs :guard (paramp param))) (let ((__function__ 'param->capacity-then-rate-p)) (declare (ignorable __function__)) (not (param->rate-then-capacity-p param))))
Theorem:
(defthm booleanp-of-param->capacity-then-rate-p (b* ((yes/no (param->capacity-then-rate-p param))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm param->capacity-then-rate-p-of-param-fix-param (equal (param->capacity-then-rate-p (param-fix param)) (param->capacity-then-rate-p param)))
Theorem:
(defthm param->capacity-then-rate-p-param-equiv-congruence-on-param (implies (param-equiv param param-equiv) (equal (param->capacity-then-rate-p param) (param->capacity-then-rate-p param-equiv))) :rule-classes :congruence)