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