character-listp - ACL2 Book

other

(in-package "ACL2")

character-listp-of-cdrtheorem

(defthm character-listp-of-cdr
  (implies (character-listp x) (character-listp (cdr x)))
  :hints (("Goal" :in-theory (enable character-listp))))

characterp-of-car-when-character-listp-strongtheorem

(defthm characterp-of-car-when-character-listp-strong
  (implies (character-listp x)
    (equal (characterp (car x)) (consp x)))
  :hints (("Goal" :in-theory (enable character-listp))))

character-listp-of-append-2theorem

(defthm character-listp-of-append-2
  (equal (character-listp (append x y))
    (and (character-listp (true-list-fix x))
      (character-listp y)))
  :hints (("Goal" :in-theory (enable character-listp))))

character-listp-of-revappendtheorem

(defthm character-listp-of-revappend
  (equal (character-listp (revappend x y))
    (and (character-listp (true-list-fix x))
      (character-listp y))))

character-listp-of-reversetheorem

(defthm character-listp-of-reverse
  (implies (true-listp x)
    (equal (character-listp (reverse x)) (character-listp x))))

character-listp-of-true-list-fixtheorem

(defthm character-listp-of-true-list-fix
  (implies (character-listp lst)
    (character-listp (true-list-fix lst)))
  :hints (("Goal" :in-theory (enable character-listp))))

character-listp-of-first-n-actheorem

(defthm character-listp-of-first-n-ac
  (implies (and (character-listp l) (true-listp ac) (<= i (len l)))
    (equal (character-listp (first-n-ac i l ac))
      (character-listp ac)))
  :hints (("Goal" :in-theory (enable character-listp take true-listp))))

character-listp-of-taketheorem

(defthm character-listp-of-take
  (implies (character-listp (double-rewrite x))
    (iff (character-listp (take n x))
      (or (characterp nil) (<= (nfix n) (len x))))))

character-listp-of-nthcdrtheorem

(defthm character-listp-of-nthcdr
  (implies (character-listp (double-rewrite x))
    (character-listp (nthcdr n x)))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (enable nthcdr character-listp))))

character-listp-of-constheorem

(defthm character-listp-of-cons
  (equal (character-listp (cons a x))
    (and (characterp a) (character-listp x)))
  :rule-classes ((:rewrite))
  :hints (("Goal" :in-theory (enable character-listp))))

character-listp-of-substitute-actheorem

(defthm character-listp-of-substitute-ac
  (implies (and (characterp new)
      (characterp old)
      (character-listp seq)
      (character-listp acc))
    (character-listp (substitute-ac new old seq acc))))

true-listp-when-character-listp2theorem

(defthmd true-listp-when-character-listp2
  (implies (character-listp x) (true-listp x)))

character-listp-of-member-equaltheorem

(defthm character-listp-of-member-equal
  (implies (character-listp x)
    (character-listp (member-equal a x)))
  :hints (("Goal" :in-theory (enable character-listp))))