A theorem about the length of the string of
a (proper) prefix of a list of
The string at the leaves of a
This inequality is used to verify some guards in subsequent functions.
The
Theorem:
(defthm nonempty-string-of-unicode-input-character-tree (implies (abnf-tree-with-root-p tree "unicode-input-character") (consp (abnf::tree->string tree))) :rule-classes :type-prescription)
Theorem:
(defthm nonempty-string-of-unicode-input-character-trees (implies (and (abnf-tree-list-with-root-p trees "unicode-input-character") (consp trees)) (consp (abnf::tree-list->string trees))) :rule-classes :type-prescription)
Theorem:
(defthm nonempty-string-of-unicode-input-character-tree-nonempty-suffix (implies (and (abnf-tree-list-with-root-p trees "unicode-input-character") (integer-range-p 0 (len trees) i)) (consp (abnf::tree-list->string (nthcdr i trees)))) :rule-classes :type-prescription)
Theorem:
(defthm len-of-abnf-tree-list-string-of-take-less-when-index-less (implies (and (integer-range-p 0 (len trees) i) (abnf-tree-list-with-root-p trees "unicode-input-character")) (< (len (abnf::tree-list->string (take i trees))) (len (abnf::tree-list->string trees)))) :rule-classes :linear)