nthcdr

other

(in-package "ACL2")

local

(local (include-book "cdr"))

local

(local (include-book "len"))

in-theory

(in-theory (disable nthcdr))

nthcdr-of-constheorem

(defthm nthcdr-of-cons
  (equal (nthcdr n (cons a x))
    (if (zp n)
      (cons a x)
      (nthcdr (+ -1 n) x)))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-of-niltheorem

(defthm nthcdr-of-nil
  (equal (nthcdr n nil) nil)
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-of-0theorem

(defthm nthcdr-of-0
  (equal (nthcdr 0 x) x)
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-when-not-posptheorem

(defthm nthcdr-when-not-posp
  (implies (not (posp n)) (equal (nthcdr n x) x))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-when-not-consp-cheaptheorem

(defthm nthcdr-when-not-consp-cheap
  (implies (not (consp x))
    (equal (nthcdr n x)
      (if (zp n)
        x
        nil)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable nthcdr))))

len-of-nthcdrtheorem

(defthm len-of-nthcdr
  (equal (len (nthcdr n l)) (nfix (- (len l) (nfix n))))
  :hints (("Goal" :in-theory (enable zp nthcdr))))

acl2-count-of-nthcdr-weak-lineartheorem

(defthm acl2-count-of-nthcdr-weak-linear
  (<= (acl2-count (nthcdr n x)) (acl2-count x))
  :rule-classes ((:linear :trigger-terms ((acl2-count (nthcdr n x)))))
  :hints (("Goal" :in-theory (enable nthcdr))))

acl2-count-of-nthcdr-strong-lineartheorem

(defthm acl2-count-of-nthcdr-strong-linear
  (implies (and (consp x) (posp n))
    (< (acl2-count (nthcdr n x)) (acl2-count x)))
  :rule-classes ((:linear :trigger-terms ((acl2-count (nthcdr n x))))))

<=-of-len-of-nthcdr-lineartheorem

(defthm <=-of-len-of-nthcdr-linear
  (<= (len (nthcdr n x)) (len x))
  :rule-classes ((:linear :trigger-terms ((len (nthcdr n x)))))
  :hints (("Goal" :in-theory (enable nthcdr))))

<-of-len-of-nthcdr-lineartheorem

(defthm <-of-len-of-nthcdr-linear
  (implies (and (consp x) (posp n))
    (< (len (nthcdr n x)) (len x)))
  :rule-classes ((:linear :trigger-terms ((len (nthcdr n x)))))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-ifftheorem

(defthm nthcdr-iff
  (iff (nthcdr n x)
    (if (< (nfix n) (len x))
      t
      (if (equal (nfix n) (len x))
        (not (true-listp x))
        nil)))
  :hints (("Goal" :in-theory (enable nthcdr))))

local

(local (defthmd not-equal-when-<-of-lens
    (implies (< (len y) (len x)) (not (equal x y)))))

equal-of-nthcdr-sametheorem

(defthm equal-of-nthcdr-same
  (equal (equal x (nthcdr n x)) (or (zp n) (not x)))
  :hints (("Goal" :in-theory (enable nthcdr not-equal-when-<-of-lens))))

nthcdr-when-equal-of-lentheorem

(defthm nthcdr-when-equal-of-len
  (implies (and (equal (len x) k)
      (syntaxp (quotep k))
      (<= k n)
      (true-listp x)
      (integerp n))
    (equal (nthcdr n x) nil))
  :hints (("Goal" :in-theory (enable nthcdr))))

local

(local (defthm integerp-of-one-less
    (equal (integerp (+ -1 n))
      (or (not (acl2-numberp n)) (integerp n)))
    :hints (("Goal" :cases ((integerp n))))))

consp-of-nthcdrtheorem

(defthm consp-of-nthcdr
  (equal (consp (nthcdr n x)) (< (nfix n) (len x)))
  :hints (("Subgoal *1/2" :cases ((< n (+ 1 (len (cdr x)))))) ("Subgoal *1/1" :cases ((consp x)))
    ("Goal" :in-theory (enable nthcdr))))

cdr-of-nthcdrtheorem

(defthmd cdr-of-nthcdr
  (equal (cdr (nthcdr n x)) (nthcdr (+ 1 (nfix n)) x))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-opener-alttheorem

(defthmd nthcdr-opener-alt
  (implies (not (zp n))
    (equal (nthcdr n l) (cdr (nthcdr (+ -1 n) l))))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-opener-alt2theorem

(defthmd nthcdr-opener-alt2
  (implies (and (< n (len l)) (natp n))
    (equal (nthcdr n l) (cons (nth n l) (nthcdr (+ 1 n) l))))
  :hints (("goal" :induct (nthcdr n l) :in-theory (enable zp nthcdr))))

nthcdr-openertheorem

(defthmd nthcdr-opener
  (implies (not (zp n))
    (equal (nthcdr n l) (nthcdr (+ n -1) (cdr l))))
  :hints (("Goal" :in-theory (enable nthcdr))))

other

(theory-invariant (incompatible (:rewrite nthcdr-opener) (:rewrite |3-cdrs|)))

nthcdr-of-+-openertheorem

(defthmd nthcdr-of-+-opener
  (implies (and (syntaxp (quotep k)) (posp k) (natp n))
    (equal (nthcdr (+ k n) x) (cdr (nthcdr (+ (+ -1 k) n) x))))
  :hints (("Goal" :in-theory (enable cdr-of-nthcdr))))

other

(theory-invariant (incompatible (:rewrite nthcdr-of-+-opener)
    (:rewrite cdr-of-nthcdr)))

car-of-nthcdrtheorem

(defthm car-of-nthcdr
  (equal (car (nthcdr i x)) (nth i x))
  :hints (("Goal" :use (:instance nthcdr-opener-alt2 (n (nfix n))))))

nth-of-nthcdrtheorem

(defthm nth-of-nthcdr
  (equal (nth n (nthcdr m x)) (nth (+ (nfix n) (nfix m)) x))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-of-true-list-fixtheorem

(defthm nthcdr-of-true-list-fix
  (equal (nthcdr n (true-list-fix x))
    (true-list-fix (nthcdr n x)))
  :hints (("Goal" :in-theory (enable nthcdr))))

true-list-fix-of-nthcdrtheorem

(defthmd true-list-fix-of-nthcdr
  (equal (true-list-fix (nthcdr n x))
    (nthcdr n (true-list-fix x))))

other

(theory-invariant (incompatible (:rewrite true-list-fix-of-nthcdr)
    (:rewrite nthcdr-of-true-list-fix)))

3-cdrstheorem

(defthmd 3-cdrs
  (equal (cdr (cdr (cdr lst))) (nthcdr 3 lst)))

nthcdr-of-1theorem

(defthm nthcdr-of-1
  (equal (nthcdr 1 lst) (cdr lst))
  :hints (("Goal" :in-theory (enable nthcdr))))

equal-of-len-of-nthcdr-and-lentheorem

(defthm equal-of-len-of-nthcdr-and-len
  (implies (and (<= n (len x)))
    (equal (equal (len (nthcdr n x)) (len x)) (zp n))))

nthcdr-of-append-gentheorem

(defthm nthcdr-of-append-gen
  (equal (nthcdr n (append x y))
    (if (<= (len x) (nfix n))
      (nthcdr (- n (len x)) y)
      (append (nthcdr n x) y)))
  :hints (("Goal" :in-theory (enable nthcdr append))))

nthcdr-of-cdr-combinetheorem

(defthmd nthcdr-of-cdr-combine
  (implies (natp n)
    (equal (nthcdr n (cdr lst)) (nthcdr (+ 1 n) lst)))
  :hints (("Goal" :in-theory (enable nthcdr))))

other

(theory-invariant (incompatible (:definition nthcdr)
    (:rewrite nthcdr-of-cdr-combine)))

nthcdr-of-cdr-combine-strongtheorem

(defthmd nthcdr-of-cdr-combine-strong
  (equal (nthcdr n (cdr lst))
    (if (natp n)
      (nthcdr (+ 1 n) lst)
      (cdr lst)))
  :hints (("Goal" :in-theory (enable nthcdr))))

other

(theory-invariant (incompatible (:definition nthcdr)
    (:rewrite nthcdr-of-cdr-combine-strong)))

nthcdr-of-nthcdrtheorem

(defthm nthcdr-of-nthcdr
  (equal (nthcdr a (nthcdr b x))
    (nthcdr (+ (nfix a) (nfix b)) x))
  :hints (("Goal" :in-theory (enable nthcdr))))

cdr-of-cdr-becomes-nthcdrtheorem

(defthmd cdr-of-cdr-becomes-nthcdr
  (equal (cdr (cdr x)) (nthcdr 2 x))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-when-<-of-lentheorem

(defthmd nthcdr-when-<-of-len
  (implies (< (len x) (nfix n)) (equal (nthcdr n x) nil))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-is-niltheorem

(defthmd nthcdr-is-nil
  (implies (and (<= (len x) n) (integerp n) (true-listp x))
    (equal (nthcdr n x) nil)))

true-listp-of-nthcdr-2theorem

(defthm true-listp-of-nthcdr-2
  (equal (true-listp (nthcdr n x))
    (if (true-listp x)
      t
      (< (len x) (nfix n))))
  :hints (("Subgoal *1/5" :cases ((< (len x) n))) ("Goal" :in-theory (e/d (nthcdr)
        (nthcdr-of-cdr-combine-strong nthcdr-of-cdr-combine)))))

true-listp-of-nthcdr-3theorem

(defthm true-listp-of-nthcdr-3
  (equal (true-listp (nthcdr n x))
    (if (<= (nfix n) (len x))
      (true-listp x)
      t)))

nthcdr-last-onetheorem

(defthmd nthcdr-last-one
  (implies (and (equal (len x) (+ 1 n)) (natp n) (true-listp x))
    (equal (nthcdr n x) (list (nth n x))))
  :hints (("Goal" :in-theory (enable nthcdr))))

nthcdr-of-len-same-when-true-listptheorem

(defthm nthcdr-of-len-same-when-true-listp
  (implies (true-listp x) (equal (nthcdr (len x) x) nil)))

nth-sum-when-nthcdr-knowntheorem

(defthmd nth-sum-when-nthcdr-known
  (implies (and (equal vals2 (nthcdr m vals)) (natp n) (natp m))
    (equal (nth (+ m n) vals) (nth n vals2))))

equal-of-len-and-len-when-equal-of-nthcdr-and-nthcdrtheorem

(defthm equal-of-len-and-len-when-equal-of-nthcdr-and-nthcdr
  (implies (and (equal (nthcdr n x) (nthcdr n y))
      (or (< n (len x)) (< n (len y))))
    (equal (equal (len x) (len y)) t))
  :hints (("Goal" :in-theory (enable nthcdr))))

Included Books