		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-phase-var-assigns

Signature
(svtv-phase-var-assigns x phase) → assigns
Arguments: x — Guard (svarlist-p x).; phase — Guard (natp phase).
Returns: assigns — Type (svex-alist-p assigns).

Definitions and Theorems

Function: svtv-phase-var-assigns

(defun svtv-phase-var-assigns (x phase)
  (declare (xargs :guard (and (svarlist-p x) (natp phase))))
  (let ((__function__ 'svtv-phase-var-assigns))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (let ((v (svar-fix (car x))))
              (cons v (svex-var (svex-phase-var v phase))))
            (svtv-phase-var-assigns (cdr x)
                                    phase)))))

Theorem: svex-alist-p-of-svtv-phase-var-assigns

(defthm svex-alist-p-of-svtv-phase-var-assigns
  (b* ((assigns (svtv-phase-var-assigns x phase)))
    (svex-alist-p assigns))
  :rule-classes :rewrite)

Theorem: svtv-phase-var-assigns-of-svarlist-fix-x

(defthm svtv-phase-var-assigns-of-svarlist-fix-x
  (equal (svtv-phase-var-assigns (svarlist-fix x)
                                 phase)
         (svtv-phase-var-assigns x phase)))

Theorem: svtv-phase-var-assigns-svarlist-equiv-congruence-on-x

(defthm svtv-phase-var-assigns-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svtv-phase-var-assigns x phase)
                  (svtv-phase-var-assigns x-equiv phase)))
  :rule-classes :congruence)

Theorem: svtv-phase-var-assigns-of-nfix-phase

(defthm svtv-phase-var-assigns-of-nfix-phase
  (equal (svtv-phase-var-assigns x (nfix phase))
         (svtv-phase-var-assigns x phase)))

Theorem: svtv-phase-var-assigns-nat-equiv-congruence-on-phase

(defthm svtv-phase-var-assigns-nat-equiv-congruence-on-phase
  (implies (nat-equiv phase phase-equiv)
           (equal (svtv-phase-var-assigns x phase)
                  (svtv-phase-var-assigns x phase-equiv)))
  :rule-classes :congruence)