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