		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Std/system/all-fnnames

Theorems about all-fnnames.

More precisely, these are theorems about all-fnnames1, because all-fnnames, as well as all-fnnames-lst, is a macro that abbreviates all-fnnames1.

We also include the following theorem from system/all-fnnames.lisp:

Theorem: true-listp-all-fnnames

(defthm true-listp-all-fnnames
  (implies (true-listp acc)
           (true-listp (all-fnnames1 flg x acc))))

Definitions and Theorems

Theorem: true-listp-of-all-fnnames1-type

(defthm true-listp-of-all-fnnames1-type
  (implies (true-listp acc)
           (true-listp (all-fnnames1 flg x acc)))
  :rule-classes :type-prescription)

Theorem: symbol-listp-of-all-fnnames1

(defthm symbol-listp-of-all-fnnames1
  (implies (and (symbol-listp acc)
                (if flg (pseudo-term-listp x)
                  (pseudo-termp x)))
           (symbol-listp (all-fnnames1 flg x acc))))

Theorem: all-fnnames1-includes-acc

(defthm all-fnnames1-includes-acc
  (subsetp-equal acc (all-fnnames1 flg x acc)))

Theorem: all-fnnames1-monotonic-acc

(defthm all-fnnames1-monotonic-acc
  (implies (subsetp-equal acc1 acc2)
           (subsetp-equal (all-fnnames1 flg x acc1)
                          (all-fnnames1 flg x acc2))))