Function:
(defun svtv-parse-path/select (x) (declare (xargs :guard (stringp x))) (let ((__function__ 'svtv-parse-path/select)) (declare (ignorable __function__)) (b* ((dotted-parts (strtok x '(#\.)))) (svtv-parse-path/select-aux dotted-parts x))))
Theorem:
(defthm return-type-of-svtv-parse-path/select.path (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select x))) (implies (not errmsg) (path-p path))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-svtv-parse-path/select.range-msb (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select x))) (or (not range-msb) (natp range-msb))) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-svtv-parse-path/select.range-lsb (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select x))) (implies range-msb (natp range-lsb))) :rule-classes :type-prescription)
Theorem:
(defthm svtv-parse-path/select-of-str-fix-x (equal (svtv-parse-path/select (str-fix x)) (svtv-parse-path/select x)))
Theorem:
(defthm svtv-parse-path/select-streqv-congruence-on-x (implies (acl2::streqv x x-equiv) (equal (svtv-parse-path/select x) (svtv-parse-path/select x-equiv))) :rule-classes :congruence)