Fixing function for svtv-data-obj structures.
(svtv-data-obj-fix x) → new-x
Function:
(defun svtv-data-obj-fix$inline (x) (declare (xargs :guard (svtv-data-obj-p x))) (let ((__function__ 'svtv-data-obj-fix)) (declare (ignorable __function__)) (mbe :logic (b* ((design (design-fix (std::da-nth 0 x))) (user-names (svtv-namemap-fix (std::da-nth 1 x))) (namemap (svtv-name-lhs-map-fix (std::da-nth 2 x))) (namemap-validp (bool-fix (std::da-nth 3 x))) (flatten (flatten-res-fix (std::da-nth 4 x))) (flatten-validp (bool-fix (std::da-nth 5 x))) (flatnorm-setup (flatnorm-setup-fix (std::da-nth 6 x))) (flatnorm (flatnorm-res-fix (std::da-nth 7 x))) (flatnorm-validp (bool-fix (std::da-nth 8 x))) (phase-fsm-setup (phase-fsm-config-fix (std::da-nth 9 x))) (phase-fsm (fsm-fix (std::da-nth 10 x))) (phase-fsm-validp (bool-fix (std::da-nth 11 x))) (cycle-phases (svtv-cyclephaselist-fix (std::da-nth 12 x))) (cycle-fsm (fsm-fix (std::da-nth 13 x))) (cycle-fsm-validp (bool-fix (std::da-nth 14 x))) (pipeline-setup (pipeline-setup-fix (std::da-nth 15 x))) (pipeline (svex-alist-fix (std::da-nth 16 x))) (pipeline-validp (bool-fix (std::da-nth 17 x)))) (list design user-names namemap namemap-validp flatten flatten-validp flatnorm-setup flatnorm flatnorm-validp phase-fsm-setup phase-fsm phase-fsm-validp cycle-phases cycle-fsm cycle-fsm-validp pipeline-setup pipeline pipeline-validp)) :exec x)))
Theorem:
(defthm svtv-data-obj-p-of-svtv-data-obj-fix (b* ((new-x (svtv-data-obj-fix$inline x))) (svtv-data-obj-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm svtv-data-obj-fix-when-svtv-data-obj-p (implies (svtv-data-obj-p x) (equal (svtv-data-obj-fix x) x)))
Function:
(defun svtv-data-obj-equiv$inline (x y) (declare (xargs :guard (and (svtv-data-obj-p x) (svtv-data-obj-p y)))) (equal (svtv-data-obj-fix x) (svtv-data-obj-fix y)))
Theorem:
(defthm svtv-data-obj-equiv-is-an-equivalence (and (booleanp (svtv-data-obj-equiv x y)) (svtv-data-obj-equiv x x) (implies (svtv-data-obj-equiv x y) (svtv-data-obj-equiv y x)) (implies (and (svtv-data-obj-equiv x y) (svtv-data-obj-equiv y z)) (svtv-data-obj-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm svtv-data-obj-equiv-implies-equal-svtv-data-obj-fix-1 (implies (svtv-data-obj-equiv x x-equiv) (equal (svtv-data-obj-fix x) (svtv-data-obj-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svtv-data-obj-fix-under-svtv-data-obj-equiv (svtv-data-obj-equiv (svtv-data-obj-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-svtv-data-obj-fix-1-forward-to-svtv-data-obj-equiv (implies (equal (svtv-data-obj-fix x) y) (svtv-data-obj-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-svtv-data-obj-fix-2-forward-to-svtv-data-obj-equiv (implies (equal x (svtv-data-obj-fix y)) (svtv-data-obj-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm svtv-data-obj-equiv-of-svtv-data-obj-fix-1-forward (implies (svtv-data-obj-equiv (svtv-data-obj-fix x) y) (svtv-data-obj-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm svtv-data-obj-equiv-of-svtv-data-obj-fix-2-forward (implies (svtv-data-obj-equiv x (svtv-data-obj-fix y)) (svtv-data-obj-equiv x y)) :rule-classes :forward-chaining)