theory Retype_AI

lemma valid_mdb_rep2:
  "valid_mdb = (\<lambda>s. valid_mdb2 (null_filter (caps_of_state s)) (cdt s) (is_original_cap s))" apply (simp add: valid_mdb_def valid_mdb2_def
                   untyped_mdb_def no_mloop_def untyped_inc_def) apply (rule ext) apply (rule conj_cong2) apply (simp add: mdb_cte_at_def) apply (rule arg_cong[where f=All, OF ext])+ apply ((clarsimp simp: cte_wp_at_caps_of_state null_filter_def
                | rule conjI iffI
                | drule iffD1 [OF not_None_eq, OF not_sym])+)[1] apply (rule conj_cong) apply (rule arg_cong[where f=All, OF ext])+ apply (clarsimp simp: null_filter_def) apply (rule conj_cong) apply (simp add:descendants_inc_null_filter) apply (rule arg_cong2 [where f="(\<and>)"]) apply (rule refl) apply (rule arg_cong2 [where f="(\<and>)"]) prefer 2 apply (rule arg_cong2 [where f="(\<and>)"]) apply (simp add: ut_revocable_def null_filter_def del: split_paired_All) apply (auto simp: is_cap_simps)[1] apply (rule arg_cong2 [where f="(\<and>)"]) apply (simp add: irq_revocable_def null_filter_def del: split_paired_All) apply auto[1] apply (rule arg_cong2 [where f="(\<and>)"]) apply (simp add: reply_master_revocable_def null_filter_def del: split_paired_All) apply (auto simp: is_cap_simps)[1] apply (simp add: reply_mdb_def null_filter_def) apply (rule arg_cong2 [where f="(\<and>)"]) apply (simp add: reply_caps_mdb_def
                del: split_paired_Ex split_paired_All) apply (fastforce elim!: allEI exEI
                  simp del: split_paired_Ex split_paired_All) apply (rule arg_cong2 [where f="(\<and>)"]) apply (fastforce simp: reply_masters_mdb_def elim!: allEI
                 simp del: split_paired_All split: if_split_asm) apply (fastforce simp: valid_arch_mdb_null_filter[simplified null_filter_def]) apply (rule arg_cong[where f=All, OF ext])+ apply ((clarsimp simp: cte_wp_at_caps_of_state null_filter_def
               | rule conjI iffI
               | drule iffD1 [OF not_None_eq, OF not_sym])+)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb = (\<lambda>s. valid_mdb2 (null_filter (caps_of_state s)) (cdt s) (is_original_cap s)) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> (\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = (\<lambda>s. (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> None \<noteq> null_filter (caps_of_state s) (a, b) \<and> None \<noteq> null_filter (caps_of_state s) (aa, ba) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (a, b) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (aa, ba)) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<and> (\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> None \<noteq> null_filter (caps_of_state s) (a, b) \<and> None \<noteq> null_filter (caps_of_state s) (aa, ba) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (a, b) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (aa, ba)) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) = (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> None \<noteq> null_filter (caps_of_state s) (a, b) \<and> None \<noteq> null_filter (caps_of_state s) (aa, ba) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (a, b) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (aa, ba))
 2. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> ((\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>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) = (\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> None \<noteq> null_filter (caps_of_state s) (a, b) \<and> None \<noteq> null_filter (caps_of_state s) (aa, ba) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (a, b) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (aa, ba))
 2. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> ((\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb xc. (cdt s (xb, xc) = Some (x, xa) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (x, xa) s \<and> cte_wp_at ((\<noteq>) NullCap) (xb, xc) s) = (cdt s (xb, xc) = Some (x, xa) \<longrightarrow> None \<noteq> null_filter (caps_of_state s) (x, xa) \<and> None \<noteq> null_filter (caps_of_state s) (xb, xc) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (x, xa) \<and> Some NullCap \<noteq> null_filter (caps_of_state s) (xb, xc))
 2. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> ((\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> ((\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) \<and> descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> (\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))\<rbrakk> \<Longrightarrow> (descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = (descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb xc xd. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s) \<Longrightarrow> (caps_of_state s (x, xa) = Some xd \<longrightarrow> is_untyped_cap xd \<longrightarrow> (\<forall>cap'. caps_of_state s (xb, xc) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range xd \<noteq> {} \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s))) = (null_filter (caps_of_state s) (x, xa) = Some xd \<longrightarrow> is_untyped_cap xd \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (xb, xc) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range xd \<noteq> {} \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))\<rbrakk> \<Longrightarrow> (descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = (descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))\<rbrakk> \<Longrightarrow> (descendants_inc (cdt s) (caps_of_state s) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = (descendants_inc (cdt s) (null_filter (caps_of_state s)) \<and> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))\<rbrakk> \<Longrightarrow> descendants_inc (cdt s) (caps_of_state s) = descendants_inc (cdt s) (null_filter (caps_of_state s))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> ((\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> ((\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) \<and> (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+) = (\<forall>a b. ((a, b), a, b) \<notin> (cdt_parent_rel (cdt s))\<^sup>+)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> ((\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> ((\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<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)) = ((\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) \<and> ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (ut_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> ut_revocable (is_original_cap s) (caps_of_state s) = ut_revocable (is_original_cap s) (null_filter (caps_of_state s))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_original_cap s p) = (\<forall>p. caps_of_state s p \<noteq> Some NullCap \<longrightarrow> (\<forall>cap. caps_of_state s p = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_original_cap s p))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (irq_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) (caps_of_state s) = irq_revocable (is_original_cap s) (null_filter (caps_of_state s))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (\<forall>p. caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p) = (\<forall>p. caps_of_state s p \<noteq> Some NullCap \<longrightarrow> caps_of_state s p = Some IRQControlCap \<longrightarrow> is_original_cap s p)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (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)) = (reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s)) \<and> reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> reply_master_revocable (is_original_cap s) (caps_of_state s) = reply_master_revocable (is_original_cap s) (null_filter (caps_of_state s))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s p) = (\<forall>p. caps_of_state s p \<noteq> Some NullCap \<longrightarrow> (\<forall>cap. caps_of_state s p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s p))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_mdb (cdt s) (null_filter (caps_of_state s)) \<and> valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (reply_caps_mdb (cdt s) (caps_of_state s) \<and> reply_masters_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_caps_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x) \<and> reply_masters_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x) \<and> valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> reply_caps_mdb (cdt s) (caps_of_state s) = reply_caps_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (reply_masters_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_masters_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x) \<and> valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (\<forall>ptr t. (\<exists>rights. caps_of_state s ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. cdt s ptr = Some ptr' \<and> (\<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t True rights')))) = (\<forall>ptr. caps_of_state s ptr \<noteq> Some NullCap \<longrightarrow> (\<forall>t. (\<exists>rights. caps_of_state s ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. caps_of_state s ptr' \<noteq> Some NullCap \<and> (caps_of_state s ptr' \<noteq> Some NullCap \<longrightarrow> cdt s ptr = Some ptr' \<and> (\<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t True rights'))))))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (reply_masters_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_masters_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x) \<and> valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x))
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> (reply_masters_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)) = (reply_masters_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x) \<and> valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x))
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> reply_masters_mdb (cdt s) (caps_of_state s) = reply_masters_mdb (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) (caps_of_state s) = valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)
 3. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. (if caps_of_state s (a, b) = Some NullCap then None else caps_of_state s (a, b)) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. (if caps_of_state s (aa, ba) = Some NullCap then None else caps_of_state s (aa, ba)) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)\<rbrakk> \<Longrightarrow> valid_arch_mdb (is_original_cap s) (caps_of_state s) = valid_arch_mdb (is_original_cap s) (\<lambda>x. if caps_of_state s x = Some NullCap then None else caps_of_state s x)
 2. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (\<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) = (\<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) (cdt s) \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc xd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); \<forall>a b aa ba c. null_filter (caps_of_state s) (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (aa, ba) = Some c' \<longrightarrow> obj_refs c' \<inter> untyped_range c \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)); descendants_inc (cdt s) (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> (caps_of_state s (x, xa) = Some xd \<longrightarrow> is_untyped_cap xd \<longrightarrow> (\<forall>c'. caps_of_state s (xb, xc) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range xd \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range xd \<or> untyped_range xd \<inter> untyped_range c' = {}) \<and> (untyped_range xd \<subset> untyped_range c' \<longrightarrow> (x, xa) \<in> descendants_of (xb, xc) (cdt s) \<and> untyped_range xd \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range xd \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range xd = {}) \<and> (untyped_range xd = untyped_range c' \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s) \<and> usable_untyped_range xd = {} \<or> (x, xa) \<in> descendants_of (xb, xc) (cdt s) \<and> usable_untyped_range c' = {} \<or> x = xb \<and> xa = xc))) = (null_filter (caps_of_state s) (x, xa) = Some xd \<longrightarrow> is_untyped_cap xd \<longrightarrow> (\<forall>c'. null_filter (caps_of_state s) (xb, xc) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range xd \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range xd \<or> untyped_range xd \<inter> untyped_range c' = {}) \<and> (untyped_range xd \<subset> untyped_range c' \<longrightarrow> (x, xa) \<in> descendants_of (xb, xc) (cdt s) \<and> untyped_range xd \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range xd \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s) \<and> untyped_range c' \<inter> usable_untyped_range xd = {}) \<and> (untyped_range xd = untyped_range c' \<longrightarrow> (xb, xc) \<in> descendants_of (x, xa) (cdt s) \<and> usable_untyped_range xd = {} \<or> (x, xa) \<in> descendants_of (xb, xc) (cdt s) \<and> usable_untyped_range c' = {} \<or> x = xb \<and> xa = xc))) proof (prove)
goal:
No subgoals!