Function:
(defun vl-bit-to-sized-expr (x) (declare (xargs :guard (vl-bit-p x))) (let ((__function__ 'vl-bit-to-sized-expr)) (declare (ignorable __function__)) (case (vl-bit-fix x) (:vl-0val |*sized-1'b0*|) (:vl-1val |*sized-1'b1*|) (:vl-xval |*sized-1'bx*|) (otherwise |*sized-1'bz*|))))
Theorem:
(defthm vl-expr-p-of-vl-bit-to-sized-expr (b* ((bit-expr (vl-bit-to-sized-expr x))) (vl-expr-p bit-expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-bit-to-sized-expr-of-vl-bit-fix-x (equal (vl-bit-to-sized-expr (vl-bit-fix x)) (vl-bit-to-sized-expr x)))
Theorem:
(defthm vl-bit-to-sized-expr-vl-bit-equiv-congruence-on-x (implies (vl-bit-equiv x x-equiv) (equal (vl-bit-to-sized-expr x) (vl-bit-to-sized-expr x-equiv))) :rule-classes :congruence)