		Search-engine friendly clone of the ACL2 documentation.

Append-theorems

Some theorems about the built-in function append.

The theorem equal-of-appends-decompose is useful to decompose the equality of two appends into equalities of the appended lists, under the assumptions that the first two lists have the same length.

Definitions and Theorems

Theorem: equal-of-appends-decompose

(defthm equal-of-appends-decompose
  (implies (equal (len a) (len b))
           (equal (equal (append a a1) (append b b1))
                  (and (equal (true-list-fix a)
                              (true-list-fix b))
                       (equal a1 b1)))))

Theorem: append-when-not-consp-2

(defthm append-when-not-consp-2
  (implies (and (true-listp y) (not (consp y)))
           (equal (append x y) (true-list-fix x))))

Theorem: equal-of-append-and-left

(defthm equal-of-append-and-left
  (implies (and (true-listp a) (true-listp b))
           (equal (equal (append a b) a)
                  (not (consp b)))))