Function:
(defun vl-gatetypenames-count-up (n idx basename) (declare (xargs :guard (and (natp n) (natp idx) (stringp basename)))) (let ((__function__ 'vl-gatetypenames-count-up)) (declare (ignorable __function__)) (if (zp n) nil (cons (cat basename (natstr idx)) (vl-gatetypenames-count-up (1- n) (1+ (lnfix idx)) basename)))))
Theorem:
(defthm return-type-of-vl-gatetypenames-count-up (b* ((names (vl-gatetypenames-count-up n idx basename))) (and (string-listp names) (eql (len names) (nfix n)))) :rule-classes :rewrite)
Theorem:
(defthm vl-gatetypenames-count-up-under-iff (b* nil (iff (vl-gatetypenames-count-up n idx basename) (posp n))))
Theorem:
(defthm vl-gatetypenames-count-up-of-nfix-n (equal (vl-gatetypenames-count-up (nfix n) idx basename) (vl-gatetypenames-count-up n idx basename)))
Theorem:
(defthm vl-gatetypenames-count-up-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-gatetypenames-count-up n idx basename) (vl-gatetypenames-count-up n-equiv idx basename))) :rule-classes :congruence)
Theorem:
(defthm vl-gatetypenames-count-up-of-nfix-idx (equal (vl-gatetypenames-count-up n (nfix idx) basename) (vl-gatetypenames-count-up n idx basename)))
Theorem:
(defthm vl-gatetypenames-count-up-nat-equiv-congruence-on-idx (implies (acl2::nat-equiv idx idx-equiv) (equal (vl-gatetypenames-count-up n idx basename) (vl-gatetypenames-count-up n idx-equiv basename))) :rule-classes :congruence)
Theorem:
(defthm vl-gatetypenames-count-up-of-str-fix-basename (equal (vl-gatetypenames-count-up n idx (str-fix basename)) (vl-gatetypenames-count-up n idx basename)))
Theorem:
(defthm vl-gatetypenames-count-up-streqv-congruence-on-basename (implies (streqv basename basename-equiv) (equal (vl-gatetypenames-count-up n idx basename) (vl-gatetypenames-count-up n idx basename-equiv))) :rule-classes :congruence)