(iname-list-rev base n) → names-rev
Function:
(defun iname-list-rev (base n) (declare (xargs :guard (and (stringp base) (natp n)))) (let ((__function__ 'iname-list-rev)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (n-1 (1- n)) (name (iname base n-1)) (names (iname-list-rev base n-1))) (cons name names))))
Theorem:
(defthm string-listp-of-iname-list-rev (b* ((names-rev (iname-list-rev base n))) (string-listp names-rev)) :rule-classes :rewrite)
Theorem:
(defthm len-of-iname-list-rev (b* ((?names-rev (iname-list-rev base n))) (equal (len names-rev) (nfix n))))
Theorem:
(defthm consp-of-iname-list-rev (b* ((?names-rev (iname-list-rev base n))) (equal (consp names-rev) (> (nfix n) 0))))
Theorem:
(defthm base-not-member-of-iname-list-rev (implies (stringp base) (not (member-equal base (iname-list-rev base n)))))