keyword-value-listp

other

(in-package "ACL2")

in-theory

(in-theory (disable keyword-value-listp))

keyword-value-listp-of-appendtheorem

(defthm keyword-value-listp-of-append
  (implies (and (keyword-value-listp x) (keyword-value-listp y))
    (keyword-value-listp (append x y)))
  :hints (("Goal" :in-theory (enable keyword-value-listp append))))

keyword-value-listp-of-cons-of-constheorem

(defthm keyword-value-listp-of-cons-of-cons
  (equal (keyword-value-listp (cons k (cons v keyword-value-list)))
    (and (keywordp k) (keyword-value-listp keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))

keyword-value-listp-of-assoc-keywordtheorem

(defthm keyword-value-listp-of-assoc-keyword
  (implies (keyword-value-listp keyword-value-list)
    (keyword-value-listp (assoc-keyword key keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))

keyword-value-listp-of-cddrtheorem

(defthm keyword-value-listp-of-cddr
  (implies (keyword-value-listp keyword-value-list)
    (keyword-value-listp (cddr keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))

keywordp-of-car-when-keyword-value-listptheorem

(defthm keywordp-of-car-when-keyword-value-listp
  (implies (keyword-value-listp keyword-value-list)
    (equal (keywordp (car keyword-value-list))
      (consp keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))