		Search-engine friendly clone of the ACL2 documentation.

Std/lists/append

Lemmas about append available in the std/lists library.

Definitions and Theorems

Theorem: append-when-not-consp

(defthm append-when-not-consp
  (implies (not (consp x))
           (equal (append x y) y)))

Theorem: append-of-cons

(defthm append-of-cons
  (equal (append (cons a x) y)
         (cons a (append x y))))

Theorem: true-listp-of-append

(defthm true-listp-of-append
  (equal (true-listp (append x y))
         (true-listp y)))

Theorem: consp-of-append

(defthm consp-of-append
  (equal (consp (append x y))
         (or (consp x) (consp y))))

Theorem: append-under-iff

(defthm append-under-iff
  (iff (append x y) (or (consp x) y)))

Theorem: len-of-append

(defthm len-of-append
  (equal (len (append x y))
         (+ (len x) (len y))))

Theorem: equal-when-append-same

(defthm equal-when-append-same
  (equal (equal (append x y1) (append x y2))
         (equal y1 y2)))

Theorem: equal-of-append-and-append-same-arg2

(defthm equal-of-append-and-append-same-arg2
  (equal (equal (append x1 y) (append x2 y))
         (equal (true-list-fix x1)
                (true-list-fix x2))))

Theorem: append-of-nil

(defthm append-of-nil
  (equal (append x nil) (list-fix x)))

Theorem: list-fix-of-append

(defthm list-fix-of-append
  (equal (list-fix (append x y))
         (append x (list-fix y))))

Theorem: car-of-append

(defthm car-of-append
  (equal (car (append x y))
         (if (consp x) (car x) (car y))))

Theorem: car-of-append-when-consp

(defthm car-of-append-when-consp
  (implies (consp x)
           (equal (car (append x y)) (car x))))

Theorem: cdr-of-append

(defthm cdr-of-append
  (equal (cdr (append x y))
         (if (consp x)
             (append (cdr x) y)
           (cdr y))))

Theorem: cdr-of-append-when-consp

(defthm cdr-of-append-when-consp
  (implies (consp x)
           (equal (cdr (append x y))
                  (append (cdr x) y))))

Theorem: associativity-of-append

(defthm associativity-of-append
  (equal (append (append a b) c)
         (append a (append b c))))

Theorem: element-list-equiv-implies-element-list-equiv-append-1

(defthm element-list-equiv-implies-element-list-equiv-append-1
  (implies (element-list-equiv a a-equiv)
           (element-list-equiv (append a b)
                               (append a-equiv b)))
  :rule-classes (:congruence))

Theorem: element-list-equiv-implies-element-list-equiv-append-2

(defthm element-list-equiv-implies-element-list-equiv-append-2
  (implies (element-list-equiv b b-equiv)
           (element-list-equiv (append a b)
                               (append a b-equiv)))
  :rule-classes (:congruence))

Theorem: element-list-p-of-append-true-list

(defthm element-list-p-of-append-true-list
  (equal (element-list-p (append a b))
         (and (element-list-p (list-fix a))
              (element-list-p b)))
  :rule-classes :rewrite)