• 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
• Nthcdr

Std/lists/nthcdr

Lemmas about nthcdr available in the std/lists library.

Definitions and Theorems

Theorem: nthcdr-when-zp

(defthm nthcdr-when-zp
        (implies (zp n) (equal (nthcdr n x) x)))

Theorem: nthcdr-when-atom

(defthm nthcdr-when-atom
        (implies (atom x)
                 (equal (nthcdr n x) (if (zp n) x nil))))

Theorem: nthcdr-of-cons

(defthm nthcdr-of-cons
        (equal (nthcdr n (cons a x))
               (if (zp n)
                   (cons a x)
                   (nthcdr (- n 1) x))))

Theorem: true-listp-of-nthcdr

(defthm true-listp-of-nthcdr
        (equal (true-listp (nthcdr n x))
               (or (true-listp x)
                   (< (len x) (nfix n))))
        :rule-classes ((:rewrite)))

Theorem: len-of-nthcdr

(defthm len-of-nthcdr
        (equal (len (nthcdr n l))
               (nfix (- (len l) (nfix n)))))

Theorem: consp-of-nthcdr

(defthm consp-of-nthcdr
        (equal (consp (nthcdr n x))
               (< (nfix n) (len x))))

Theorem: open-small-nthcdr

(defthm open-small-nthcdr
        (implies (syntaxp (and (quotep n)
                               (natp (unquote n))
                               (< (unquote n) 5)))
                 (equal (nthcdr n x)
                        (if (zp n)
                            x (nthcdr (+ -1 n) (cdr x))))))

Theorem: acl2-count-of-nthcdr-rewrite

(defthm acl2-count-of-nthcdr-rewrite
        (equal (< (acl2-count (nthcdr n x))
                  (acl2-count x))
               (if (zp n)
                   nil
                   (or (consp x) (< 0 (acl2-count x))))))

Theorem: acl2-count-of-nthcdr-linear

(defthm acl2-count-of-nthcdr-linear
        (implies (and (not (zp n)) (consp x))
                 (< (acl2-count (nthcdr n x))
                    (acl2-count x)))
        :rule-classes :linear)

Theorem: acl2-count-of-nthcdr-linear-weak

(defthm acl2-count-of-nthcdr-linear-weak
        (<= (acl2-count (nthcdr n x))
            (acl2-count x))
        :rule-classes :linear)

Theorem: car-of-nthcdr

(defthm car-of-nthcdr
        (equal (car (nthcdr i x)) (nth i x)))

Theorem: nthcdr-of-cdr

(defthm nthcdr-of-cdr
        (equal (nthcdr i (cdr x))
               (cdr (nthcdr i x))))

Theorem: nthcdr-when-less-than-len-under-iff

(defthm nthcdr-when-less-than-len-under-iff
        (implies (< (nfix n) (len x))
                 (iff (nthcdr n x) t)))

Theorem: nthcdr-of-nthcdr

(defthm nthcdr-of-nthcdr
        (equal (nthcdr a (nthcdr b x))
               (nthcdr (+ (nfix a) (nfix b)) x)))

Theorem: append-of-take-and-nthcdr

(defthm append-of-take-and-nthcdr
        (implies (<= (nfix n) (len x))
                 (equal (append (take n x) (nthcdr n x))
                        x)))

Theorem: nthcdr-of-list-fix

(defthm nthcdr-of-list-fix
        (equal (nthcdr n (list-fix x))
               (list-fix (nthcdr n x))))

Theorem: element-list-p-of-nthcdr

(defthm element-list-p-of-nthcdr
        (implies (element-list-p (double-rewrite x))
                 (element-list-p (nthcdr n x)))
        :rule-classes :rewrite)

Theorem: nthcdr-of-elementlist-projection

(defthm nthcdr-of-elementlist-projection
        (equal (nthcdr n (elementlist-projection x))
               (elementlist-projection (nthcdr n x)))
        :rule-classes :rewrite)

Theorem: subsetp-of-nthcdr

(defthm subsetp-of-nthcdr
        (subsetp-equal (nthcdr n l) l))