		Search-engine friendly clone of the ACL2 documentation.

Variable-visibility-preservation

Var-visible-preservep-of-write-object

Preservation of variable visbility under write-object.

The predicate var-visible-preservep holds between a computation state and the one obtained from it via write-object.

This theorem is used, in var-visible-preservep-of-exec, to handle the execution of assignments.

Definitions and Theorems

Theorem: var-visible-preservep-of-write-object

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