		Search-engine friendly clone of the ACL2 documentation.

Vl-lex-plain-token/remainder-thms

Token and remainder theorems for vl-lex-plain, automatically generated by def-token/remainder-thms.

Definitions and Theorems

Theorem: vl-token-p-of-vl-lex-plain

(defthm vl-token-p-of-vl-lex-plain
 (implies
  (and (force (vl-echarlist-p echars))
       (force (vl-plaintokentype-p type)))
  (equal
    (vl-token-p (mv-nth 0
                        (vl-lex-plain echars string type warnings)))
    (if (mv-nth 0
                (vl-lex-plain echars string type warnings))
        t
      nil))))

Theorem: true-listp-of-vl-lex-plain

(defthm true-listp-of-vl-lex-plain
 (equal
    (true-listp (mv-nth 1
                        (vl-lex-plain echars string type warnings)))
    (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
       (true-listp echars)
       (true-listp
            (mv-nth 1
                    (vl-lex-plain echars string type warnings)))))))

Theorem: vl-echarlist-p-of-vl-lex-plain

(defthm vl-echarlist-p-of-vl-lex-plain
 (implies
    (force (vl-echarlist-p echars))
    (equal (vl-echarlist-p
                (mv-nth 1
                        (vl-lex-plain echars string type warnings)))
           t)))

Theorem: append-of-vl-lex-plain

(defthm append-of-vl-lex-plain
 (implies
  (and (mv-nth 0
               (vl-lex-plain echars string type warnings))
       (force (vl-echarlist-p echars))
       (force (vl-plaintokentype-p type)))
  (equal
   (append (vl-token->etext
                (mv-nth 0
                        (vl-lex-plain echars string type warnings)))
           (mv-nth 1
                   (vl-lex-plain echars string type warnings)))
   echars)))

Theorem: no-change-loser-of-vl-lex-plain

(defthm no-change-loser-of-vl-lex-plain
 (implies (not (mv-nth 0
                       (vl-lex-plain echars string type warnings)))
          (equal (mv-nth 1
                         (vl-lex-plain echars string type warnings))
                 echars)))

Theorem: acl2-count-of-vl-lex-plain-weak

(defthm acl2-count-of-vl-lex-plain-weak
 (<=
    (acl2-count (mv-nth 1
                        (vl-lex-plain echars string type warnings)))
    (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-plain-strong

(defthm acl2-count-of-vl-lex-plain-strong
 (implies
  (and (mv-nth 0
               (vl-lex-plain echars string type warnings))
       t)
  (<
    (acl2-count (mv-nth 1
                        (vl-lex-plain echars string type warnings)))
    (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))