		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Assigns->netassigns

Signature
(assigns->netassigns x) → netassigns
Arguments: x — Guard (assigns-p x).
Returns: netassigns — Type (netassigns-p netassigns).

Definitions and Theorems

Function: assigns->netassigns

(defun assigns->netassigns (x)
  (declare (xargs :guard (assigns-p x)))
  (let ((__function__ 'assigns->netassigns))
    (declare (ignorable __function__))
    (fast-alist-free
         (fast-alist-clean (assigns->netassigns-aux x nil)))))

Theorem: netassigns-p-of-assigns->netassigns

(defthm netassigns-p-of-assigns->netassigns
  (b* ((netassigns (assigns->netassigns x)))
    (netassigns-p netassigns))
  :rule-classes :rewrite)

Theorem: vars-of-assigns->netassigns

(defthm vars-of-assigns->netassigns
 (implies (not (member v (assigns-vars x)))
          (not (member v
                       (netassigns-vars (assigns->netassigns x))))))

Theorem: hons-assoc-equal-of-assigns->netassigns

(defthm hons-assoc-equal-of-assigns->netassigns
  (implies (not (member v (assigns-vars x)))
           (not (hons-assoc-equal v (assigns->netassigns x)))))

Theorem: assigns->netassigns-of-assigns-fix-x

(defthm assigns->netassigns-of-assigns-fix-x
  (equal (assigns->netassigns (assigns-fix x))
         (assigns->netassigns x)))

Theorem: assigns->netassigns-assigns-equiv-congruence-on-x

(defthm assigns->netassigns-assigns-equiv-congruence-on-x
  (implies (assigns-equiv x x-equiv)
           (equal (assigns->netassigns x)
                  (assigns->netassigns x-equiv)))
  :rule-classes :congruence)