		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Names-indexed-below

Create a list of indexed names, with the same base and indices from 0 to n-1 (i.e. below n).

Signature
(names-indexed-below base n) → names
Arguments: base — Guard (stringp base).; n — Guard (natp n).
Returns: names — Type (name-listp names).

Definitions and Theorems

Function: names-indexed-below-rev

(defun names-indexed-below-rev (base n)
  (declare (xargs :guard (and (stringp base) (natp n))))
  (let ((__function__ 'names-indexed-below-rev))
    (declare (ignorable __function__))
    (b* (((when (zp n)) nil)
         (n-1 (1- n))
         (name (name-indexed base n-1))
         (names (names-indexed-below-rev base n-1)))
      (cons name names))))

Theorem: name-listp-of-names-indexed-below-rev

(defthm name-listp-of-names-indexed-below-rev
  (b* ((names-rev (names-indexed-below-rev base n)))
    (name-listp names-rev))
  :rule-classes :rewrite)

Theorem: len-of-names-indexed-below-rev

(defthm len-of-names-indexed-below-rev
  (b* ((?names-rev (names-indexed-below-rev base n)))
    (equal (len names-rev) (nfix n))))

Theorem: consp-of-names-indexed-below-rev

(defthm consp-of-names-indexed-below-rev
  (b* ((?names-rev (names-indexed-below-rev base n)))
    (equal (consp names-rev)
           (> (nfix n) 0))))

Theorem: base-not-member-of-names-indexed-below-rev

(defthm base-not-member-of-names-indexed-below-rev
  (implies (stringp base)
           (not (member-equal (name-simple base)
                              (names-indexed-below-rev base n)))))

Theorem: member-equal-of-names-indexed-below-rev

(defthm member-equal-of-names-indexed-below-rev
  (iff (member-equal (name-indexed base i)
                     (names-indexed-below-rev base1 n))
       (and (equal (str-fix base) (str-fix base1))
            (< (nfix i) (nfix n)))))

Theorem: no-duplicatesp-equal-of-names-indexed-below-rev

(defthm no-duplicatesp-equal-of-names-indexed-below-rev
  (no-duplicatesp-equal (names-indexed-below-rev base n)))

Function: names-indexed-below

(defun names-indexed-below (base n)
  (declare (xargs :guard (and (stringp base) (natp n))))
  (let ((__function__ 'names-indexed-below))
    (declare (ignorable __function__))
    (rev (names-indexed-below-rev base n))))

Theorem: name-listp-of-names-indexed-below

(defthm name-listp-of-names-indexed-below
  (b* ((names (names-indexed-below base n)))
    (name-listp names))
  :rule-classes :rewrite)

Theorem: len-of-names-indexed-below

(defthm len-of-names-indexed-below
  (b* ((?names (names-indexed-below base n)))
    (equal (len names) (nfix n))))

Theorem: consp-of-names-indexed-below

(defthm consp-of-names-indexed-below
  (b* ((?names (names-indexed-below base n)))
    (equal (consp names) (> (nfix n) 0))))

Theorem: base-not-member-of-names-indexed-below

(defthm base-not-member-of-names-indexed-below
  (implies (stringp base)
           (not (member-equal (name-simple base)
                              (names-indexed-below base n)))))

Theorem: member-equal-of-names-indexed-below

(defthm member-equal-of-names-indexed-below
  (iff (member-equal (name-indexed base i)
                     (names-indexed-below base1 n))
       (and (equal (str-fix base) (str-fix base1))
            (< (nfix i) (nfix n)))))

Theorem: no-duplicatesp-equal-of-names-indexed-below

(defthm no-duplicatesp-equal-of-names-indexed-below
  (no-duplicatesp-equal (names-indexed-below base n)))