		Search-engine friendly clone of the ACL2 documentation.

Built-in-theorems

Built-in-theorems-about-bad-atoms

Built-in theorems about bad atoms.

Definition: booleanp-bad-atom<=

(defaxiom booleanp-bad-atom<=
          (or (equal (bad-atom<= x y) t)
              (equal (bad-atom<= x y) nil))
          :rule-classes :type-prescription)

Definition: bad-atom<=-antisymmetric

(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: bad-atom<=-transitive

(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: bad-atom<=-total

(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: bad-atom-compound-recognizer

(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)