		Search-engine friendly clone of the ACL2 documentation.

Variable-resolution-preservation

Var-resolve-preservep-of-write-object

Preservation of variable resolution under write-object.

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

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

Definitions and Theorems

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

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