Rules about pop-frame.
The theorems about pop-frame remove all the add-var and enter-scope calls until they reach add-frame, with which pop-frame neutralizes. No rules are needed for computation states that start with update-var because these only occur when executing loops, which do not pop frames.
Theorem:
(defthm pop-frame-of-add-frame (implies (compustatep compst) (equal (pop-frame (add-frame fun compst)) compst)))
Theorem:
(defthm pop-frame-of-enter-scope (equal (pop-frame (enter-scope compst)) (pop-frame compst)))
Theorem:
(defthm pop-frame-of-add-var (equal (pop-frame (add-var var val compst)) (pop-frame compst)))
Theorem:
(defthm pop-frame-of-exit-scope (equal (pop-frame (exit-scope compst)) (pop-frame compst)))
Theorem:
(defthm pop-frame-of-if* (equal (pop-frame (if* a b c)) (if* a (pop-frame b) (pop-frame c))))