msgp - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable msgp))

msgp-compound-recognizertheorem

(defthm msgp-compound-recognizer
  (if (msgp x)
    (or (stringp x) (and (consp x) (true-listp x)))
    (not (stringp x)))
  :rule-classes :compound-recognizer :hints (("Goal" :in-theory (enable msgp))))

msgp-of-constheorem

(defthm msgp-of-cons
  (equal (msgp (cons str alist))
    (and (stringp str) (character-alistp alist)))
  :hints (("Goal" :in-theory (enable msgp))))