		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Objdesign-of-var-and-read/write-var-theorems

Some theorems about objdesign-of-var and the functions to read and write variables.

Definitions and Theorems

Theorem: objdesign-of-var-aux-iff-read-auto-var-aux

(defthm objdesign-of-var-aux-iff-read-auto-var-aux
  (iff (objdesign-of-var-aux var frame scopes)
       (read-auto-var-aux var scopes)))

Theorem: objdesign-of-var-when-valuep-of-read-var

(defthm objdesign-of-var-when-valuep-of-read-var
  (implies (valuep (read-var id compst))
           (objdesign-of-var id compst)))

Theorem: write-auto-var-aux-iff-objdesign-of-var-aux

(defthm write-auto-var-aux-iff-objdesign-of-var-aux
  (iff (write-auto-var-aux var val scopes)
       (objdesign-of-var-aux var frame scopes)))

Theorem: objdesignp-of-objdesign-of-var-when-valuep-of-read-var

(defthm objdesignp-of-objdesign-of-var-when-valuep-of-read-var
  (implies (valuep (read-var id compst))
           (objdesignp (objdesign-of-var id compst))))