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