Generate the name for a state bit, like
Function:
(defun stv-forge-state-bit (instnames st-name) (declare (xargs :guard (atom st-name))) (let ((__function__ 'stv-forge-state-bit)) (declare (ignorable __function__)) (if (atom instnames) st-name (prefix-atom (stringify (car instnames)) "!" (stv-forge-state-bit (cdr instnames) st-name)))))
Theorem:
(defthm atom-of-stv-forge-state-bit (implies (and (atom st-name)) (b* ((full-name (stv-forge-state-bit instnames st-name))) (atom full-name))) :rule-classes :rewrite)