		Search-engine friendly clone of the ACL2 documentation.

Prefixp-theorems

Some theorems about the library function prefixp.

Definitions and Theorems

Theorem: same-car-when-prefixp-and-consp

(defthm same-car-when-prefixp-and-consp
  (implies (and (prefixp x y) (consp x))
           (equal (car x) (car y)))
  :rule-classes nil)

Theorem: same-take-when-prefixp-and-longer

(defthm same-take-when-prefixp-and-longer
  (implies (and (prefixp x y)
                (>= (len x) (nfix n)))
           (equal (take n x) (take n y)))
  :rule-classes nil)

Theorem: prefixp-of-cdr-cdr

(defthm prefixp-of-cdr-cdr
  (implies (and (prefixp x y) (consp x))
           (prefixp (cdr x) (cdr y))))

Theorem: prefixp-of-rcons

(defthm prefixp-of-rcons
  (equal (prefixp x (rcons a y))
         (or (list-equiv x (rcons a y))
             (prefixp x y))))

Theorem: prefixp-of-butlast-1-right

(defthm prefixp-of-butlast-1-right
  (equal (prefixp x (butlast y 1))
         (and (prefixp x y)
              (or (not (consp y))
                  (not (list-equiv x y))))))