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