		Search-engine friendly clone of the ACL2 documentation.

Defequal-event-generation

Defequal-gen-theory-invariant

Generate the theory invariant.

Signature
(defequal-gen-theory-invariant left-to-right right-to-left) → even
Arguments: left-to-right — Guard (symbolp left-to-right).; right-to-left — Guard (symbolp right-to-left).
Returns: even — Type (pseudo-event-formp even).

Definitions and Theorems

Function: defequal-gen-theory-invariant

(defun defequal-gen-theory-invariant (left-to-right right-to-left)
  (declare (xargs :guard (and (symbolp left-to-right)
                              (symbolp right-to-left))))
  (let ((__function__ 'defequal-gen-theory-invariant))
    (declare (ignorable __function__))
    (cons 'theory-invariant
          (cons (cons 'incompatible
                      (cons (cons ':rewrite
                                  (cons left-to-right 'nil))
                            (cons (cons ':rewrite
                                        (cons right-to-left 'nil))
                                  'nil)))
                'nil))))

Theorem: pseudo-event-formp-of-defequal-gen-theory-invariant

(defthm pseudo-event-formp-of-defequal-gen-theory-invariant
 (b*
  ((even
       (defequal-gen-theory-invariant left-to-right right-to-left)))
  (pseudo-event-formp even))
 :rule-classes :rewrite)