(vl-replicate-orig-instnames1 low high instname) → names
Function:
(defun vl-replicate-orig-instnames1 (low high instname) (declare (xargs :guard (and (natp low) (natp high) (stringp instname)))) (declare (xargs :guard (<= low high))) (let ((__function__ 'vl-replicate-orig-instnames1)) (declare (ignorable __function__)) (b* ((low (lnfix low)) (high (lnfix high)) (name (cat instname "[" (natstr low) "]")) ((when (mbe :logic (zp (- high low)) :exec (eql low high))) (list name))) (cons name (vl-replicate-orig-instnames1 (+ 1 low) high instname)))))
Theorem:
(defthm string-listp-of-vl-replicate-orig-instnames1 (b* ((names (vl-replicate-orig-instnames1 low high instname))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-replicate-orig-instnames1 (equal (len (vl-replicate-orig-instnames1 low high instname)) (+ 1 (nfix (- (nfix high) (nfix low))))))
Theorem:
(defthm vl-replicate-orig-instnames1-of-nfix-low (equal (vl-replicate-orig-instnames1 (nfix low) high instname) (vl-replicate-orig-instnames1 low high instname)))
Theorem:
(defthm vl-replicate-orig-instnames1-nat-equiv-congruence-on-low (implies (acl2::nat-equiv low low-equiv) (equal (vl-replicate-orig-instnames1 low high instname) (vl-replicate-orig-instnames1 low-equiv high instname))) :rule-classes :congruence)
Theorem:
(defthm vl-replicate-orig-instnames1-of-nfix-high (equal (vl-replicate-orig-instnames1 low (nfix high) instname) (vl-replicate-orig-instnames1 low high instname)))
Theorem:
(defthm vl-replicate-orig-instnames1-nat-equiv-congruence-on-high (implies (acl2::nat-equiv high high-equiv) (equal (vl-replicate-orig-instnames1 low high instname) (vl-replicate-orig-instnames1 low high-equiv instname))) :rule-classes :congruence)
Theorem:
(defthm vl-replicate-orig-instnames1-of-str-fix-instname (equal (vl-replicate-orig-instnames1 low high (str-fix instname)) (vl-replicate-orig-instnames1 low high instname)))
Theorem:
(defthm vl-replicate-orig-instnames1-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-replicate-orig-instnames1 low high instname) (vl-replicate-orig-instnames1 low high instname-equiv))) :rule-classes :congruence)