• Top
  • Documentation
  • Books
  • 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
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • 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/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

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