Rules about exit-scope.
The theorems about exit-scope cancel it with enter-scope and move it past add-var. No rule for add-frame is needed because that case should never happen in the symbolic execution. No rule is needed for computation states that start with update-var because update-var is always pushed past enter-scope.
Theorem:
(defthm exit-scope-of-enter-scope (implies (and (compustatep compst) (> (compustate-frames-number compst) 0)) (equal (exit-scope (enter-scope compst)) compst)))
Theorem:
(defthm exit-scope-of-add-var (equal (exit-scope (add-var var val compst)) (exit-scope compst)))
Theorem:
(defthm exit-scope-of-if* (equal (exit-scope (if* a b c)) (if* a (exit-scope b) (exit-scope c))))