theory CSpace_AI

lemma cap_insert_simple_mdb:
  fixes dest src cap
  shows
  "\<lbrace>valid_mdb and valid_objs and
    cte_wp_at (\<lambda>c. c = cap.NullCap) dest and
    (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
    K (is_simple_cap cap)\<rbrace>
  cap_insert cap src dest \<lbrace>\<lambda>rv. valid_mdb :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: cap_insert_def valid_mdb_def2 update_cdt_def set_cdt_def set_untyped_cap_as_full_def) apply (wp set_cap_caps_of_state2 get_cap_wp|simp del: fun_upd_apply split del: if_split)+ apply (clarsimp simp: cte_wp_at_caps_of_state safe_parent_is_parent valid_mdb_def2
                  simp del: fun_upd_apply
                  split del: if_split) apply (rule conjI) apply (cases src, cases dest) apply (clarsimp simp: mdb_cte_at_def is_simple_cap_def split del: if_split) apply (subgoal_tac "mdb_insert_abs (cdt s) src dest") prefer 2 apply (rule mdb_insert_abs.intro) apply clarsimp apply (erule (1) mdb_cte_at_Null_None) apply (erule (1) mdb_cte_at_Null_descendants) apply (intro conjI impI) apply (clarsimp simp:mdb_cte_at_def is_simple_cap_def split del:if_split) apply (fastforce split:if_split_asm) apply (erule (4) mdb_insert_abs.untyped_mdb_simple) apply (simp add: is_simple_cap_def) apply (erule safe_parent_refs_or_descendants) apply (erule(1) mdb_insert_abs.descendants_inc) apply simp apply (simp add:safe_parent_cap_range) apply (clarsimp simp:safe_parent_for_def same_region_as_cap_class) apply (frule mdb_insert_abs.neq) apply (simp add: no_mloop_def mdb_insert_abs.parency) apply (intro allI impI) apply (rule notI) apply (simp add: mdb_insert_abs.dest_no_parent_trancl) apply (erule(2)  mdb_insert_abs.untyped_inc_simple) apply (drule(1) caps_of_state_valid)+ apply (simp add:valid_cap_aligned) apply (simp add:is_simple_cap_def)+ apply (clarsimp simp: ut_revocable_def is_simple_cap_def) apply (clarsimp simp: irq_revocable_def is_simple_cap_def) apply (clarsimp simp: reply_master_revocable_def is_simple_cap_def) apply (erule(2)  mdb_insert_abs.reply_mdb_simple) apply (fastforce simp: is_simple_cap_def safe_parent_for_def is_cap_simps) apply (clarsimp simp: is_simple_cap_def) apply (erule (2) valid_arch_mdb_simple) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb and valid_objs and cte_wp_at (\<lambda>c. c = NullCap) dest and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and K (is_simple_cap cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) and valid_objs and cte_wp_at (\<lambda>c. c = NullCap) dest and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and (\<lambda>y. is_simple_cap cap)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src)\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s) \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. c = NullCap) dest s \<and> cte_wp_at (safe_parent_for (cdt s) src cap) src s \<and> is_simple_cap cap \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) \<and> untyped_mdb ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) \<and> untyped_inc ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap))) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) \<and> untyped_mdb ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) \<and> untyped_inc ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest := if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap))) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b aa ba. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; src = (a, b); dest = (aa, ba)\<rbrakk> \<Longrightarrow> is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(src \<mapsto> max_free_index_update capa, dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> mdb_insert_abs (cdt s) src dest proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> mdb_insert_abs (cdt s) src dest
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (4 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> src \<noteq> dest
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> cdt s dest = None
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> descendants_of dest (cdt s) = {}
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> cdt s dest = None
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> descendants_of dest (cdt s) = {}
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> descendants_of dest (cdt s) = {}
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> (obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src)) \<and> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> no_mloop ((cdt s)(dest \<mapsto> src)) \<and> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap)) \<and> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (10 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. ((caps_of_state s)(dest \<mapsto> cap)) p = Some c \<and> NullCap \<noteq> c) ((cdt s)(dest \<mapsto> src))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (10 subgoals):
 1. \<And>s capa a b aa ba. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> NullCap \<noteq> c); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; cap \<noteq> NullCap; cap \<noteq> IRQControlCap; \<not> is_untyped_cap cap; \<not> is_master_reply_cap cap; \<not> is_reply_cap cap; \<not> is_ep_cap cap; \<not> is_ntfn_cap cap; \<not> is_thread_cap cap; \<not> is_cnode_cap cap; \<not> is_zombie cap; is_simple_cap_arch cap; (if (aa, ba) = dest then Some src else cdt s (aa, ba)) = Some (a, b)\<rbrakk> \<Longrightarrow> (\<exists>c. (if (a, b) = dest then Some cap else caps_of_state s (a, b)) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. (if (aa, ba) = dest then Some cap else caps_of_state s (aa, ba)) = Some c \<and> NullCap \<noteq> c)
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (9 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (10 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap cap
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs capa \<or> descendants_of src (cdt s) = {} \<and> obj_refs cap \<subseteq> untyped_range capa \<or> safe_parent_for_arch cap capa
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (9 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs capa \<or> descendants_of src (cdt s) = {} \<and> obj_refs cap \<subseteq> untyped_range capa \<or> safe_parent_for_arch cap capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (8 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> descendants_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (9 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> caps_of_state s src = Some (?c288 s capa)
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (?c288 s capa) \<and> cap_range cap \<subseteq> cap_range (?c288 s capa)
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (8 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (8 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (7 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (7 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap; src \<noteq> dest\<rbrakk> \<Longrightarrow> no_mloop ((cdt s)(dest \<mapsto> src))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (7 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap; src \<noteq> dest\<rbrakk> \<Longrightarrow> \<forall>a b. cdt s \<Turnstile> (a, b) \<rightarrow> src \<longrightarrow> (a, b) \<noteq> dest
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (7 subgoals):
 1. \<And>s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap; src \<noteq> dest; cdt s \<Turnstile> (a, b) \<rightarrow> src\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (7 subgoals):
 1. \<And>s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap; src \<noteq> dest; cdt s \<Turnstile> (a, b) \<rightarrow> src; (a, b) = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (6 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_inc ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (11 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> cap_aligned capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> caps_of_state s dest = Some NullCap
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_range cap = untyped_range capa \<or> \<not> is_untyped_cap cap
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> descendants_of src (cdt s) = {}
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap; s \<turnstile> NullCap; s \<turnstile> capa\<rbrakk> \<Longrightarrow> cap_aligned capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> caps_of_state s dest = Some NullCap
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_range cap = untyped_range capa \<or> \<not> is_untyped_cap cap
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> descendants_of src (cdt s) = {}
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> caps_of_state s dest = Some NullCap
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> untyped_range cap = untyped_range capa \<or> \<not> is_untyped_cap cap
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> descendants_of src (cdt s) = {}
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> usable_untyped_range capa = {}
 6. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 7. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 8. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 9. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 10. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (5 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; cap \<noteq> NullCap \<and> cap \<noteq> IRQControlCap \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> \<not> is_ep_cap cap \<and> \<not> is_ntfn_cap cap \<and> \<not> is_thread_cap cap \<and> \<not> is_cnode_cap cap \<and> \<not> is_zombie cap \<and> is_simple_cap_arch cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest\<rbrakk> \<Longrightarrow> ut_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 5. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (4 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> irq_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 4. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_master_revocable ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> reply_mdb ((cdt s)(dest \<mapsto> src)) ((caps_of_state s)(dest \<mapsto> cap))
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<not> is_reply_cap capa \<and> \<not> is_master_reply_cap capa
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap
 3. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap
 2. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_objs s; caps_of_state s dest = Some NullCap; is_simple_cap cap; safe_parent_for (cdt s) src cap capa; caps_of_state s src = Some capa; mdb_insert_abs (cdt s) src dest; obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap)) proof (prove)
goal:
No subgoals!