DEFCONG

prove congruence rule 
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.