theory Untyped_R

lemma untyped_inc_mdbD:
  "\<lbrakk> sameRegionAs cap cap'; isUntypedCap cap;
      ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node');
        untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes \<rbrakk>
     \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or>
          (isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap'
                  \<and> sameRegionAs cap' cap
                  \<and> ctes \<turnstile> p' \<rightarrow> p)" apply (subgoal_tac "untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> sameRegionAs cap' cap") apply (cases "isUntypedCap cap'") apply (drule(4) untyped_incD'[where p=p and p'=p']) apply (erule sameRegionAsE, simp_all add: untypedCapRange)[1] apply (cases "untypedRange cap = untypedRange cap'") apply simp apply (elim disjE conjE) apply (simp only: simp_thms descendants_of'_D)+ apply (elim disjE conjE) apply (simp add: subset_iff_psubset_eq) apply (elim disjE) apply (simp add:descendants_of'_D)+ apply (clarsimp simp:descendants_of'_def) apply (clarsimp simp: isCap_simps) apply clarsimp apply (erule sameRegionAsE) apply simp apply (drule(1) untyped_mdbD',simp) apply (simp add:untypedCapRange) apply blast apply simp apply assumption apply (simp add:descendants_of'_def) apply (clarsimp simp:isCap_simps) apply (simp add:isCap_simps) apply (clarsimp simp:sameRegionAs_def3) apply (erule disjE) apply (intro conjI) apply blast apply (simp add:untypedCapRange) apply (erule subset_trans[OF _ untypedRange_in_capRange]) apply clarsimp apply (rule untypedRange_not_emptyD) apply (simp add:untypedCapRange) apply blast apply (clarsimp simp:isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isUntypedCap cap; untypedRange cap = untypedRange cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isUntypedCap cap; untypedRange cap \<noteq> untypedRange cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 6. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; global.sameRegionAs cap' cap; isUntypedCap cap'; p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'; untypedRange cap' \<noteq> {}; isUntypedCap cap; untypedRange cap = untypedRange cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isUntypedCap cap; untypedRange cap \<noteq> untypedRange cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 6. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (8 subgoals):
 1. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; isUntypedCap cap; untypedRange cap = untypedRange cap'; p' \<in> descendants_of' p ctes; usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; isUntypedCap cap; untypedRange cap = untypedRange cap'; p \<in> descendants_of' p' ctes; usableUntypedRange cap' = {}\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; isUntypedCap cap; untypedRange cap = untypedRange cap'; p = p'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isUntypedCap cap; untypedRange cap \<noteq> untypedRange cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 5. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 6. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 7. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 8. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; untypedRange cap' \<subseteq> untypedRange cap; isArchPageCap cap; isArchPageCap cap'; untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}; untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; untypedRange cap' \<subset> untypedRange cap \<or> untypedRange cap' = untypedRange cap; isArchPageCap cap; isArchPageCap cap'; untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}; untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (5 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; isArchPageCap cap; isArchPageCap cap'; untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}; untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'; untypedRange cap' \<subset> untypedRange cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap = untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap' \<noteq> {}; isArchPageCap cap; isArchPageCap cap'; untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}; untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}; untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap = untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; global.sameRegionAs cap' cap; isUntypedCap cap'; untypedRange cap \<noteq> {}; isArchPageCap cap; isArchPageCap cap'; p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'; untypedRange cap' = untypedRange cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; isUntypedCap cap'; (untypedRange cap \<subseteq> untypedRange cap' \<or> untypedRange cap' \<subseteq> untypedRange cap \<or> untypedRange cap \<inter> untypedRange cap' = {}) \<and> (untypedRange cap \<subset> untypedRange cap' \<longrightarrow> p \<in> descendants_of' p' ctes \<and> untypedRange cap \<inter> usableUntypedRange cap' = {}) \<and> (untypedRange cap' \<subset> untypedRange cap \<longrightarrow> p' \<in> descendants_of' p ctes \<and> untypedRange cap' \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap = untypedRange cap' \<longrightarrow> p' \<in> descendants_of' p ctes \<and> usableUntypedRange cap = {} \<or> p \<in> descendants_of' p' ctes \<and> usableUntypedRange cap' = {} \<or> p = p'); isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' \<or> p = p' \<or> isUntypedCap cap' \<and> untypedRange cap \<subseteq> untypedRange cap' \<and> global.sameRegionAs cap' cap \<and> ctes \<turnstile> p' \<rightarrow> p
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (5 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 4. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (7 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap' node')) \<inter> untypedRange (cteCap (CTE cap node)) \<noteq> {}
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap' node'))
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' ctes
 4. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap; p' \<in> descendants_of' p ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 5. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 6. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 7. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (7 subgoals):
 1. \<lbrakk>ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> untypedRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> untypedRange cap \<noteq> {}
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap' node'))
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' ctes
 4. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap; p' \<in> descendants_of' p ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 5. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 6. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 7. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (6 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap' node'))
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' ctes
 3. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap; p' \<in> descendants_of' p ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 4. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 5. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 6. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (5 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> untyped_mdb' ctes
 2. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap; p' \<in> descendants_of' p ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 4. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 5. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap; p' \<in> descendants_of' p ctes\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 4. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 3. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap; \<not> isUntypedCap cap'; p \<noteq> p'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
 2. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> untypedRange cap' \<longrightarrow> global.sameRegionAs cap' cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'; isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap)
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {}
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange cap'
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap
 4. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange cap'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> untypedRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<subseteq> capRange cap'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap
 3. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap' \<longrightarrow> \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap'
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap' \<longrightarrow> \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> untypedRange cap' \<noteq> {}
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> untypedRange cap; isArchPageCap cap' \<longrightarrow> \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> untypedRange cap' \<noteq> {}
 2. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap cap; ctes p = Some (CTE cap node); ctes p' = Some (CTE cap' node'); untyped_inc' ctes; untyped_mdb' ctes; no_loops ctes; untypedRange cap \<subseteq> untypedRange cap'; isIRQControlCap cap' \<longrightarrow> \<not> isIRQHandlerCap cap; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} \<and> capRange cap \<subseteq> capRange cap' \<and> (isUntypedCap cap' \<or> isArchPageCap cap' \<and> isArchPageCap cap) proof (prove)
goal:
No subgoals!