		Search-engine friendly clone of the ACL2 documentation.

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