Function:
(defun vl-distance-to-tab$inline (col tabsize) (declare (xargs :guard (and (natp col) (posp tabsize)))) (let ((__function__ 'vl-distance-to-tab)) (declare (ignorable __function__)) (mbe :logic (b* ((col (nfix col)) (tabsize (pos-fix tabsize))) (nfix (- tabsize (mod col tabsize)))) :exec (- tabsize (rem col tabsize)))))
Theorem:
(defthm natp-of-vl-distance-to-tab (b* ((distance (vl-distance-to-tab$inline col tabsize))) (natp distance)) :rule-classes :type-prescription)
Theorem:
(defthm vl-distance-to-tab$inline-of-nfix-col (equal (vl-distance-to-tab$inline (nfix col) tabsize) (vl-distance-to-tab$inline col tabsize)))
Theorem:
(defthm vl-distance-to-tab$inline-nat-equiv-congruence-on-col (implies (acl2::nat-equiv col col-equiv) (equal (vl-distance-to-tab$inline col tabsize) (vl-distance-to-tab$inline col-equiv tabsize))) :rule-classes :congruence)
Theorem:
(defthm vl-distance-to-tab$inline-of-pos-fix-tabsize (equal (vl-distance-to-tab$inline col (pos-fix tabsize)) (vl-distance-to-tab$inline col tabsize)))
Theorem:
(defthm vl-distance-to-tab$inline-pos-equiv-congruence-on-tabsize (implies (acl2::pos-equiv tabsize tabsize-equiv) (equal (vl-distance-to-tab$inline col tabsize) (vl-distance-to-tab$inline col tabsize-equiv))) :rule-classes :congruence)