		Search-engine friendly clone of the ACL2 documentation.

Stv-fully-general-in-alists

Stv-fully-general-in-alists-aux

Signature
(stv-fully-general-in-alists-aux n flat-ins acc) → in-alists
Arguments: n — Guard (natp n).; flat-ins — Guard (symbol-listp flat-ins).
Returns: in-alists — Type (cons-list-listp in-alists), given (cons-list-listp acc).

Definitions and Theorems

Function: stv-fully-general-in-alists-aux

(defun
    stv-fully-general-in-alists-aux
    (n flat-ins acc)
    (declare (xargs :guard (and (natp n) (symbol-listp flat-ins))))
    (let ((__function__ 'stv-fully-general-in-alists-aux))
         (declare (ignorable __function__))
         (let ((acc (cons (stv-fully-general-in-alist-n n flat-ins)
                          acc)))
              (if (zp n)
                  acc
                  (stv-fully-general-in-alists-aux (- n 1)
                                                   flat-ins acc)))))

Theorem: cons-list-listp-of-stv-fully-general-in-alists-aux

(defthm
 cons-list-listp-of-stv-fully-general-in-alists-aux
 (implies
  (cons-list-listp acc)
  (b* ((in-alists (stv-fully-general-in-alists-aux n flat-ins acc)))
      (cons-list-listp in-alists)))
 :rule-classes :rewrite)

Theorem: len-stv-fully-general-in-alists-aux

(defthm
     len-stv-fully-general-in-alists-aux
     (equal (len (stv-fully-general-in-alists-aux n flat-ins acc))
            (+ 1 (nfix n) (len acc))))