Given a variable and a size in bits, create an LHS that covers those bits.
(sv::svar->lhs-by-size acl2::x sv::size) → sv::lhs
Function:
(defun sv::svar->lhs-by-size (acl2::x sv::size) (declare (xargs :guard (and (sv::svar-p acl2::x) (natp sv::size)))) (let ((__function__ 'sv::svar->lhs-by-size)) (declare (ignorable __function__)) (if (mbe :logic (zp sv::size) :exec (eql sv::size 0)) nil (list (sv::make-lhrange :w sv::size :atom (sv::make-lhatom-var :name acl2::x :rsh 0))))))
Theorem:
(defthm sv::lhs-p-of-svar->lhs-by-size (b* ((sv::lhs (sv::svar->lhs-by-size acl2::x sv::size))) (sv::lhs-p sv::lhs)) :rule-classes :rewrite)
Theorem:
(defthm sv::vars-of-svar->lhs-by-size (implies (not (equal sv::v (sv::svar-fix acl2::x))) (not (member sv::v (sv::lhs-vars (sv::svar->lhs-by-size acl2::x sv::size))))))
Theorem:
(defthm sv::svar->lhs-by-size-of-svar-fix-x (equal (sv::svar->lhs-by-size (sv::svar-fix acl2::x) sv::size) (sv::svar->lhs-by-size acl2::x sv::size)))
Theorem:
(defthm sv::svar->lhs-by-size-svar-equiv-congruence-on-x (implies (sv::svar-equiv acl2::x sv::x-equiv) (equal (sv::svar->lhs-by-size acl2::x sv::size) (sv::svar->lhs-by-size sv::x-equiv sv::size))) :rule-classes :congruence)
Theorem:
(defthm sv::svar->lhs-by-size-of-nfix-size (equal (sv::svar->lhs-by-size acl2::x (nfix sv::size)) (sv::svar->lhs-by-size acl2::x sv::size)))
Theorem:
(defthm sv::svar->lhs-by-size-nat-equiv-congruence-on-size (implies (acl2::nat-equiv sv::size sv::size-equiv) (equal (sv::svar->lhs-by-size acl2::x sv::size) (sv::svar->lhs-by-size acl2::x sv::size-equiv))) :rule-classes :congruence)