		Search-engine friendly clone of the ACL2 documentation.

Stobj-updater-independence

Def-updater-independence-thm

Prove an updater independence theorem, as discussed in stobj-updater-independence.

This just adds the appropriate bind-free form to your theorem, which should use the variables new and old (from the ACL2 package). For example:

(def-updater-independence-thm access-3rd-updater-independence
  (implies (equal (nth 3 new) (nth 3 old))
           (equal (access-3rd new) (access-3rd old)))
  :hints(("Goal" :in-theory (enable access-3rd))))

Note new should appear in the LHS and old should not.