Function:
(defun looks-like-hex-string-fringe (fringe) (declare (xargs :guard (nat-listp fringe))) (let ((__function__ 'looks-like-hex-string-fringe)) (declare (ignorable __function__)) (and (true-listp fringe) (>= (len fringe) 5) (equal (subseq fringe 0 3) (list (char-code #\h) (char-code #\e) (char-code #\x))) (equal (nth 3 fringe) (nth (- (len fringe) 1) fringe)) (member (nth 3 fringe) (list (char-code #\") (char-code #\'))) t)))
Theorem:
(defthm booleanp-of-looks-like-hex-string-fringe (b* ((yes/no (looks-like-hex-string-fringe fringe))) (booleanp yes/no)) :rule-classes :rewrite)