Fixing function for non-empty vl-bitlists.
(vl-bitlist-nonempty-fix x) → x-fix
This is just a technical helper function that supports the ACL2::fty-discipline. It is used to ensure that the
Function:
(defun vl-bitlist-nonempty-fix$inline (x) (declare (xargs :guard (vl-bitlist-p x))) (declare (xargs :guard (consp x))) (let ((__function__ 'vl-bitlist-nonempty-fix)) (declare (ignorable __function__)) (mbe :logic (if (atom x) (list :vl-0val) (vl-bitlist-fix x)) :exec x)))
Theorem:
(defthm vl-bitlist-p-of-vl-bitlist-nonempty-fix (b* ((x-fix (vl-bitlist-nonempty-fix$inline x))) (vl-bitlist-p x-fix)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-vl-bitlist-nonempty-fix (b* ((?x-fix (vl-bitlist-nonempty-fix$inline x))) (consp x-fix)) :rule-classes :type-prescription)
Theorem:
(defthm vl-bitlist-nonempty-fix-idempotent (b* ((?x-fix (vl-bitlist-nonempty-fix$inline x))) (implies (consp x) (equal x-fix (vl-bitlist-fix x)))))
Theorem:
(defthm vl-bitlist-nonempty-fix$inline-of-vl-bitlist-fix-x (equal (vl-bitlist-nonempty-fix$inline (vl-bitlist-fix x)) (vl-bitlist-nonempty-fix$inline x)))
Theorem:
(defthm vl-bitlist-nonempty-fix$inline-vl-bitlist-equiv-congruence-on-x (implies (vl-bitlist-equiv x x-equiv) (equal (vl-bitlist-nonempty-fix$inline x) (vl-bitlist-nonempty-fix$inline x-equiv))) :rule-classes :congruence)