		Search-engine friendly clone of the ACL2 documentation.

Theorems-about-osets

Note that the theorem that rewrites in to member-equal is disabled by default. It can be locally enabled in certain proofs as needed.

Theorem: cardinality-of-tail

(defthm cardinality-of-tail
  (equal (cardinality (tail x))
         (if (emptyp x) 0 (1- (cardinality x)))))

Theorem: subset-of-tail-left

(defthm subset-of-tail-left
  (implies (subset x y)
           (subset (tail x) y)))

Theorem: in-to-member-when-setp

(defthm in-to-member-when-setp
  (implies (setp x)
           (iff (in a x) (member-equal a x))))