Check if all the strings in a list have a length less than or equal to 8, which is the maximum length in the English wordlist.
The maximum length of the words in the English wordlist is 8. This function is used to prove upper bounds on the length of the menmonic, based on the lengths of the words in the English wordlist and on the maximum number of words in a mnemonic. See bip39-entropy-to-mnemonic.
(defun bip39-english-words-bound-p (strings) (declare (xargs :guard (string-listp strings))) (or (endp strings) (and (<= (length (car strings)) 8) (bip39-english-words-bound-p (cdr strings)))))
(defthm booleanp-of-bip39-english-words-bound-p (b* ((yes/no (bip39-english-words-bound-p strings))) (booleanp yes/no)) :rule-classes :rewrite)