		Search-engine friendly clone of the ACL2 documentation.

Expand.lisp

Svtv-expand-lines

Signature
(svtv-expand-lines x len) → xx
Arguments: x — Guard (svtv-lines-p x).; len — Guard (natp len).
Returns: xx — Type (svtv-lines-p xx).

Definitions and Theorems

Function: svtv-expand-lines

(defun svtv-expand-lines (x len)
 (declare (xargs :guard (and (svtv-lines-p x) (natp len))))
 (let ((__function__ 'svtv-expand-lines))
  (declare (ignorable __function__))
  (if (atom x)
      nil
   (cons
    (change-svtv-line
       (car x)
       :entries
       (svtv-extend-entrylist (svtv-line->entries (car x))
                              len '_
                              '_
                              (lhs-width (svtv-line->lhs (car x)))))
    (svtv-expand-lines (cdr x) len)))))

Theorem: svtv-lines-p-of-svtv-expand-lines

(defthm svtv-lines-p-of-svtv-expand-lines
  (b* ((xx (svtv-expand-lines x len)))
    (svtv-lines-p xx))
  :rule-classes :rewrite)

Theorem: svtv-expand-lines-of-svtv-lines-fix-x

(defthm svtv-expand-lines-of-svtv-lines-fix-x
  (equal (svtv-expand-lines (svtv-lines-fix x)
                            len)
         (svtv-expand-lines x len)))

Theorem: svtv-expand-lines-svtv-lines-equiv-congruence-on-x

(defthm svtv-expand-lines-svtv-lines-equiv-congruence-on-x
  (implies (svtv-lines-equiv x x-equiv)
           (equal (svtv-expand-lines x len)
                  (svtv-expand-lines x-equiv len)))
  :rule-classes :congruence)

Theorem: svtv-expand-lines-of-nfix-len

(defthm svtv-expand-lines-of-nfix-len
  (equal (svtv-expand-lines x (nfix len))
         (svtv-expand-lines x len)))

Theorem: svtv-expand-lines-nat-equiv-congruence-on-len

(defthm svtv-expand-lines-nat-equiv-congruence-on-len
  (implies (nat-equiv len len-equiv)
           (equal (svtv-expand-lines x len)
                  (svtv-expand-lines x len-equiv)))
  :rule-classes :congruence)