make-character-list

other

(in-package "ACL2")

in-theory

(in-theory (disable make-character-list))

character-listp-of-make-character-listtheorem

(defthm character-listp-of-make-character-list
  (character-listp (make-character-list x))
  :hints (("Goal" :in-theory (enable make-character-list))))

len-of-make-character-listtheorem

(defthm len-of-make-character-list
  (equal (len (make-character-list x)) (len x))
  :hints (("Goal" :in-theory (enable make-character-list))))

make-character-list-ifftheorem

(defthm make-character-list-iff
  (iff (make-character-list x) (consp x))
  :hints (("Goal" :in-theory (enable make-character-list))))

consp-of-make-character-listtheorem

(defthm consp-of-make-character-list
  (equal (consp (make-character-list x)) (consp x))
  :hints (("Goal" :in-theory (enable make-character-list))))

car-of-make-character-listtheorem

(defthm car-of-make-character-list
  (equal (car (make-character-list x))
    (if (not (consp x))
      nil
      (let ((car (first x)))
        (if (characterp car)
          car
          *null-char*))))
  :hints (("Goal" :in-theory (enable make-character-list))))

nth-of-make-character-listtheorem

(defthm nth-of-make-character-list
  (equal (nth n (make-character-list x))
    (if (<= (len x) (nfix n))
      nil
      (let ((char (nth n x)))
        (if (characterp char)
          char
          *null-char*))))
  :hints (("Goal" :in-theory (enable make-character-list (:i nth)))))