(vl-clocking-block-item-fix x) is a fty fixing function.
(vl-clocking-block-item-fix x) → fty::newx
Note that in the execution this is just an inline identity function.
Function:
(defun vl-clocking-block-item-fix$inline (x) (declare (xargs :guard (vl-clocking-block-item-p x))) (let ((__function__ 'vl-clocking-block-item-fix)) (declare (ignorable __function__)) (mbe :logic (common-lisp::case (tag x) ((:vl-defaultskew) (vl-defaultskew-item-fix x)) ((:vl-clkassign) (vl-clkassign-fix x)) ((:vl-property) (vl-property-fix x)) (otherwise (vl-sequence-fix x))) :exec x)))
Theorem:
(defthm vl-clocking-block-item-p-of-vl-clocking-block-item-fix (b* ((fty::newx (vl-clocking-block-item-fix$inline x))) (vl-clocking-block-item-p fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm vl-clocking-block-item-fix-when-vl-clocking-block-item-p (implies (vl-clocking-block-item-p x) (equal (vl-clocking-block-item-fix x) x)))
Function:
(defun vl-clocking-block-item-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (vl-clocking-block-item-p acl2::x) (vl-clocking-block-item-p acl2::y)))) (equal (vl-clocking-block-item-fix acl2::x) (vl-clocking-block-item-fix acl2::y)))
Theorem:
(defthm vl-clocking-block-item-equiv-is-an-equivalence (and (booleanp (vl-clocking-block-item-equiv x y)) (vl-clocking-block-item-equiv x x) (implies (vl-clocking-block-item-equiv x y) (vl-clocking-block-item-equiv y x)) (implies (and (vl-clocking-block-item-equiv x y) (vl-clocking-block-item-equiv y z)) (vl-clocking-block-item-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm vl-clocking-block-item-equiv-implies-equal-vl-clocking-block-item-fix-1 (implies (vl-clocking-block-item-equiv acl2::x x-equiv) (equal (vl-clocking-block-item-fix acl2::x) (vl-clocking-block-item-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-clocking-block-item-fix-under-vl-clocking-block-item-equiv (vl-clocking-block-item-equiv (vl-clocking-block-item-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-vl-clocking-block-item-fix-1-forward-to-vl-clocking-block-item-equiv (implies (equal (vl-clocking-block-item-fix acl2::x) acl2::y) (vl-clocking-block-item-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-vl-clocking-block-item-fix-2-forward-to-vl-clocking-block-item-equiv (implies (equal acl2::x (vl-clocking-block-item-fix acl2::y)) (vl-clocking-block-item-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm vl-clocking-block-item-equiv-of-vl-clocking-block-item-fix-1-forward (implies (vl-clocking-block-item-equiv (vl-clocking-block-item-fix acl2::x) acl2::y) (vl-clocking-block-item-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm vl-clocking-block-item-equiv-of-vl-clocking-block-item-fix-2-forward (implies (vl-clocking-block-item-equiv acl2::x (vl-clocking-block-item-fix acl2::y)) (vl-clocking-block-item-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm tag-of-vl-clocking-block-item-fix-forward (or (equal (tag (vl-clocking-block-item-fix x)) :vl-defaultskew) (equal (tag (vl-clocking-block-item-fix x)) :vl-clkassign) (equal (tag (vl-clocking-block-item-fix x)) :vl-property) (equal (tag (vl-clocking-block-item-fix x)) :vl-sequence)) :rule-classes ((:forward-chaining :trigger-terms ((tag (vl-clocking-block-item-fix x))))))