DEFEQUIV

prove that a function is an equivalence relation 
Major Section:  EVENTS


Example:
(defequiv set-equal)

is an abbreviation for
(defthm set-equal-is-an-equivalence
  (and (booleanp (set-equal x y))
       (set-equal x x)
       (implies (set-equal x y) (set-equal y x))
       (implies (and (set-equal x y)
                     (set-equal y z))
                (set-equal x z)))
  :rule-classes (:equivalence))
See equivalence. 

General Form:
(defequiv fn
  :rule-classes rule-classes
  :instructions instructions
  :hints hints
  :otf-flg otf-flg
  :event-name event-name
  :doc doc)
where fn is a function symbol of arity 2, event-name, if supplied, is a symbol, and all other arguments are as specified in the documentation for defthm. The defequiv macro expands into a call of defthm. The name of the defthm is fn-is-an-equivalence, unless event-name is supplied, in which case event-name is the name used. The term generated for the defthm event states that fn is Boolean, reflexive, symmetric, and transitive. The rule-class :equivalence is added to the rule-classes specified, if it is not already there. All other arguments to the generated defthm form are as specified by the other keyword arguments above.