• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Len

Std/lists/len

Lemmas about len available in the std/lists library.

Definitions and Theorems

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))))