• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Append

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)