		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-inalist-resolve-unassigned

Signature
(svtv-inalist-resolve-unassigned inalist masks phase) → inalist1
Arguments: inalist — Guard (svex-alist-p inalist).; masks — Guard (4vmask-alist-p masks).; phase — Guard (natp phase).
Returns: inalist1 — Type (svex-alist-p inalist1).

Definitions and Theorems

Function: svtv-inalist-resolve-unassigned

(defun svtv-inalist-resolve-unassigned (inalist masks phase)
 (declare (xargs :guard (and (svex-alist-p inalist)
                             (4vmask-alist-p masks)
                             (natp phase))))
 (let ((__function__ 'svtv-inalist-resolve-unassigned))
   (declare (ignorable __function__))
   (b*
    ((inalist (svex-alist-fix inalist))
     (masks (4vmask-alist-fix masks))
     ((when (atom inalist)) nil)
     ((cons var expr) (car inalist))
     (mask (or (cdr (hons-get var masks)) 0))
     (exp (svex-call 'bit?
                     (list (svex-quote (2vec (sparseint-val mask)))
                           expr
                           (svex-var (svex-phase-var var phase))))))
    (cons (cons var exp)
          (svtv-inalist-resolve-unassigned (cdr inalist)
                                           masks phase)))))

Theorem: svex-alist-p-of-svtv-inalist-resolve-unassigned

(defthm svex-alist-p-of-svtv-inalist-resolve-unassigned
 (b*
  ((inalist1 (svtv-inalist-resolve-unassigned inalist masks phase)))
  (svex-alist-p inalist1))
 :rule-classes :rewrite)

Theorem: svtv-inalist-resolve-unassigned-of-svex-alist-fix-inalist

(defthm svtv-inalist-resolve-unassigned-of-svex-alist-fix-inalist
  (equal (svtv-inalist-resolve-unassigned (svex-alist-fix inalist)
                                          masks phase)
         (svtv-inalist-resolve-unassigned inalist masks phase)))

Theorem: svtv-inalist-resolve-unassigned-svex-alist-equiv-congruence-on-inalist

(defthm
 svtv-inalist-resolve-unassigned-svex-alist-equiv-congruence-on-inalist
 (implies
  (svex-alist-equiv inalist inalist-equiv)
  (equal
       (svtv-inalist-resolve-unassigned inalist masks phase)
       (svtv-inalist-resolve-unassigned inalist-equiv masks phase)))
 :rule-classes :congruence)

Theorem: svtv-inalist-resolve-unassigned-of-4vmask-alist-fix-masks

(defthm svtv-inalist-resolve-unassigned-of-4vmask-alist-fix-masks
 (equal
   (svtv-inalist-resolve-unassigned inalist (4vmask-alist-fix masks)
                                    phase)
   (svtv-inalist-resolve-unassigned inalist masks phase)))

Theorem: svtv-inalist-resolve-unassigned-4vmask-alist-equiv-congruence-on-masks

(defthm
 svtv-inalist-resolve-unassigned-4vmask-alist-equiv-congruence-on-masks
 (implies
  (4vmask-alist-equiv masks masks-equiv)
  (equal
       (svtv-inalist-resolve-unassigned inalist masks phase)
       (svtv-inalist-resolve-unassigned inalist masks-equiv phase)))
 :rule-classes :congruence)

Theorem: svtv-inalist-resolve-unassigned-of-nfix-phase

(defthm svtv-inalist-resolve-unassigned-of-nfix-phase
 (equal (svtv-inalist-resolve-unassigned inalist masks (nfix phase))
        (svtv-inalist-resolve-unassigned inalist masks phase)))

Theorem: svtv-inalist-resolve-unassigned-nat-equiv-congruence-on-phase

(defthm
      svtv-inalist-resolve-unassigned-nat-equiv-congruence-on-phase
 (implies
  (nat-equiv phase phase-equiv)
  (equal
       (svtv-inalist-resolve-unassigned inalist masks phase)
       (svtv-inalist-resolve-unassigned inalist masks phase-equiv)))
 :rule-classes :congruence)