theory CSpace_R

lemma updateCapFreeIndex_valid_mdb_ctes:
  assumes preserve:"\<And>m m'. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (Q m) (Q m')"
  and     coin  :"\<And>m cte. \<lbrakk>m src = Some cte\<rbrakk> \<Longrightarrow> (\<exists>cte'. (Q m) src = Some cte' \<and> cteCap cte = cteCap cte')"
  and     assoc :"\<And>m f. Q (modify_map m src (cteCap_update f)) = modify_map (Q m) src (cteCap_update f)"
  shows
 "\<lbrace>\<lambda>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap
       \<and>  valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace>
  updateCap src (capFreeIndex_update (\<lambda>_. index) cap)
 \<lbrace>\<lambda>r s. (valid_mdb_ctes (Q (ctes_of s)))\<rbrace>" apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src
              (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))") apply (clarsimp simp:valid_mdb_ctes_def) apply (intro conjI) apply ((simp add:mdb_inv_preserve.preserve_stuff mdb_inv_preserve.by_products)+)[7] apply (rule mdb_inv_preserve.untyped_inc') apply assumption apply (clarsimp simp:assoc cte_wp_at_ctes_of) apply (clarsimp simp:modify_map_def split:if_splits) apply (drule coin) apply clarsimp apply (erule(1) subsetD) apply simp apply (simp_all add:mdb_inv_preserve.preserve_stuff  mdb_inv_preserve.by_products) apply (rule preserve) apply (clarsimp simp:cte_wp_at_ctes_of) apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. valid_mdb_ctes (Q (ctes_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> valid_mdb_ctes (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s; mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))\<rbrakk> \<Longrightarrow> valid_mdb_ctes (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> no_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> mdb_chain_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> valid_badges (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> caps_contained' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> mdb_chunked (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> untyped_mdb' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> untyped_inc' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) \<and> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (15 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_dlist (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> no_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> mdb_chain_0 (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_badges (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> caps_contained' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> mdb_chunked (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_mdb' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 10. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
A total of 15 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> mdb_inv_preserve (?m37 s) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s x cte cte'. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s; ?m37 s x = Some cte; Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) x = Some cte'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (?m37 s)
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 10. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (9 subgoals):
 1. \<And>s x cte cte'. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s; Q (ctes_of s) x = Some cte; Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) x = Some cte'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte') \<subseteq> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (9 subgoals):
 1. \<And>s x cte cte' xa ctea. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (modify_map (Q (ctes_of s)) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<subseteq> usableUntypedRange (cteCap ctea); isUntypedCap (cteCap ctea); valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); Q (ctes_of s) x = Some cte; modify_map (Q (ctes_of s)) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea))) x = Some cte'; isUntypedCap (cteCap cte); xa \<in> usableUntypedRange (cteCap cte'); ctes_of s src = Some ctea; cap = cteCap ctea\<rbrakk> \<Longrightarrow> xa \<in> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (9 subgoals):
 1. \<And>s cte xa ctea. \<lbrakk>isUntypedCap (cteCap cte); xa \<in> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)); ctes_of s src = Some ctea; cap = cteCap ctea; mdb_inv_preserve (Q (ctes_of s)) ((Q (ctes_of s))(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) cte)); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<subseteq> usableUntypedRange (cteCap ctea); isUntypedCap (cteCap ctea); valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); Q (ctes_of s) src = Some cte\<rbrakk> \<Longrightarrow> xa \<in> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (9 subgoals):
 1. \<And>s cte xa ctea. \<lbrakk>isUntypedCap (cteCap cte); xa \<in> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)); cap = cteCap ctea; mdb_inv_preserve (Q (ctes_of s)) ((Q (ctes_of s))(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) cte)); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<subseteq> usableUntypedRange (cteCap ctea); isUntypedCap (cteCap ctea); valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); Q (ctes_of s) src = Some cte; \<exists>cte'. Q (ctes_of s) src = Some cte' \<and> cteCap ctea = cteCap cte'\<rbrakk> \<Longrightarrow> xa \<in> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (9 subgoals):
 1. \<And>s cte xa ctea. \<lbrakk>isUntypedCap (cteCap cte); xa \<in> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)); cap = cteCap cte; mdb_inv_preserve (Q (ctes_of s)) ((Q (ctes_of s))(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap cte)) cte)); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte); valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); Q (ctes_of s) src = Some cte; cteCap ctea = cteCap cte\<rbrakk> \<Longrightarrow> xa \<in> usableUntypedRange (cteCap cte)
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 9. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> untyped_inc' (Q (ctes_of s))
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 8. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> valid_nullcaps (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 2. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> ut_revocable' (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 3. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> class_links (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 4. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> distinct_zombies (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 5. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> irq_control (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 6. \<And>s. \<lbrakk>mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap; isUntypedCap cap; valid_dlist (Q (ctes_of s)); no_0 (Q (ctes_of s)); mdb_chain_0 (Q (ctes_of s)); valid_badges (Q (ctes_of s)); caps_contained' (Q (ctes_of s)); mdb_chunked (Q (ctes_of s)); untyped_mdb' (Q (ctes_of s)); untyped_inc' (Q (ctes_of s)); valid_nullcaps (Q (ctes_of s)); ut_revocable' (Q (ctes_of s)); class_links (Q (ctes_of s)); distinct_zombies (Q (ctes_of s)); irq_control (Q (ctes_of s)); reply_masters_rvk_fb (Q (ctes_of s)); cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))))
 7. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<subseteq> usableUntypedRange cap \<and> isUntypedCap cap \<and> valid_mdb_ctes (Q (ctes_of s)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte); isUntypedCap (cteCap cte); valid_mdb_ctes (Q (ctes_of s)); ctes_of s src = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap cte)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte); isUntypedCap (cteCap cte); valid_mdb_ctes (Q (ctes_of s)); ctes_of s src = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> ctes_of s src = Some cte
 2. \<And>s cte. \<lbrakk>usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte); isUntypedCap (cteCap cte); valid_mdb_ctes (Q (ctes_of s)); ctes_of s src = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) proof (prove)
goal:
No subgoals!