a theorem about env_rs holding for the really-empty initial states