		Search-engine friendly clone of the ACL2 documentation.

Std/alists/strip-cdrs

Lemmas about strip-cdrs available in the std/alists library.

Note that strip-cdrs is a "traditional" alist function: it has an alistp guard and fails to respect the non-alist convention. We generally prefer to work with alist-vals instead.

Even so, we provide many lemmas for working with strip-cdrs, in case for some reason that's what you want to do.

Definitions and Theorems

Theorem: strip-cdrs-when-atom

(defthm strip-cdrs-when-atom
  (implies (atom x)
           (equal (strip-cdrs x) nil)))

Theorem: strip-cdrs-of-cons

(defthm strip-cdrs-of-cons
  (equal (strip-cdrs (cons a x))
         (cons (cdr a) (strip-cdrs x))))

Theorem: len-of-strip-cdrs

(defthm len-of-strip-cdrs
  (equal (len (strip-cdrs x)) (len x)))

Theorem: consp-of-strip-cdrs

(defthm consp-of-strip-cdrs
  (equal (consp (strip-cdrs x))
         (consp x)))

Theorem: car-of-strip-cdrs

(defthm car-of-strip-cdrs
  (equal (car (strip-cdrs x))
         (cdr (car x))))

Theorem: cdr-of-strip-cdrs

(defthm cdr-of-strip-cdrs
  (equal (cdr (strip-cdrs x))
         (strip-cdrs (cdr x))))

Theorem: strip-cdrs-under-iff

(defthm strip-cdrs-under-iff
  (iff (strip-cdrs x) (consp x)))

Theorem: strip-cdrs-of-list-fix

(defthm strip-cdrs-of-list-fix
  (equal (strip-cdrs (list-fix x))
         (strip-cdrs x)))

Theorem: list-equiv-implies-equal-strip-cdrs-1

(defthm list-equiv-implies-equal-strip-cdrs-1
  (implies (list-equiv x x-equiv)
           (equal (strip-cdrs x)
                  (strip-cdrs x-equiv)))
  :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-strip-cdrs-1

(defthm set-equiv-implies-set-equiv-strip-cdrs-1
  (implies (set-equiv x x-equiv)
           (set-equiv (strip-cdrs x)
                      (strip-cdrs x-equiv)))
  :rule-classes (:congruence))

Theorem: strip-cdrs-of-append

(defthm strip-cdrs-of-append
  (equal (strip-cdrs (append x y))
         (append (strip-cdrs x) (strip-cdrs y))))

Theorem: strip-cdrs-of-rev

(defthm strip-cdrs-of-rev
  (equal (strip-cdrs (rev x))
         (rev (strip-cdrs x))))

Theorem: strip-cdrs-of-revappend

(defthm strip-cdrs-of-revappend
  (equal (strip-cdrs (revappend x y))
         (revappend (strip-cdrs x)
                    (strip-cdrs y))))

Theorem: strip-cdrs-of-repeat

(defthm strip-cdrs-of-repeat
  (equal (strip-cdrs (repeat n x))
         (repeat n (cdr x))))

Theorem: strip-cdrs-of-take

(defthm strip-cdrs-of-take
  (equal (strip-cdrs (take n x))
         (take n (strip-cdrs x))))

Theorem: strip-cdrs-of-nthcdr

(defthm strip-cdrs-of-nthcdr
  (equal (strip-cdrs (nthcdr n x))
         (nthcdr n (strip-cdrs x))))

Theorem: strip-cdrs-of-last

(defthm strip-cdrs-of-last
  (equal (strip-cdrs (last x))
         (last (strip-cdrs x))))

Theorem: strip-cdrs-of-butlast

(defthm strip-cdrs-of-butlast
  (equal (strip-cdrs (butlast x n))
         (butlast (strip-cdrs x) n)))

Theorem: strip-cdrs-of-pairlis$

(defthm strip-cdrs-of-pairlis$
  (equal (strip-cdrs (pairlis$ x y))
         (take (len x) y)))