theory KHeap_AI

lemma valid_mdb_lift:
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
  assumes m: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>"
  assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>"
  shows "\<lbrace>valid_mdb\<rbrace> f \<lbrace>\<lambda>r. valid_mdb\<rbrace>" apply (clarsimp simp add: valid_def valid_mdb_def mdb_cte_at_def) apply (frule_tac P1="(=) (cdt s)" in use_valid [OF _  m], rule refl) apply (rule conjI) apply clarsimp apply (erule allE)+ apply (erule (1) impE) apply clarsimp apply (rule conjI) apply (erule use_valid [OF _ c [THEN hoare_cte_wp_caps_of_state_lift]]) apply simp apply (erule use_valid [OF _ c [THEN hoare_cte_wp_caps_of_state_lift]]) apply simp apply (rule use_valid [OF _ c], assumption+) apply (rule use_valid [OF _ r], assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> f \<lbrace>\<lambda>r. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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> (\<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (aa, bb) b) \<and> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> (\<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (aa, bb) b) \<and> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (aa, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, ba) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, bb) s; untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cdt b (?a38 s a b aa ba ab bb, ?b40 s a b aa ba ab bb) = Some (?a34 s a b aa ba ab bb, ?b36 s a b aa ba ab bb) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (?a34 s a b aa ba ab bb, ?b36 s a b aa ba ab bb) s \<and> cte_wp_at ((\<noteq>) NullCap) (?a38 s a b aa ba ab bb, ?b40 s a b aa ba ab bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s \<and> cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) b \<and> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) b
 2. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s
 2. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(a, b) \<in> fst (f s); untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (ab, bb) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>untyped_mdb (cdt b) (caps_of_state s); descendants_inc (cdt b) (caps_of_state s); no_mloop (cdt b); untyped_inc (cdt b) (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 b) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s = cdt b; cdt b (ab, bb) = Some (aa, ba); cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; cte_wp_at ((\<noteq>) NullCap) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) (ab, bb) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state b) \<and> descendants_inc (cdt b) (caps_of_state b) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state b) \<and> ut_revocable (is_original_cap b) (caps_of_state b) \<and> irq_revocable (is_original_cap b) (caps_of_state b) \<and> reply_master_revocable (is_original_cap b) (caps_of_state b) \<and> reply_mdb (cdt b) (caps_of_state b) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state s) \<and> descendants_inc (cdt b) (caps_of_state s) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (caps_of_state s) \<and> ut_revocable (is_original_cap b) (caps_of_state s) \<and> irq_revocable (is_original_cap b) (caps_of_state s) \<and> reply_master_revocable (is_original_cap b) (caps_of_state s) \<and> reply_mdb (cdt b) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap b) (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) 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); cdt s = cdt b\<rbrakk> \<Longrightarrow> untyped_mdb (cdt b) (caps_of_state s) \<and> descendants_inc (cdt b) (caps_of_state s) \<and> no_mloop (cdt b) \<and> untyped_inc (cdt b) (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 b) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s) proof (prove)
goal:
No subgoals!