(rulenames-from-singular-conc-and-rep concs) → rulenames
Function:
(defun rulenames-from-singular-conc-and-rep (concs) (declare (xargs :guard (alternationp concs))) (let ((__function__ 'rulenames-from-singular-conc-and-rep)) (declare (ignorable __function__)) (b* (((when (endp concs)) nil) (first-conc (first concs)) ((unless (equal (len first-conc) 1)) (reserrf (cons :concatenation-is-not-singular first-conc))) (the-rep (car first-conc)) ((unless (and (repetitionp the-rep) (numrep-match-repeat-range-p 1 (repetition->range the-rep)))) (reserrf (cons :not-singular-repetition the-rep))) (the-el (repetition->element the-rep)) ((unless (and (elementp the-el) (element-case the-el :rulename))) (reserrf (cons :not-rulename-element the-el))) (rest-rulenames (rulenames-from-singular-conc-and-rep (rest concs))) ((when (reserrp rest-rulenames)) rest-rulenames) ((unless (string-listp rest-rulenames)) (reserrf (cons :impossible rest-rulenames)))) (cons (acl2::str-fix (rulename->get (element-rulename->get the-el))) rest-rulenames))))
Theorem:
(defthm string-list-resultp-of-rulenames-from-singular-conc-and-rep (b* ((rulenames (rulenames-from-singular-conc-and-rep concs))) (acl2::string-list-resultp rulenames)) :rule-classes :rewrite)