theory Untyped_R

lemma updateFreeIndex_updateCap_caps_no_overlap'':
  "\<lbrace>\<lambda>s. isUntypedCap cap \<and> caps_no_overlap'' ptr sz s \<and>
        cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace>
   updateCap src (capFreeIndex_update (\<lambda>_. index) cap)
   \<lbrace>\<lambda>r s. caps_no_overlap'' ptr sz s\<rbrace>" apply (clarsimp simp:caps_no_overlap''_def) apply (wp updateCap_ctes_of_wp) apply (clarsimp simp: modify_map_def ran_def cte_wp_at_ctes_of
              simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                        Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex) apply (case_tac "a = src") apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
     Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex) apply (erule subsetD[rotated]) apply (elim allE impE) apply fastforce apply (clarsimp simp:isCap_simps) apply (erule subset_trans) apply (clarsimp simp:isCap_simps) apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
     Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex) apply (erule subsetD[rotated]) apply (elim allE impE) prefer 2 apply assumption apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isUntypedCap cap \<and> caps_no_overlap'' ptr sz s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r. caps_no_overlap'' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isUntypedCap cap \<and> (\<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. \<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. isUntypedCap cap \<and> (\<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s \<Longrightarrow> \<forall>cte\<in>ran (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap))). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a = src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (4 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>a. ctes_of s a = Some (?cte38 s ctea x)
 2. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange (cteCap (?cte38 s ctea x)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 3. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap (?cte38 s ctea x))\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 4. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (3 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange (cteCap ctea) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 3. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap ctea)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange (cteCap ctea) \<subseteq> untypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea))
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; a = src \<longrightarrow> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) ctea = cte; a \<noteq> src \<longrightarrow> ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; a \<noteq> src\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>aa. ctes_of s aa = Some (?cte69 s cte ctea a x)
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> untypedRange (cteCap (?cte69 s cte ctea a x)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 3. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap (?cte69 s cte ctea a x))\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> untypedRange (cteCap (?cte69 s cte ctea a x)) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>aa. ctes_of s aa = Some (?cte69 s cte ctea a x)
 3. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap (?cte69 s cte ctea a x))\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>a. ctes_of s a = Some cte
 2. \<And>s cte ctea a x. \<lbrakk>isUntypedCap (cteCap ctea); ctes_of s src = Some ctea; cap = cteCap ctea; ctes_of s a = Some cte; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; a \<noteq> src; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) proof (prove)
goal:
No subgoals!