Create the name (keyword) of an applicability condition from its parts.
All the applicability condition names consist of
a prefix (
Function:
(defun casesplit-gen-appcond-name-from-parts (prefix k suffix) (declare (xargs :guard (and (stringp prefix) (natp k) (stringp suffix)))) (let ((__function__ 'casesplit-gen-appcond-name-from-parts)) (declare (ignorable __function__)) (intern (str::cat prefix (str::nat-to-dec-string k) suffix) "KEYWORD")))
Theorem:
(defthm symbolp-of-casesplit-gen-appcond-name-from-parts (b* ((name (casesplit-gen-appcond-name-from-parts prefix k suffix))) (symbolp name)) :rule-classes :rewrite)