theory Untyped_R

lemma inv_untyped_corres_helper1:
  "list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps
   \<Longrightarrow>
   corres dc
      (\<lambda>s. pspace_aligned s \<and> pspace_distinct s
          \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s
          \<and> cte_wp_at is_untyped_cap p s
          \<and> (\<forall>tup \<in> set (zip crefs orefs).
              cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s)
          \<and> (\<forall>tup \<in> set (zip crefs orefs).
              descendants_range (default_cap tp (snd tup) sz d) p s)
          \<and> (\<forall>tup \<in> set (zip crefs orefs).
              caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s)
          \<and> (\<forall>tup \<in> set (zip crefs orefs). real_cte_at (fst tup) s)
          \<and> (\<forall>tup \<in> set (zip crefs orefs).
              cte_wp_at ((=) cap.NullCap) (fst tup) s)
          \<and> distinct (p # (map fst (zip crefs orefs)))
          \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (zip crefs orefs))
          \<and> (\<forall>tup \<in> set (zip crefs orefs).
              valid_cap (default_cap tp (snd tup) sz d) s))
      (\<lambda>s. (\<forall>tup \<in> set (zip (map cte_map crefs) cps). valid_cap' (snd tup) s)
         \<and> (\<forall>tup \<in> set (zip (map cte_map crefs) cps). cte_wp_at' (\<lambda>c. cteCap c = NullCap) (fst tup) s)
         \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                         (\<forall>tup \<in> set (zip (map cte_map crefs) cps).
                               sameRegionAs (cteCap cte) (snd tup)))
              (cte_map p) s
         \<and> distinct ((cte_map p) # (map fst (zip (map cte_map crefs) cps)))
         \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s
         \<and> (\<forall>tup \<in> set (zip (map cte_map crefs) cps). descendants_range' (snd tup) (cte_map p) (ctes_of s))
         \<and> (\<forall>tup \<in> set (zip (map cte_map crefs) cps).
              caps_overlap_reserved' (capRange (snd tup)) s)
         \<and> distinct_sets (map capRange (map snd (zip (map cte_map crefs) cps))))
      (sequence_x (map (create_cap tp sz p d) (zip crefs orefs)))
      (zipWithM_x (insertNewCap (cte_map p))
             ((map cte_map crefs)) cps)" apply (simp add: zipWithM_x_def zipWith_def split_def) apply (fold mapM_x_def) apply (rule corres_list_all2_mapM_) apply (rule corres_guard_imp) apply (erule insertNewCap_corres) apply (clarsimp simp: cte_wp_at_def is_cap_simps) apply (clarsimp simp: fun_upd_def cte_wp_at_ctes_of) apply clarsimp apply (rule hoare_pre, wp hoare_vcg_const_Ball_lift) apply clarsimp apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state
                           cap_range_def[where c="default_cap a b c d" for a b c d]) apply (drule(2) caps_overlap_reservedD[rotated]) apply (simp add:Int_ac) apply (rule conjI) apply (clarsimp simp: valid_cap_def) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule conjI) apply (clarsimp simp:Int_ac) apply (erule disjoint_subset2[rotated]) apply fastforce apply clarsimp apply (rule conjI) apply clarsimp apply (rule conjI) subgoal by fastforce apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_cap_def) apply (fastforce simp: image_def) apply (rule hoare_pre) apply (wp
              hoare_vcg_const_Ball_lift insertNewCap_valid_mdb hoare_vcg_all_lift
              insertNewCap_ranges
               | subst cte_wp_at_cteCaps_of)+ apply (subst(asm) cte_wp_at_cteCaps_of)+ apply (clarsimp simp only:) apply simp apply (rule conjI) apply clarsimp apply (thin_tac "cte_map p \<notin> S" for S) apply (erule notE, erule rev_image_eqI) apply simp apply (rule conjI,clarsimp+) apply (rule conjI,erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) apply (rule conjI,erule no_default_zombie) apply (rule conjI, clarsimp simp:Int_ac) apply fastforce apply (clarsimp simp:Int_ac valid_capAligned ) apply fastforce apply (rule list_all2_zip_split) apply (simp add: list_all2_map2 list_all2_refl) apply (simp add: list_all2_map1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> corres dc (\<lambda>s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). descendants_range (default_cap tp (snd tup) sz d) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> distinct (p # map fst (zip crefs orefs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz d)) (\<lambda>s. (\<forall>tup\<in>set (zip (map cte_map crefs) cps). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> distinct (cte_map p # map fst (zip (map cte_map crefs) cps)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd (zip (map cte_map crefs) cps)))) (sequence_x (map (create_cap tp sz p d) (zip crefs orefs))) (zipWithM_x (insertNewCap (cte_map p)) (map cte_map crefs) cps) proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> corres dc (\<lambda>s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). descendants_range (default_cap tp (snd tup) sz d) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> p \<notin> fst ` set (zip crefs orefs) \<and> distinct (map fst (zip crefs orefs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz d)) (\<lambda>s. (\<forall>tup\<in>set (zip (map cte_map crefs) cps). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (zip (map cte_map crefs) cps) \<and> distinct (map fst (zip (map cte_map crefs) cps)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (zip (map cte_map crefs) cps))) (sequence_x (map (create_cap tp sz p d) (zip crefs orefs))) (sequence_x (map (\<lambda>pa. insertNewCap (cte_map p) (fst pa) (snd pa)) (zip (map cte_map crefs) cps))) proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> corres dc (\<lambda>s. pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). descendants_range (default_cap tp (snd tup) sz d) p s) \<and> (\<forall>tup\<in>set (zip crefs orefs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> p \<notin> fst ` set (zip crefs orefs) \<and> distinct (map fst (zip crefs orefs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz d)) (\<lambda>s. (\<forall>tup\<in>set (zip (map cte_map crefs) cps). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (zip (map cte_map crefs) cps) \<and> distinct (map fst (zip (map cte_map crefs) cps)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (zip (map cte_map crefs) cps). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (zip (map cte_map crefs) cps))) (mapM_x (create_cap tp sz p d) (zip crefs orefs)) (mapM_x (\<lambda>pa. insertNewCap (cte_map p) (fst pa) (snd pa)) (zip (map cte_map crefs) cps)) proof (prove)
goal (4 subgoals):
 1. \<And>x xs y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)) (\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))) (create_cap tp sz p d x) (insertNewCap (cte_map p) (fst y) (snd y))
 2. \<And>x y xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d x \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 ?F4 (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> corres dc (?Q9 x xs y ys) (?Q'9 x xs y ys) (create_cap tp sz p d x) (insertNewCap (cte_map p) (fst y) (snd y))
 2. \<And>x xs y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps); pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p s) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). s \<turnstile> default_cap tp (snd tup) sz d)\<rbrakk> \<Longrightarrow> ?Q9 x xs y ys s
 3. \<And>x xs y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> ?Q'9 x xs y ys s
 4. \<And>x y xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (x # xs) (zip crefs orefs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d x \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 5. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; ?F4 x y; suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 6. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 ?F4 (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (5 subgoals):
 1. \<And>x xs y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps); pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p s) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). s \<turnstile> default_cap tp (snd tup) sz d)\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) cap.NullCap) (fst x) and pspace_aligned and pspace_distinct and valid_objs and valid_mdb and valid_list and cte_wp_at ((\<noteq>) cap.NullCap) p) s
 2. \<And>x xs y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst y) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd y)) (cte_map p) and valid_mdb' and pspace_aligned' and pspace_distinct' and valid_objs' and (\<lambda>s. descendants_range' (snd y) (cte_map p) (ctes_of s))) s
 3. \<And>x y xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d x \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 4. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 5. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>x xs y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst y) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd y)) (cte_map p) and valid_mdb' and pspace_aligned' and pspace_distinct' and valid_objs' and (\<lambda>s. descendants_range' (snd y) (cte_map p) (ctes_of s))) s
 2. \<And>x y xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d x \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>x y xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (x # xs) (zip crefs orefs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set (x # xs). descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set (x # xs). caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set (x # xs). real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set (x # xs). cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set (x # xs) \<and> distinct (map fst (x # xs)) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) (x # xs)) \<and> (\<forall>tup\<in>set (x # xs). a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d x \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>c. pspace_aligned c \<and> pspace_distinct c \<and> valid_objs c \<and> valid_mdb c \<and> valid_list c \<and> cte_wp_at is_untyped_cap p c \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p c \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p c) \<and> descendants_range (default_cap tp ba sz d) p c \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p c) \<and> caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) c \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) c) \<and> cap_table_at (length b) a c \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) c) \<and> cte_wp_at ((=) cap.NullCap) (a, b) c \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) c) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set xs \<and> (a, b) \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> c \<turnstile> default_cap tp ba sz d \<and> (\<forall>tup\<in>set xs. c \<turnstile> default_cap tp (snd tup) sz d)\<rbrace> create_cap tp sz p d ((a, b), ba) \<lbrace>\<lambda>rv a. pspace_aligned a \<and> pspace_distinct a \<and> valid_objs a \<and> valid_mdb a \<and> valid_list a \<and> cte_wp_at is_untyped_cap p a \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p a) \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p a) \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) a) \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) a) \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) a) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>tup\<in>set xs. a \<turnstile> default_cap tp (snd tup) sz d)\<rbrace>
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s \<and> cte_wp_at is_untyped_cap p s \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s \<and> (\<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s) \<and> descendants_range (default_cap tp ba sz d) p s \<and> (\<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s) \<and> caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s \<and> (\<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set xs. real_cte_at (fst tup) s) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set xs \<and> (a, b) \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> s \<turnstile> default_cap tp ba sz d \<and> (\<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> pspace_distinct s \<and> (valid_objs and valid_cap (default_cap tp ba sz d) and real_cte_at (a, b)) s \<and> (valid_mdb and valid_objs and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_refs (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<inter> usable_untyped_range c = {}) p and descendants_range (default_cap tp ba sz d) p and cte_wp_at ((=) cap.NullCap) (a, b) and K (cap_aligned (default_cap tp ba sz d))) s \<and> valid_list s \<and> (cte_wp_at is_untyped_cap p and K (p \<noteq> (a, b))) s \<and> (\<forall>x\<in>set xs. (cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd x) sz d) \<subseteq> untyped_range c) p and K (p \<noteq> (a, b))) s) \<and> (\<forall>x\<in>set xs. (descendants_range (default_cap tp (snd x) sz d) p and K (cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {}) and cte_wp_at ((\<noteq>) cap.NullCap) p and cte_wp_at ((=) cap.NullCap) (a, b) and valid_mdb) s) \<and> (\<forall>x\<in>set xs. (caps_overlap_reserved (untyped_range (default_cap tp (snd x) sz d)) and K (cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {}) and cte_wp_at ((\<noteq>) cap.NullCap) p and cte_wp_at ((=) cap.NullCap) (a, b) and valid_mdb and K (cap_aligned (default_cap tp ba sz d))) s) \<and> (\<forall>x\<in>set xs. real_cte_at (fst x) s) \<and> (\<forall>x\<in>set xs. (cte_wp_at ((=) cap.NullCap) (fst x) and K (fst x \<noteq> (a, b))) s) \<and> p \<notin> fst ` set xs \<and> distinct (map fst xs) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs) \<and> (\<forall>x\<in>set xs. s \<turnstile> default_cap tp (snd x) sz d)
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_refs (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<inter> usable_untyped_range c = {}) p s \<and> cap_aligned (default_cap tp ba sz d) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_refs (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz d) \<inter> usable_untyped_range c = {}) p s
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cap_aligned (default_cap tp ba sz d) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. untyped_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap \<and> obj_refs (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); (untyped_range (default_cap tp ba sz d) \<union> obj_refs (default_cap tp ba sz d)) \<inter> (\<Union>x\<in>set xs. untyped_range (default_cap tp (snd x) sz d) \<union> obj_refs (default_cap tp (snd x) sz d)) = {}; distinct_sets (map (\<lambda>tup. untyped_range (default_cap tp (snd tup) sz d) \<union> obj_refs (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; is_untyped_cap cap; caps_of_state s p = Some cap; untyped_range (default_cap tp ba sz d) \<subseteq> untyped_range cap; obj_refs (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp ba sz d) \<inter> usable_untyped_range cap = {}
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cap_aligned (default_cap tp ba sz d) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. untyped_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap \<and> obj_refs (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); (untyped_range (default_cap tp ba sz d) \<union> obj_refs (default_cap tp ba sz d)) \<inter> (\<Union>x\<in>set xs. untyped_range (default_cap tp (snd x) sz d) \<union> obj_refs (default_cap tp (snd x) sz d)) = {}; distinct_sets (map (\<lambda>tup. untyped_range (default_cap tp (snd tup) sz d) \<union> obj_refs (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; is_untyped_cap cap; untyped_range (default_cap tp ba sz d) \<subseteq> untyped_range cap; obj_refs (default_cap tp ba sz d) \<subseteq> untyped_range cap; usable_untyped_range cap \<inter> untyped_range (default_cap tp ba sz d) = {}\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp ba sz d) \<inter> usable_untyped_range cap = {}
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cap_aligned (default_cap tp ba sz d) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cap_aligned (default_cap tp ba sz d) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> cap_aligned (default_cap tp ba sz d)
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s) \<and> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cap.NullCap \<noteq> cap
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (5 subgoals):
 1. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd sz d) \<inter> cap_range (default_cap tp ba sz d) = {}
 2. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap.NullCap \<noteq> cap
 3. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 4. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 5. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (5 subgoals):
 1. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap_range (default_cap tp ba sz d) \<inter> cap_range (default_cap tp bd sz d) = {}
 2. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap.NullCap \<noteq> cap
 3. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 4. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 5. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (5 subgoals):
 1. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd sz d) \<subseteq> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d))
 2. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap.NullCap \<noteq> cap
 3. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 4. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 5. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s aa bc bd cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; \<forall>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range cap; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; caps_of_state s (a, b) = Some cap.NullCap; \<forall>tup\<in>set xs. caps_of_state s (fst tup) = Some cap.NullCap; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs; is_untyped_cap cap; caps_of_state s p = Some cap; cap_range (default_cap tp ba sz d) \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> cap.NullCap \<noteq> cap
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)) \<and> (\<forall>x\<in>set xs. fst x \<noteq> (a, b))
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. cap_range (default_cap tp (snd x) sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. fst x \<noteq> (a, b)
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s aa bc bd. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd sz d) \<inter> cap_range (default_cap tp ba sz d) = {} \<and> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. fst x \<noteq> (a, b)
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (5 subgoals):
 1. \<And>a b ba bb xs s aa bc bd. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd sz d) \<inter> cap_range (default_cap tp ba sz d) = {}
 2. \<And>a b ba bb xs s aa bc bd. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)
 3. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. fst x \<noteq> (a, b)
 4. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 5. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a_, b_), ba_) # xs_) (zip crefs orefs); cap_relation (default_cap tp ba_ sz d) bb_; pspace_aligned s_; pspace_distinct s_; valid_objs s_; valid_mdb s_; valid_list s_; cte_wp_at is_untyped_cap p s_; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba_ sz d) \<subseteq> untyped_range c) p s_; \<forall>tup\<in>set xs_. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s_; descendants_range (default_cap tp ba_ sz d) p s_; \<forall>tup\<in>set xs_. descendants_range (default_cap tp (snd tup) sz d) p s_; caps_overlap_reserved (untyped_range (default_cap tp ba_ sz d)) s_; \<forall>tup\<in>set xs_. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s_; cap_table_at (length b_) a_ s_; \<forall>tup\<in>set xs_. real_cte_at (fst tup) s_; cte_wp_at ((=) cap.NullCap) (a_, b_) s_; \<forall>tup\<in>set xs_. cte_wp_at ((=) cap.NullCap) (fst tup) s_; p \<noteq> (a_, b_); p \<notin> fst ` set xs_; (a_, b_) \<notin> fst ` set xs_; distinct (map fst xs_); cap_range (default_cap tp ba_ sz d) \<inter> (\<Union>tup\<in>set xs_. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs_); s_ \<turnstile> default_cap tp ba_ sz d; \<forall>tup\<in>set xs_. s_ \<turnstile> default_cap tp (snd tup) sz d; ((aa_, bc_), bd_) \<in> set xs_\<rbrakk> \<Longrightarrow> cap_range (default_cap tp bd_ sz d) \<inter> cap_range (default_cap tp ba_ sz d) = {} proof (prove)
goal (4 subgoals):
 1. \<And>a b ba bb xs s aa bc bd. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d; ((aa, bc), bd) \<in> set xs\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cap_aligned (default_cap tp ba sz d)
 2. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. fst x \<noteq> (a, b)
 3. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 4. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb xs s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix (((a, b), ba) # xs) (zip crefs orefs); cap_relation (default_cap tp ba sz d) bb; pspace_aligned s; pspace_distinct s; valid_objs s; valid_mdb s; valid_list s; cte_wp_at is_untyped_cap p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz d) \<subseteq> untyped_range c) p s; \<forall>tup\<in>set xs. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz d) \<subseteq> untyped_range c) p s; descendants_range (default_cap tp ba sz d) p s; \<forall>tup\<in>set xs. descendants_range (default_cap tp (snd tup) sz d) p s; caps_overlap_reserved (untyped_range (default_cap tp ba sz d)) s; \<forall>tup\<in>set xs. caps_overlap_reserved (untyped_range (default_cap tp (snd tup) sz d)) s; cap_table_at (length b) a s; \<forall>tup\<in>set xs. real_cte_at (fst tup) s; cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set xs. cte_wp_at ((=) cap.NullCap) (fst tup) s; p \<noteq> (a, b); p \<notin> fst ` set xs; (a, b) \<notin> fst ` set xs; distinct (map fst xs); cap_range (default_cap tp ba sz d) \<inter> (\<Union>tup\<in>set xs. cap_range (default_cap tp (snd tup) sz d)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz d)) xs); s \<turnstile> default_cap tp ba sz d; \<forall>tup\<in>set xs. s \<turnstile> default_cap tp (snd tup) sz d\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. fst x \<noteq> (a, b)
 2. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>x y ys. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps)\<rbrakk> \<Longrightarrow> \<lbrace>?Q254 x y ys\<rbrace> insertNewCap (cte_map p) (fst y) (snd y) \<lbrace>\<lambda>rv a. (\<forall>tup\<in>set ys. valid_cap' (snd tup) a) \<and> (\<forall>tup\<in>set ys. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) a) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ys. global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) a \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> valid_mdb' a \<and> valid_objs' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of a)) \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) a) \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrace>
 2. \<And>x y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> ?Q254 x y ys s
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>x y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (fst tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs (cteCap cte) (snd tup))) (cte_map p) s \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ys. valid_cap' (snd x) s) \<and> (\<forall>x\<in>set ys. \<exists>cap. ((cteCaps_of s)(fst y \<mapsto> snd y)) (fst x) = Some cap \<and> cap = capability.NullCap) \<and> (\<exists>cap. ((cteCaps_of s)(fst y \<mapsto> snd y)) (cte_map p) = Some cap \<and> isUntypedCap cap \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup))) \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> (valid_mdb' and valid_objs' and K (fst y \<noteq> cte_map p) and caps_overlap_reserved' (untypedRange (snd y)) and (\<lambda>a. \<exists>cap. cteCaps_of a (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) and K (\<not> isZombie (snd y)) and valid_cap' (snd y) and (\<lambda>s. descendants_range' (snd y) (cte_map p) (ctes_of s))) s \<and> (valid_objs' and valid_cap' (snd y) and pspace_aligned' and pspace_distinct') s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>x\<in>set ys. descendants_range' (snd x) (cte_map p) (ctes_of s) \<and> descendants_range' (snd y) (cte_map p) (ctes_of s) \<and> capRange (snd x) \<inter> capRange (snd y) = {} \<and> (\<exists>cap. cteCaps_of s (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) \<and> valid_mdb' s \<and> valid_objs' s) \<and> (\<forall>x\<in>set ys. caps_overlap_reserved' (capRange (snd x)) s \<and> capRange (snd x) \<inter> capRange (snd y) = {} \<and> capAligned (snd y) \<and> (\<exists>cap. cteCaps_of s (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) \<and> valid_mdb' s \<and> valid_objs' s) \<and> distinct_sets (map (capRange \<circ> snd) ys)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>x y ys s. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y); suffix (y # ys) (zip (map cte_map crefs) cps); (\<forall>tup\<in>set (y # ys). valid_cap' (snd tup) s) \<and> (\<forall>tup\<in>set (y # ys). \<exists>cap. cteCaps_of s (fst tup) = Some cap \<and> cap = capability.NullCap) \<and> (\<exists>cap. cteCaps_of s (cte_map p) = Some cap \<and> isUntypedCap cap \<and> (\<forall>tup\<in>set (y # ys). global.sameRegionAs cap (snd tup))) \<and> cte_map p \<notin> fst ` set (y # ys) \<and> distinct (map fst (y # ys)) \<and> valid_mdb' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>tup\<in>set (y # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s)) \<and> (\<forall>tup\<in>set (y # ys). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) (y # ys))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ys. valid_cap' (snd x) s) \<and> (\<forall>x\<in>set ys. \<exists>cap. ((cteCaps_of s)(fst y \<mapsto> snd y)) (fst x) = Some cap \<and> cap = capability.NullCap) \<and> (\<exists>cap. ((cteCaps_of s)(fst y \<mapsto> snd y)) (cte_map p) = Some cap \<and> isUntypedCap cap \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup))) \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> (valid_mdb' and valid_objs' and K (fst y \<noteq> cte_map p) and caps_overlap_reserved' (untypedRange (snd y)) and (\<lambda>a. \<exists>cap. cteCaps_of a (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) and K (\<not> isZombie (snd y)) and valid_cap' (snd y) and (\<lambda>s. descendants_range' (snd y) (cte_map p) (ctes_of s))) s \<and> (valid_objs' and valid_cap' (snd y) and pspace_aligned' and pspace_distinct') s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<forall>x\<in>set ys. descendants_range' (snd x) (cte_map p) (ctes_of s) \<and> descendants_range' (snd y) (cte_map p) (ctes_of s) \<and> capRange (snd x) \<inter> capRange (snd y) = {} \<and> (\<exists>cap. cteCaps_of s (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) \<and> valid_mdb' s \<and> valid_objs' s) \<and> (\<forall>x\<in>set ys. caps_overlap_reserved' (capRange (snd x)) s \<and> capRange (snd x) \<inter> capRange (snd y) = {} \<and> capAligned (snd y) \<and> (\<exists>cap. cteCaps_of s (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd y)) \<and> valid_mdb' s \<and> valid_objs' s) \<and> distinct_sets (map (capRange \<circ> snd) ys)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((aa, bb) # ys) (zip (map cte_map crefs) cps); fst (aa, bb) = cte_map (fst ((a, b), ba)); cap_relation (default_cap tp (snd ((a, b), ba)) sz d) (snd (aa, bb)); \<forall>tup\<in>set ((aa, bb) # ys). valid_cap' (snd tup) s; \<forall>tup\<in>set ((aa, bb) # ys). \<exists>cap. cteCaps_of s (fst tup) = Some cap \<and> cap = capability.NullCap; cte_map p \<notin> fst ` set ((aa, bb) # ys); cteCaps_of s (cte_map p) = Some cap; distinct (map fst ((aa, bb) # ys)); isUntypedCap cap; \<forall>tup\<in>set ((aa, bb) # ys). global.sameRegionAs cap (snd tup); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; \<forall>tup\<in>set ((aa, bb) # ys). descendants_range' (snd tup) (cte_map p) (ctes_of s); \<forall>tup\<in>set ((aa, bb) # ys). caps_overlap_reserved' (capRange (snd tup)) s; distinct_sets (map (capRange \<circ> snd) ((aa, bb) # ys))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ys. valid_cap' (snd x) s) \<and> (\<forall>x\<in>set ys. \<exists>cap. ((cteCaps_of s)(cte_map (fst ((a, b), ba)) \<mapsto> snd (aa, bb))) (fst x) = Some cap \<and> cap = capability.NullCap) \<and> (\<exists>cap. ((cteCaps_of s)(cte_map (fst ((a, b), ba)) \<mapsto> snd (aa, bb))) (cte_map p) = Some cap \<and> isUntypedCap cap \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup))) \<and> cte_map p \<notin> fst ` set ys \<and> distinct (map fst ys) \<and> (valid_mdb' and valid_objs' and K (cte_map (fst ((a, b), ba)) \<noteq> cte_map p) and caps_overlap_reserved' (untypedRange (snd (aa, bb))) and (\<lambda>a. \<exists>cap. cteCaps_of a (cte_map p) = Some cap \<and> isUntypedCap cap \<and> global.sameRegionAs cap (snd (aa, bb))) and K (\<not> isZombie (snd (aa, bb))) and valid_cap' (snd (aa, bb)) and (\<lambda>s. descendants_range' (snd (aa, bb)) (cte_map p) (ctes_of s))) s \<and> (valid_objs' and valid_cap' (snd (aa, bb)) and pspace_aligned' and pspace_distinct') s \<and> True \<and> True \<and> (\<forall>x\<in>set ys. descendants_range' (snd x) (cte_map p) (ctes_of s) \<and> descendants_range' (snd (aa, bb)) (cte_map p) (ctes_of s) \<and> capRange (snd x) \<inter> capRange (snd (aa, bb)) = {} \<and> (\<exists>capa. Some cap = Some capa \<and> isUntypedCap capa \<and> global.sameRegionAs capa (snd (aa, bb))) \<and> True \<and> True) \<and> (\<forall>x\<in>set ys. caps_overlap_reserved' (capRange (snd x)) s \<and> capRange (snd x) \<inter> capRange (snd (aa, bb)) = {} \<and> capAligned (snd (aa, bb)) \<and> (\<exists>capa. Some cap = Some capa \<and> isUntypedCap capa \<and> global.sameRegionAs capa (snd (aa, bb))) \<and> True \<and> True) \<and> distinct_sets (map (capRange \<circ> snd) ys)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> ((\<exists>x\<in>set ys. fst x = cte_map (a, b)) \<longrightarrow> bb = capability.NullCap) \<and> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>set ys. fst x = cte_map (a, b)) \<longrightarrow> bb = capability.NullCap
 2. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb ys s cap bc. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys); (cte_map (a, b), bc) \<in> set ys\<rbrakk> \<Longrightarrow> bb = capability.NullCap
 2. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb ys s cap bc. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys); (cte_map (a, b), bc) \<in> set ys\<rbrakk> \<Longrightarrow> bb = capability.NullCap
 2. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb ys s cap bc. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) = fst (cte_map (a, b), bc)
 2. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); aa = cte_map (a, b); cap_relation (default_cap tp ba sz d) bb; valid_cap' bb s \<and> (\<forall>tup\<in>set ys. valid_cap' (snd tup) s); cteCaps_of s (cte_map (a, b)) = Some capability.NullCap \<and> (\<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap); cte_map p \<noteq> cte_map (a, b) \<and> cte_map p \<notin> fst ` set ys; cteCaps_of s (cte_map p) = Some cap; cte_map (a, b) \<notin> fst ` set ys \<and> distinct (map fst ys); isUntypedCap cap; global.sameRegionAs cap bb \<and> (\<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup)); valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; descendants_range' bb (cte_map p) (ctes_of s) \<and> (\<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s)); caps_overlap_reserved' (capRange bb) s \<and> (\<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s); capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> cte_map (a, b) \<noteq> cte_map p \<and> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (untypedRange bb) s \<and> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> untypedRange bb \<subseteq> capRange bb
 2. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> \<not> isZombie bb \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {}) \<and> (\<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba bb ys s cap aa bc. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys); (aa, bc) \<in> set ys\<rbrakk> \<Longrightarrow> capRange bb \<inter> capRange bc = {}
 2. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb
 3. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb ys s cap. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ys. capRange (snd x) \<inter> capRange bb = {} \<and> capAligned bb
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb ys s cap aa bc. \<lbrakk>list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps; suffix ((cte_map (a, b), bb) # ys) (zip (map cte_map crefs) cps); cap_relation (default_cap tp ba sz d) bb; cteCaps_of s (cte_map p) = Some cap; isUntypedCap cap; valid_mdb' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_cap' bb s; \<forall>tup\<in>set ys. valid_cap' (snd tup) s; cteCaps_of s (cte_map (a, b)) = Some capability.NullCap; \<forall>tup\<in>set ys. cteCaps_of s (fst tup) = Some capability.NullCap; cte_map p \<noteq> cte_map (a, b); cte_map p \<notin> fst ` set ys; cte_map (a, b) \<notin> fst ` set ys; distinct (map fst ys); global.sameRegionAs cap bb; \<forall>tup\<in>set ys. global.sameRegionAs cap (snd tup); descendants_range' bb (cte_map p) (ctes_of s); \<forall>tup\<in>set ys. descendants_range' (snd tup) (cte_map p) (ctes_of s); caps_overlap_reserved' (capRange bb) s; \<forall>tup\<in>set ys. caps_overlap_reserved' (capRange (snd tup)) s; capRange bb \<inter> (\<Union>x\<in>set ys. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ys); (aa, bc) \<in> set ys\<rbrakk> \<Longrightarrow> capRange bb \<inter> capRange bc = {}
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>x y. fst y = cte_map (fst x) \<and> cap_relation (default_cap tp (snd x) sz d) (snd y)) (zip crefs orefs) (zip (map cte_map crefs) cps) proof (prove)
goal (2 subgoals):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>a b. b = cte_map a) crefs (map cte_map crefs)
 2. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>a. cap_relation (default_cap tp a sz d)) orefs cps proof (prove)
goal (1 subgoal):
 1. list_all2 cap_relation (map (\<lambda>ref. default_cap tp ref sz d) orefs) cps \<Longrightarrow> list_all2 (\<lambda>a. cap_relation (default_cap tp a sz d)) orefs cps proof (prove)
goal:
No subgoals!