		Search-engine friendly clone of the ACL2 documentation.

Std/lists/true-listp

Lemmas about true-listp available in the std/lists library.

Note: the list of lemmas below is quite incomplete. For instance, the true-listp rule about append will be found in the documentation for std/lists/append, instead of here.

Definitions and Theorems

Theorem: true-listp-when-atom

(defthm true-listp-when-atom
  (implies (atom x)
           (equal (true-listp x) (not x))))

Theorem: true-listp-of-cons

(defthm true-listp-of-cons
  (equal (true-listp (cons a x))
         (true-listp x)))

Theorem: consp-under-iff-when-true-listp

(defthm consp-under-iff-when-true-listp
  (implies (true-listp x)
           (iff (consp x) x))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))