		Search-engine friendly clone of the ACL2 documentation.

Std/lists/len

Lemmas about len available in the std/lists library.

Theorem: len-when-atom

(defthm len-when-atom
  (implies (atom x) (equal (len x) 0)))

Theorem: len-of-cons

(defthm len-of-cons
  (equal (len (cons a x)) (+ 1 (len x))))

Theorem: (equal 0 (len x))

(defthm |(equal 0 (len x))|
  (equal (equal 0 (len x)) (atom x)))

Theorem: (< 0 (len x))

(defthm |(< 0 (len x))|
  (equal (< 0 (len x)) (consp x)))

Theorem: consp-by-len

(defthm consp-by-len
  (implies (and (equal (len x) n)
                (syntaxp (quotep n)))
           (equal (consp x) (< 0 n))))

Theorem: consp-of-cdr-by-len

(defthm consp-of-cdr-by-len
  (implies (and (equal (len x) n)
                (syntaxp (quotep n)))
           (equal (consp (cdr x)) (< 1 n))))

Theorem: consp-of-cddr-by-len

(defthm consp-of-cddr-by-len
  (implies (and (equal (len x) n)
                (syntaxp (quotep n)))
           (equal (consp (cddr x)) (< 2 n))))

Theorem: consp-of-cdddr-by-len

(defthm consp-of-cdddr-by-len
  (implies (and (equal (len x) n)
                (syntaxp (quotep n)))
           (equal (consp (cdddr x)) (< 3 n))))