		Search-engine friendly clone of the ACL2 documentation.

Builtin-defaxioms/defthms-by-rule-classes

Builtin-defaxioms/defthms-of-class-equivalence

Built-in axioms and theorems of the :equivalence rule class.

Theorem: fn-equal-is-an-equivalence

(defthm fn-equal-is-an-equivalence
  (and (booleanp (fn-equal x y))
       (fn-equal x x)
       (implies (fn-equal x y) (fn-equal y x))
       (implies (and (fn-equal x y) (fn-equal y z))
                (fn-equal x z)))
  :rule-classes (:equivalence))

Theorem: iff-is-an-equivalence

(defthm iff-is-an-equivalence
  (and (booleanp (iff x y))
       (iff x x)
       (implies (iff x y) (iff y x))
       (implies (and (iff x y) (iff y z))
                (iff x z)))
  :rule-classes (:equivalence))