		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Objdesign-of-var-of-write-object

How objdesign-of-var changes under write-object.

Definitions and Theorems

Theorem: objdesign-of-var-aux-of-write-object

(defthm objdesign-of-var-aux-of-write-object
  (b*
    ((compst1 (write-object objdes val compst))
     (scopes (frame->scopes (nth i (compustate->frames compst))))
     (scopes1 (frame->scopes (nth i (compustate->frames compst1)))))
    (implies (not (errorp compst1))
             (equal (objdesign-of-var-aux var frame scopes1)
                    (objdesign-of-var-aux var frame scopes)))))

Theorem: objdesign-of-var-of-write-object

(defthm objdesign-of-var-of-write-object
  (b* ((compst1 (write-object objdes val compst)))
    (implies (not (errorp compst1))
             (equal (objdesign-of-var var compst1)
                    (objdesign-of-var var compst)))))