theory Detype_AI

lemma valid_mdb_detype[detype_invs_lemmas]: "valid_mdb (detype (untyped_range cap) s)" apply (insert invs, drule invs_mdb) apply (simp add: valid_mdb_def) apply (rule context_conjI) apply (safe intro!: mdb_cte_atI elim!: untyped_mdb untyped_inc reply_mdb) apply (drule(1) mdb_cte_atD) apply (clarsimp dest!: non_null_present) apply (drule(1) mdb_cte_atD) apply (clarsimp dest!: non_null_present) apply (erule descendants_inc_empty_slot) apply (clarsimp simp:cte_wp_at_caps_of_state swp_def) apply clarsimp apply (simp add: ut_revocable_def detype_def del: split_paired_All) apply (simp add: irq_revocable_def detype_def del: split_paired_All) apply (simp add: reply_master_revocable_def detype_def del: split_paired_All) apply (simp add: valid_arch_mdb_detype) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> valid_mdb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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) \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s) \<and> untyped_mdb (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> untyped_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> reply_mdb (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (2 subgoals):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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) \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s)\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> untyped_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> reply_mdb (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) \<and> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some (aa, ba); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (aa, ba)
 2. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some (aa, ba); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (a, b)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 6. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 7. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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); swp (cte_wp_at ((\<noteq>) NullCap)) s (aa, ba) \<and> swp (cte_wp_at ((\<noteq>) NullCap)) s (a, b)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (aa, ba)
 2. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some (aa, ba); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (a, b)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 6. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 7. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some (aa, ba); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (a, b)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 6. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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); swp (cte_wp_at ((\<noteq>) NullCap)) s (aa, ba) \<and> swp (cte_wp_at ((\<noteq>) NullCap)) s (a, b)\<rbrakk> \<Longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s) (a, b)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 6. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (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)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. (if fst p \<in> untyped_range cap then None else caps_of_state s p) = Some c \<and> NullCap \<noteq> c) (cdt s)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (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)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p). caps_of_state s x = (if fst x \<in> untyped_range cap then None else caps_of_state s x)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 6. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (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)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p). caps_of_state s x = (if fst x \<in> untyped_range cap then None else caps_of_state s x)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 5. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 4. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 3. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (detype (untyped_range cap) s)) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (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)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal:
No subgoals!