Token and remainder theorems for vl-lex-token1, automatically generated by def-token/remainder-thms.
Theorem:
(defthm vl-token-p-of-vl-lex-token1 (implies (and (force (vl-echarlist-p echars)) (and (force (consp echars)) (force (equal char1 (vl-echar->char (car echars)))) (force (vl-lexstate-p st)))) (equal (vl-token-p (mv-nth 0 (vl-lex-token1 char1 echars st warnings))) (if (mv-nth 0 (vl-lex-token1 char1 echars st warnings)) t nil))))
Theorem:
(defthm true-listp-of-vl-lex-token1 (equal (true-listp (mv-nth 1 (vl-lex-token1 char1 echars st warnings))) (true-listp echars)) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp echars) (true-listp (mv-nth 1 (vl-lex-token1 char1 echars st warnings)))))))
Theorem:
(defthm vl-echarlist-p-of-vl-lex-token1 (implies (force (vl-echarlist-p echars)) (equal (vl-echarlist-p (mv-nth 1 (vl-lex-token1 char1 echars st warnings))) t)))
Theorem:
(defthm append-of-vl-lex-token1 (implies (and (mv-nth 0 (vl-lex-token1 char1 echars st warnings)) (force (vl-echarlist-p echars)) (and (force (consp echars)) (force (equal char1 (vl-echar->char (car echars)))) (force (vl-lexstate-p st)))) (equal (append (vl-token->etext (mv-nth 0 (vl-lex-token1 char1 echars st warnings))) (mv-nth 1 (vl-lex-token1 char1 echars st warnings))) echars)))
Theorem:
(defthm no-change-loser-of-vl-lex-token1 (implies (not (mv-nth 0 (vl-lex-token1 char1 echars st warnings))) (equal (mv-nth 1 (vl-lex-token1 char1 echars st warnings)) echars)))
Theorem:
(defthm acl2-count-of-vl-lex-token1-weak (<= (acl2-count (mv-nth 1 (vl-lex-token1 char1 echars st warnings))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-lex-token1-strong (implies (and (mv-nth 0 (vl-lex-token1 char1 echars st warnings)) (force (equal char1 (vl-echar->char (car echars))))) (< (acl2-count (mv-nth 1 (vl-lex-token1 char1 echars st warnings))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))