		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Read-object-of-objdesign-of-var-to-read-var

Equivalence of read-object and read-var for object designators of variables.

Definitions and Theorems

Theorem: read-object-of-objdesign-of-var-to-read-var

(defthm read-object-of-objdesign-of-var-to-read-var
  (b* ((objdes (objdesign-of-var var compst)))
    (implies objdes
             (equal (read-object objdes compst)
                    (read-var var compst)))))

Subtopics

Read-var-to-read-object-of-objdesign-of-var: Converse of read-object-of-objdesign-of-var-to-read-var.