		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-init-states

Signature
(svtv-init-states x) → initst
Arguments: x — Guard (svarlist-p x).
Returns: initst — Type (svex-alist-p initst).

Definitions and Theorems

Function: svtv-init-states

(defun svtv-init-states (x)
 (declare (xargs :guard (svarlist-p x)))
 (let ((__function__ 'svtv-init-states))
  (declare (ignorable __function__))
  (if (atom x)
      nil
   (cons
    (let ((v (svar-fix (car x))))
     (cons
       v
       (svex-var
            (make-svar :name (list :svtv-init-st (svar->name v))))))
    (svtv-init-states (cdr x))))))

Theorem: svex-alist-p-of-svtv-init-states

(defthm svex-alist-p-of-svtv-init-states
  (b* ((initst (svtv-init-states x)))
    (svex-alist-p initst))
  :rule-classes :rewrite)

Theorem: svtv-init-states-of-svarlist-fix-x

(defthm svtv-init-states-of-svarlist-fix-x
  (equal (svtv-init-states (svarlist-fix x))
         (svtv-init-states x)))

Theorem: svtv-init-states-svarlist-equiv-congruence-on-x

(defthm svtv-init-states-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svtv-init-states x)
                  (svtv-init-states x-equiv)))
  :rule-classes :congruence)