Built-in axioms and theorems about bad atoms.
Definition:
(defaxiom booleanp-bad-atom<= (or (equal (bad-atom<= x y) t) (equal (bad-atom<= x y) nil)) :rule-classes :type-prescription)
Definition:
(defaxiom bad-atom<=-antisymmetric (implies (and (bad-atom x) (bad-atom y) (bad-atom<= x y) (bad-atom<= y x)) (equal x y)) :rule-classes nil)
Definition:
(defaxiom bad-atom<=-transitive (implies (and (bad-atom<= x y) (bad-atom<= y z) (bad-atom x) (bad-atom y) (bad-atom z)) (bad-atom<= x z)) :rule-classes ((:rewrite :match-free :all)))
Definition:
(defaxiom bad-atom<=-total (implies (and (bad-atom x) (bad-atom y)) (or (bad-atom<= x y) (bad-atom<= y x))) :rule-classes nil)
Theorem:
(defthm bad-atom-compound-recognizer (iff (bad-atom x) (not (or (consp x) (acl2-numberp x) (symbolp x) (characterp x) (stringp x)))) :rule-classes :compound-recognizer)