Theorems about the variables in a computation state after execution of certain kinds of constructs.
Theorem:
(defthm keys-of-cstate->local-of-exec-statement-list (b* ((outcome (exec-statement-list stmts cstate funenv limit))) (implies (not (reserrp outcome)) (subset (omap::keys (cstate->local cstate)) (omap::keys (cstate->local (soutcome->cstate outcome)))))))
Theorem:
(defthm keys-of-cstate->local-of-exec-for-iterations (b* ((outcome (exec-for-iterations test update body cstate funenv limit))) (implies (not (reserrp outcome)) (equal (omap::keys (cstate->local cstate)) (omap::keys (cstate->local (soutcome->cstate outcome)))))))