		Search-engine friendly clone of the ACL2 documentation.

Library-extensions

Set::nonemptyp

Check if an oset is not empty, using an existential quantifier.

When this predicate is true, it provides an under-specified witness member of the set, which is useful for certain kinds of reasoning.

Definitions and Theorems

Theorem: nonemptyp-suff

(defthm set::nonemptyp-suff
  (implies (in elem set)
           (set::nonemptyp set)))

Theorem: booleanp-of-nonemptyp

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

Theorem: nonemptyp-when-not-emptyp

(defthm set::nonemptyp-when-not-emptyp
  (implies (not (emptyp set))
           (set::nonemptyp set)))

Theorem: not-emptyp-when-nonemptyp

(defthm set::not-emptyp-when-nonemptyp
  (implies (set::nonemptyp set)
           (not (emptyp set))))

Theorem: not-emptyp-to-nonemptyp

(defthm set::not-emptyp-to-nonemptyp
  (equal (not (emptyp set))
         (set::nonemptyp set)))

Theorem: nonempty-witness-from-not-emptyp

(defthm set::nonempty-witness-from-not-emptyp
  (implies (not (emptyp set))
           (in (set::nonempty-witness set) set))
  :rule-classes ((:forward-chaining :trigger-terms ((emptyp set)))))