(n-output-comb-transform-fix x) is a ACL2::fty fixing function.
(n-output-comb-transform-fix x) → fty::newx
Note that in the execution this is just an inline identity function.
Function:
(defun n-output-comb-transform-fix$inline (x) (declare (xargs :guard (n-output-comb-transform-p x))) (let ((__function__ 'n-output-comb-transform-fix)) (declare (ignorable __function__)) (mbe :logic (case (tag x) ((:n-outputs-unreachability-config) (n-outputs-unreachability-config-fix x)) ((:n-outputs-dom-supergates-sweep-config) (n-outputs-dom-supergates-sweep-config-fix x)) (otherwise (comb-transform-fix x))) :exec x)))
Theorem:
(defthm n-output-comb-transform-p-of-n-output-comb-transform-fix (b* ((fty::newx (n-output-comb-transform-fix$inline x))) (n-output-comb-transform-p fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm n-output-comb-transform-fix-when-n-output-comb-transform-p (implies (n-output-comb-transform-p x) (equal (n-output-comb-transform-fix x) x)))
Function:
(defun n-output-comb-transform-equiv$inline (x acl2::y) (declare (xargs :guard (and (n-output-comb-transform-p x) (n-output-comb-transform-p acl2::y)))) (equal (n-output-comb-transform-fix x) (n-output-comb-transform-fix acl2::y)))
Theorem:
(defthm n-output-comb-transform-equiv-is-an-equivalence (and (booleanp (n-output-comb-transform-equiv x y)) (n-output-comb-transform-equiv x x) (implies (n-output-comb-transform-equiv x y) (n-output-comb-transform-equiv y x)) (implies (and (n-output-comb-transform-equiv x y) (n-output-comb-transform-equiv y z)) (n-output-comb-transform-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm n-output-comb-transform-equiv-implies-equal-n-output-comb-transform-fix-1 (implies (n-output-comb-transform-equiv x x-equiv) (equal (n-output-comb-transform-fix x) (n-output-comb-transform-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm n-output-comb-transform-fix-under-n-output-comb-transform-equiv (n-output-comb-transform-equiv (n-output-comb-transform-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-n-output-comb-transform-fix-1-forward-to-n-output-comb-transform-equiv (implies (equal (n-output-comb-transform-fix x) acl2::y) (n-output-comb-transform-equiv x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-n-output-comb-transform-fix-2-forward-to-n-output-comb-transform-equiv (implies (equal x (n-output-comb-transform-fix acl2::y)) (n-output-comb-transform-equiv x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm n-output-comb-transform-equiv-of-n-output-comb-transform-fix-1-forward (implies (n-output-comb-transform-equiv (n-output-comb-transform-fix x) acl2::y) (n-output-comb-transform-equiv x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm n-output-comb-transform-equiv-of-n-output-comb-transform-fix-2-forward (implies (n-output-comb-transform-equiv x (n-output-comb-transform-fix acl2::y)) (n-output-comb-transform-equiv x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm tag-of-n-output-comb-transform-fix-forward (or (equal (tag (n-output-comb-transform-fix x)) :n-outputs-unreachability-config) (equal (tag (n-output-comb-transform-fix x)) :n-outputs-dom-supergates-sweep-config) (equal (tag (n-output-comb-transform-fix x)) :balance-config) (equal (tag (n-output-comb-transform-fix x)) :fraig-config) (equal (tag (n-output-comb-transform-fix x)) :rewrite-config) (equal (tag (n-output-comb-transform-fix x)) :abc-comb-simp-config) (equal (tag (n-output-comb-transform-fix x)) :obs-constprop-config) (equal (tag (n-output-comb-transform-fix x)) :observability-config) (equal (tag (n-output-comb-transform-fix x)) :constprop-config) (equal (tag (n-output-comb-transform-fix x)) :snapshot-config) (equal (tag (n-output-comb-transform-fix x)) :prune-config) (equal (tag (n-output-comb-transform-fix x)) :unreachability-config) (equal (tag (n-output-comb-transform-fix x)) :dom-supergates-sweep-config)) :rule-classes ((:forward-chaining :trigger-terms ((tag (n-output-comb-transform-fix x))))))