Fixing function for fgl-binder-rule structures.
(fgl-binder-rule-fix x) → new-x
Function:
(defun fgl-binder-rule-fix$inline (x) (declare (xargs :guard (fgl-binder-rule-p x))) (let ((__function__ 'fgl-binder-rule-fix)) (declare (ignorable __function__)) (mbe :logic (case (fgl-binder-rule-kind x) (:brewrite (b* ((rune (fgl-binder-rune-fix (car (car (cdr x))))) (lhs-fn (pseudo-fnsym-fix (car (cdr (car (cdr x)))))) (lhs-args (pseudo-term-list-fix (cdr (cdr (car (cdr x)))))) (hyps (pseudo-term-list-fix (car (car (cdr (cdr x)))))) (rhs (pseudo-term-fix (cdr (car (cdr (cdr x)))))) (equiv (pseudo-fnsym-fix (car (cdr (cdr (cdr x)))))) (r-equiv (pseudo-fnsym-fix (cdr (cdr (cdr (cdr x))))))) (cons :brewrite (cons (cons rune (cons lhs-fn lhs-args)) (cons (cons hyps rhs) (cons equiv r-equiv)))))) (:bmeta (b* ((name (pseudo-fnsym-fix (std::da-nth 0 (cdr x))))) (cons :bmeta (list name))))) :exec x)))
Theorem:
(defthm fgl-binder-rule-p-of-fgl-binder-rule-fix (b* ((new-x (fgl-binder-rule-fix$inline x))) (fgl-binder-rule-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm fgl-binder-rule-fix-when-fgl-binder-rule-p (implies (fgl-binder-rule-p x) (equal (fgl-binder-rule-fix x) x)))
Function:
(defun fgl-binder-rule-equiv$inline (x y) (declare (xargs :guard (and (fgl-binder-rule-p x) (fgl-binder-rule-p y)))) (equal (fgl-binder-rule-fix x) (fgl-binder-rule-fix y)))
Theorem:
(defthm fgl-binder-rule-equiv-is-an-equivalence (and (booleanp (fgl-binder-rule-equiv x y)) (fgl-binder-rule-equiv x x) (implies (fgl-binder-rule-equiv x y) (fgl-binder-rule-equiv y x)) (implies (and (fgl-binder-rule-equiv x y) (fgl-binder-rule-equiv y z)) (fgl-binder-rule-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm fgl-binder-rule-equiv-implies-equal-fgl-binder-rule-fix-1 (implies (fgl-binder-rule-equiv x x-equiv) (equal (fgl-binder-rule-fix x) (fgl-binder-rule-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm fgl-binder-rule-fix-under-fgl-binder-rule-equiv (fgl-binder-rule-equiv (fgl-binder-rule-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-fgl-binder-rule-fix-1-forward-to-fgl-binder-rule-equiv (implies (equal (fgl-binder-rule-fix x) y) (fgl-binder-rule-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-fgl-binder-rule-fix-2-forward-to-fgl-binder-rule-equiv (implies (equal x (fgl-binder-rule-fix y)) (fgl-binder-rule-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm fgl-binder-rule-equiv-of-fgl-binder-rule-fix-1-forward (implies (fgl-binder-rule-equiv (fgl-binder-rule-fix x) y) (fgl-binder-rule-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm fgl-binder-rule-equiv-of-fgl-binder-rule-fix-2-forward (implies (fgl-binder-rule-equiv x (fgl-binder-rule-fix y)) (fgl-binder-rule-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm fgl-binder-rule-kind$inline-of-fgl-binder-rule-fix-x (equal (fgl-binder-rule-kind$inline (fgl-binder-rule-fix x)) (fgl-binder-rule-kind$inline x)))
Theorem:
(defthm fgl-binder-rule-kind$inline-fgl-binder-rule-equiv-congruence-on-x (implies (fgl-binder-rule-equiv x x-equiv) (equal (fgl-binder-rule-kind$inline x) (fgl-binder-rule-kind$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-fgl-binder-rule-fix (consp (fgl-binder-rule-fix x)) :rule-classes :type-prescription)