Explode a
(vl-msb-bitslice-constint x) → bit-exprs
We require that
Function:
(defun vl-msb-bitslice-constint (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (and (vl-atom-p x) (vl-atom-welltyped-p x) (vl-fast-constint-p (vl-atom->guts x))))) (let ((__function__ 'vl-msb-bitslice-constint)) (declare (ignorable __function__)) (vl-msb-bitslice-constint-aux (vl-atom->finalwidth x) (vl-constint->value (vl-atom->guts x)) nil)))
Theorem:
(defthm vl-exprlist-p-of-vl-msb-bitslice-constint (b* ((bit-exprs (vl-msb-bitslice-constint x))) (vl-exprlist-p bit-exprs)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-bitslice-constint (true-listp (vl-msb-bitslice-constint x)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-msb-bitslice-constint (equal (len (vl-msb-bitslice-constint x)) (nfix (vl-atom->finalwidth x))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-constint (equal (vl-exprlist->finalwidths (vl-msb-bitslice-constint x)) (replicate (vl-atom->finalwidth x) 1)))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-constint (equal (vl-exprlist->finaltypes (vl-msb-bitslice-constint x)) (replicate (vl-atom->finalwidth x) :vl-unsigned)))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-constint (vl-exprlist-welltyped-p (vl-msb-bitslice-constint x)))
Theorem:
(defthm vl-msb-bitslice-constint-of-vl-expr-fix-x (equal (vl-msb-bitslice-constint (vl-expr-fix x)) (vl-msb-bitslice-constint x)))
Theorem:
(defthm vl-msb-bitslice-constint-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-msb-bitslice-constint x) (vl-msb-bitslice-constint x-equiv))) :rule-classes :congruence)