Rules for executing identifiers.
We use a binding hypothesis to read the variable's value, and we rewrite exec-ident differently based on whether the value is an array or not.
We also introduce a rule that is used in the modular proofs, and that follows the definition of exec-ident more closely. This will eventually replace the other rule below.
Theorem:
(defthm exec-ident-open (implies (and (equal val (read-var id compst)) (valuep val)) (equal (exec-ident id compst) (make-expr-value :value val :object (objdesign-of-var id compst)))))
Theorem:
(defthm exec-ident-open-via-object (implies (and (equal objdes (objdesign-of-var id compst)) objdes) (equal (exec-ident id compst) (make-expr-value :value (read-object objdes compst) :object objdes))))