Prefix and remainder theorems for vl-read-decimal-base, automatically generated by def-prefix/remainder-thms.
Theorem:
(defthm prefix-of-vl-read-decimal-base (and (true-listp (mv-nth 0 (vl-read-decimal-base echars))) (implies (force (vl-echarlist-p echars)) (vl-echarlist-p (mv-nth 0 (vl-read-decimal-base echars))))) :rule-classes ((:rewrite) (:type-prescription :corollary (true-listp (mv-nth 0 (vl-read-decimal-base echars))))))
Theorem:
(defthm remainder-of-vl-read-decimal-base (and (equal (true-listp (mv-nth 1 (vl-read-decimal-base echars))) (true-listp echars)) (implies (force (vl-echarlist-p echars)) (vl-echarlist-p (mv-nth 1 (vl-read-decimal-base echars))))) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp echars) (true-listp (mv-nth 1 (vl-read-decimal-base echars)))))))
Theorem:
(defthm append-of-vl-read-decimal-base (equal (append (mv-nth 0 (vl-read-decimal-base echars)) (mv-nth 1 (vl-read-decimal-base echars))) echars))
Theorem:
(defthm no-change-loser-of-vl-read-decimal-base (implies (not (mv-nth 0 (vl-read-decimal-base echars))) (equal (mv-nth 1 (vl-read-decimal-base echars)) echars)))
Theorem:
(defthm acl2-count-of-vl-read-decimal-base-weak (<= (acl2-count (mv-nth 1 (vl-read-decimal-base echars))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-read-decimal-base-strong (implies (mv-nth 0 (vl-read-decimal-base echars)) (< (acl2-count (mv-nth 1 (vl-read-decimal-base echars))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))