		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Nonzero-uletters-after-p

Check if, in a list of Unicode characters, the character at position pos is followed by a non-zero number of `u' letters.

In this definition, we want n to be not merely a non-zero number of `u' letters at positions (+ pos 1) etc., but the maximum such number, i.e. such that (+ pos n 1) either is past the end of the list or is not a `u' letter; this is expressed by the last conjunct inside the quantification. The witness function returns this number, which is used in subsequent definitions.

Note that (take n (nthcdr (1+ pos) unicodes)) consists of the characters from position (+ pos 1) to (+ pos n), both extremes inclusive (positions in lists are zero-based).

Definitions and Theorems

Theorem: nonzero-uletters-after-p-suff

(defthm nonzero-uletters-after-p-suff
  (implies (and (posp n)
                (< (+ pos n) (len unicodes))
                (equal (take n (nthcdr (1+ pos) unicodes))
                       (repeat n (char-code #\u)))
                (or (equal (1+ (+ pos n)) (len unicodes))
                    (not (equal (nth (1+ (+ pos n)) unicodes)
                                (char-code #\u)))))
           (nonzero-uletters-after-p pos unicodes)))

Theorem: booleanp-of-nonzero-uletters-after-p

(defthm booleanp-of-nonzero-uletters-after-p
  (b* ((yes/no (nonzero-uletters-after-p pos unicodes)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: posp-of-nonzero-uletters-number

(defthm posp-of-nonzero-uletters-number
  (implies (nonzero-uletters-after-p pos unicodes)
           (posp (number-of-nonzero-uletters-after pos unicodes)))
  :rule-classes :type-prescription)