		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-nonemptyp

Check is a committee is not empty.

Signature
(committee-nonemptyp commtt) → yes/no
Arguments: commtt — Guard (committeep commtt).
Returns: yes/no — Type (booleanp yes/no).

That is, check whether it has members.

Definitions and Theorems

Function: committee-nonemptyp

(defun committee-nonemptyp (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-nonemptyp))
    (declare (ignorable __function__))
    (not (emptyp (committee-members commtt)))))

Theorem: booleanp-of-committee-nonemptyp

(defthm booleanp-of-committee-nonemptyp
  (b* ((yes/no (committee-nonemptyp commtt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: committee-nonemptyp-when-nonempty-subset

(defthm committee-nonemptyp-when-nonempty-subset
  (implies (and (subset members (committee-members commtt))
                (not (emptyp members)))
           (committee-nonemptyp commtt)))

Theorem: committee-nonemptyp-of-committee-fix-commtt

(defthm committee-nonemptyp-of-committee-fix-commtt
  (equal (committee-nonemptyp (committee-fix commtt))
         (committee-nonemptyp commtt)))

Theorem: committee-nonemptyp-committee-equiv-congruence-on-commtt

(defthm committee-nonemptyp-committee-equiv-congruence-on-commtt
  (implies (committee-equiv commtt commtt-equiv)
           (equal (committee-nonemptyp commtt)
                  (committee-nonemptyp commtt-equiv)))
  :rule-classes :congruence)