Major Section: EVENTS

`Defcong`

is used to prove that one equivalence relation preserves
another in a given argument position of a given function.
Example:
(defcong set-equal iff (memb x y) 2)
is an abbreviation for
(defthm set-equal-implies-iff-memb-2
(implies (set-equal y y-equiv)
(iff (memb x y) (memb x y-equiv)))
:rule-classes (:congruence))

See congruence and also see equivalence.

General Form: (defcong equiv1 equiv2 term k :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :event-name event-name :doc doc)where

`equiv1`

and `equiv2`

are known equivalence relations, `term`

is a
call of a function `fn`

on the correct number of distinct variable
arguments `(fn x1 ... xn)`

, `k`

is a positive integer less than or equal
to the arity of `fn`

, and other arguments are as specified in the
documentation for `defthm`

. The `defcong`

macro expands into a call
of `defthm`

. The name of the `defthm`

event is
`equiv1-implies-equiv2-fn-k`

unless an `:event-name`

keyword argument is
supplied for the name. The term of the theorem is
(implies (equiv1 xk yk) (equiv2 (fn x1... xk ...xn) (fn x1... yk ...xn))).The rule-class

`:`

`congruence`

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 keyword arguments above.