		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-expand-hids-in-lines

(stv-expand-hids-in-lines lines mod) expands all of the HIDs in a list of STV internal lines into lists of esim paths.

Signature
(stv-expand-hids-in-lines lines mod) → new-lines
Arguments: lines — Guard (true-list-listp lines).
Returns: new-lines — Copy of lines except with expanded names.

Definitions and Theorems

Function: stv-expand-hids-in-lines

(defun stv-expand-hids-in-lines (lines mod)
  (declare (xargs :guard (true-list-listp lines)))
  (let ((__function__ 'stv-expand-hids-in-lines))
    (declare (ignorable __function__))
    (b* (((when (atom lines)) nil)
         (line1 (car lines))
         ((cons name phases) line1)
         (lsb-paths (stv-expand-hid name mod)))
      (cons (cons lsb-paths phases)
            (stv-expand-hids-in-lines (cdr lines)
                                      mod)))))

Theorem: alistp-of-stv-expand-hids-in-lines

(defthm alistp-of-stv-expand-hids-in-lines
  (alistp (stv-expand-hids-in-lines lines mod)))

Theorem: true-list-listp-of-stv-expand-hids-in-lines

(defthm true-list-listp-of-stv-expand-hids-in-lines
  (implies (true-list-listp lines)
           (true-list-listp (stv-expand-hids-in-lines lines mod))))