		Search-engine friendly clone of the ACL2 documentation.

Nthcdr-theorems

Some theorems about the built-in function nthcdr.

The theorems nthcdr-of-append-when-leq-len-first and nthcdr-of-append-when-gt-len-first are disabled by default. They are special cases of nthcdr-of-append, which is enabled by default and is perhaps more useful in general.

Definitions and Theorems

Theorem: nthcdr-of-append-when-leq-len-first

(defthm nthcdr-of-append-when-leq-len-first
  (implies (<= n (len a))
           (equal (nthcdr n (append a b))
                  (append (nthcdr n a) b))))

Theorem: nthcdr-of-append-when-gt-len-first

(defthm nthcdr-of-append-when-gt-len-first
  (implies (and (natp n) (> n (len a)))
           (equal (nthcdr n (append a b))
                  (nthcdr (- n (len a)) b))))

Theorem: nthcdr-of-append

(defthm nthcdr-of-append
  (implies (natp n)
           (equal (nthcdr n (append a b))
                  (if (<= n (len a))
                      (append (nthcdr n a) b)
                    (nthcdr (- n (len a)) b)))))

Theorem: nthcdr-when-len

(defthm nthcdr-when-len
  (implies (equal n (len x))
           (list-equiv (nthcdr n x) nil)))