theory Retype_DP

lemma invoke_untyped_wp:
  "\<lbrace> K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType
     \<and> length slots = n \<and> free_range \<subseteq> tot_free_range
     \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range)
     and (\<lambda>s. cdl_current_domain s = minBound)
     and < \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots
    \<and>*(\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
    \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range
    \<and>* P > \<rbrace>
  invoke_untyped (Retype uref nt ts slots has_kids n)
  \<lbrace>\<lambda>_ s. (\<exists>nlist free_range'.
  length nlist = n \<and> distinct nlist \<and> set nlist \<subseteq> free_range
  \<and> free_range' \<subseteq> free_range - (set nlist) \<and>
  < \<And>* map (\<lambda>(dest_slot, obj_refs). dest_slot \<mapsto>c (default_cap nt obj_refs ts dev)) (zip slots (map (\<lambda>x. {x}) nlist))
  \<and>* (\<And>* ptr\<in>set nlist. ptr \<mapsto>o obj)
  \<and>* (\<And>* ptr\<in>tot_free_range - set nlist. ptr \<mapsto>o Untyped)
  \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range'
  \<and>* P > s) \<rbrace>, -" apply (simp add: validE_R_def) apply (rule hoare_name_pre_stateE) apply (clarsimp simp:invoke_untyped_def unless_def) apply (rule hoare_pre) apply wp apply (rule hoare_vcg_ex_lift) apply (rule_tac P = "new_obj_refs = map (\<lambda>x. {x}) nlist \<and> untyped_is_device untyped_cap = dev" in hoare_gen_asm) apply (simp add:create_cap_def split_def) apply (wp hoare_vcg_ex_lift) apply (rule cdl.mapM_x_sep') apply (rule hoare_pre, wp set_parent_wp set_cap_wp) apply fastforce apply (rule_tac P = "untyped_cap = UntypedCap dev obj_range free_range
         \<and> length new_obj_refs = length slots
         \<and> distinct (map pick new_obj_refs)
         \<and> pick ` set new_obj_refs \<subseteq> free_range
         \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs" in hoare_gen_asm) apply (wp hoare_vcg_ex_lift) apply (rule_tac P = "x = map pick new_obj_refs" in hoare_gen_asm) apply simp apply (rule_tac
          hoare_strengthen_post[OF retype_region_wp[where obj_range = tot_free_range]]) apply (simp add:map_zip_first_simp) apply (elim conjE) apply (sep_select 3,sep_select 3) apply assumption apply wp+ apply (rule hoare_vcg_conj_lift) apply (rule hoare_vcg_ex_lift) apply (wp hoare_vcg_conj_lift) apply (rule_tac P = "x = map pick new_obj_refs
          \<and> (untyped_cap = UntypedCap dev obj_range free_range)
          \<and>  distinct (map pick new_obj_refs) \<and>
           new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and>
           pick ` set new_obj_refs \<subseteq> tot_free_range" in hoare_gen_asm) apply (simp del:set_map split del:if_split) apply (rule hoare_strengthen_post[OF update_available_range_wp]) apply clarsimp apply (rule_tac x = nfr in exI) apply (rule conjI) apply (clarsimp split:if_splits) apply (sep_select 3,sep_select 2,simp) apply (wp|simp split del:if_split)+ apply (rule_tac P = "untyped_cap = UntypedCap dev obj_range free_range"
       in hoare_gen_asm) apply (clarsimp simp:conj_comms split del: if_split) apply (simp add: conj_assoc[symmetric] del:conj_assoc split del: if_split)+ apply (rule hoare_vcg_conj_lift) apply wp apply (rule hoare_strengthen_post[OF generate_object_ids_rv]) apply (clarsimp simp:Fun.comp_def split:if_splits) apply (drule(1) subset_trans[rotated],fastforce)+ apply (wp reset_untyped_cap_wp unlessE_wp| simp)+ apply (wp hoare_drop_impE_R) apply (erule hoare_post_imp_R[OF reset_untyped_cap_wp
            [where free_range = free_range and obj_range = obj_range]]) apply clarsimp apply (rule conjI) apply sep_solve apply (drule opt_cap_sep_imp) apply (fastforce dest!: reset_cap_asid_simps2) apply (clarsimp split: if_splits) apply (sep_select_asm 3) apply (frule opt_cap_sep_imp, clarsimp dest!: reset_cap_asid_simps2) apply (intro conjI impI) apply sep_cancel+ apply (erule sep_list_conj_impl[rotated]) apply (rule list_all2I) apply (clarsimp simp add: zip_map1 zip_map2 set_zip_same sep_any_map_c_imp)+ apply sep_cancel+ apply (erule sep_list_conj_impl[rotated]) apply (rule list_all2I) apply (clarsimp simp add: zip_map1 zip_map2 set_zip_same sep_any_map_c_imp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length slots = n \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> invoke_untyped (Retype uref nt ts slots has_kids n) \<lbrace>\<lambda>_ s. \<exists>nlist free_range'. length nlist = n \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> free_range' \<subseteq> free_range - set nlist \<and> cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length slots = n \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> invoke_untyped (Retype uref nt ts slots has_kids n) \<lbrace>\<lambda>_ s. \<exists>nlist. length nlist = n \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> length slots = n \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_untyped (Retype uref nt ts slots has_kids n) \<lbrace>\<lambda>_ s. \<exists>nlist. length nlist = n \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (length slots) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip slots new_obj_refs)
od)
odE \<lbrace>\<lambda>_ s. \<exists>nlist. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (length slots) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip slots new_obj_refs)
od)
odE \<lbrace>\<lambda>_ s. \<exists>nlist. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya yb. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s y untyped_cap new_obj_refs ya yb\<rbrace> mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip slots new_obj_refs) \<lbrace>\<lambda>_ s. \<exists>nlist. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>?B23 s y untyped_cap new_obj_refs ya\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya yb nlist. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P25 s y untyped_cap new_obj_refs ya yb nlist\<rbrace> mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip slots new_obj_refs) \<lbrace>\<lambda>rv s. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. ?P25 s y untyped_cap new_obj_refs ya yb x sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya yb nlist. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; new_obj_refs = map (\<lambda>x. {x}) nlist \<and> untyped_is_device untyped_cap = dev\<rbrakk> \<Longrightarrow> \<lbrace>?P'27 s y untyped_cap new_obj_refs ya yb nlist\<rbrace> mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip slots new_obj_refs) \<lbrace>\<lambda>rv s. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map2 (\<lambda>dest_slot obj_refs. dest_slot \<mapsto>c default_cap nt obj_refs ts dev) slots (map (\<lambda>x. {x}) nlist) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. (?P'27 s y untyped_cap new_obj_refs ya yb x and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s untyped_cap yb nlist. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_is_device untyped_cap = dev\<rbrakk> \<Longrightarrow> \<lbrace>?P'27 s () untyped_cap (map (\<lambda>x. {x}) nlist) () yb nlist\<rbrace> mapM_x (\<lambda>p. do old_cap <- get_cap (fst p);
y <- assert (old_cap = NullCap);
y <- set_cap (fst p) (default_cap nt (snd p) ts dev);
set_parent (fst p) uref
od) (zip slots (map (\<lambda>x. {x}) nlist)) \<lbrace>\<lambda>rv s. length nlist = length slots \<and> distinct nlist \<and> set nlist \<subseteq> free_range \<and> (\<exists>free_range'\<subseteq>free_range - set nlist. cdl.lift (\<And>* map (\<lambda>p. fst p \<mapsto>c default_cap nt (snd p) ts dev) (zip slots (map (\<lambda>x. {x}) nlist)) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P) s)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. (?P'27 s y untyped_cap new_obj_refs ya yb x and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s untyped_cap yb nlist free_range'. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_is_device untyped_cap = dev\<rbrakk> \<Longrightarrow> \<lbrace>?P'51 s () untyped_cap (map (\<lambda>x. {x}) nlist) () yb nlist free_range'\<rbrace> mapM_x (\<lambda>p. do old_cap <- get_cap (fst p);
y <- assert (old_cap = NullCap);
y <- set_cap (fst p) (default_cap nt (snd p) ts dev);
set_parent (fst p) uref
od) (zip slots (map (\<lambda>x. {x}) nlist)) \<lbrace>\<lambda>rv. cdl.lift (\<And>* map (\<lambda>p. fst p \<mapsto>c default_cap nt (snd p) ts dev) (zip slots (map (\<lambda>x. {x}) nlist)) \<and>* (SETSEPCONJ ptr:set nlist. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set nlist. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range' \<and>* P)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. ((\<lambda>a. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. ?P'51 s y untyped_cap new_obj_refs ya yb x xa a)) and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s untyped_cap yb nlist free_range' R x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_is_device untyped_cap = dev; x \<in> set (zip slots (map (\<lambda>x. {x}) nlist))\<rbrakk> \<Longrightarrow> \<lbrace>cdl.lift (?P65 s () untyped_cap (map (\<lambda>x. {x}) nlist) () yb nlist free_range' x \<and>* R)\<rbrace> do old_cap <- get_cap (fst x);
y <- assert (old_cap = NullCap);
y <- set_cap (fst x) (default_cap nt (snd x) ts dev);
set_parent (fst x) uref
od \<lbrace>\<lambda>rv. cdl.lift (fst x \<mapsto>c default_cap nt (snd x) ts dev \<and>* R)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. ((\<lambda>a. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. cdl.lift (\<And>* map (?P65 s y untyped_cap new_obj_refs ya yb x xa) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) a)) and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s untyped_cap yb nlist free_range' R x sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_is_device untyped_cap = dev; x \<in> set (zip slots (map (\<lambda>x. {x}) nlist)); cdl.lift (?P65 s () untyped_cap (map (\<lambda>x. {x}) nlist) () yb nlist free_range' x \<and>* R) sa\<rbrakk> \<Longrightarrow> opt_cap (fst x) sa \<noteq> None \<longrightarrow> the (opt_cap (fst x) sa) = NullCap \<longrightarrow> cdl.lift ((fst x) \<mapsto>c - \<and>* R) sa
 2. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb sa. \<exists>x. ((\<lambda>a. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. cdl.lift (\<And>* map (?P65 s y untyped_cap new_obj_refs ya yb x xa) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) a)) and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) sa\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb s. \<exists>x. ((\<lambda>a. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) a)) and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B22 s y untyped_cap new_obj_refs\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'98 s y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb s. \<exists>x. ((\<lambda>a. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) a)) and K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. ?P'98 s y untyped_cap new_obj_refs ya and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya x xa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'113 s y untyped_cap new_obj_refs ya x xa\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. ?P'113 s y untyped_cap new_obj_refs ya x xa sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya x xa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; x = map pick new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'116 s y untyped_cap new_obj_refs ya x xa\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:set x. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - set x. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (?P'116 s y untyped_cap new_obj_refs ya x xa and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs x xa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; x = map pick new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'116 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (?P'116 s y untyped_cap new_obj_refs ya x xa and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs x xa rv sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; x = map pick new_obj_refs; cdl.lift ((SETSEPCONJ ptr:set (map pick new_obj_refs). ptr \<mapsto>o ?obj131 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) \<and>* (SETSEPCONJ ptr:tot_free_range - set (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* ?P129 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (\<lambda>a. (fst a) \<mapsto>c -) (zip slots new_obj_refs) \<and>* (SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some (?obj131 s y untyped_cap new_obj_refs ya x xa) \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P129 s y untyped_cap new_obj_refs ya x xa) and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs x xa sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; x = map pick new_obj_refs; cdl.lift ((SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o ?obj131 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* ?P129 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_c slots \<and>* (SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some (?obj131 s y untyped_cap new_obj_refs ya x xa) \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P129 s y untyped_cap new_obj_refs ya x xa) and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs x xa sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; x = map pick new_obj_refs; cdl.lift ((SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o ?obj131 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* ?P129 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) sa; length new_obj_refs = length slots; distinct (map pick new_obj_refs); pick ` set new_obj_refs \<subseteq> free_range; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_c slots \<and>* (SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some (?obj131 s y untyped_cap new_obj_refs ya x xa) \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P129 s y untyped_cap new_obj_refs ya x xa) and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs x xa sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; x = map pick new_obj_refs; cdl.lift ((SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o ?obj131 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* ?P129 s () (UntypedCap dev obj_range free_range) new_obj_refs () (map pick new_obj_refs) xa) sa; length new_obj_refs = length slots; distinct (map pick new_obj_refs); pick ` set new_obj_refs \<subseteq> free_range; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set new_obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:tot_free_range - pick ` set new_obj_refs. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some (?obj131 s y untyped_cap new_obj_refs ya x xa) \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P129 s y untyped_cap new_obj_refs ya x xa) and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs ya x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'111 s y untyped_cap new_obj_refs ya x\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya. (\<lambda>sa. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) sa) \<and> ?P'111 s y untyped_cap new_obj_refs ya x sa) and K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>ya s. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) s) \<and> K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev) s) \<and> K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs) s\<rbrace>
 2. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>?B21 s y untyped_cap\<rbrace>
 3. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 4. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv s. \<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) s) \<and> K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. ?P153 s y untyped_cap new_obj_refs sa \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P156 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv s. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (\<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) s) \<and> K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. ?P156 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv s. \<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ?P165 s y untyped_cap new_obj_refs x sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range\<rbrakk> \<Longrightarrow> \<lbrace>?P'167 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv s. \<exists>xa\<subseteq>free_range - set x. (K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> distinct x \<and> new_obj_refs = map (\<lambda>x. {x}) x \<and> set x \<subseteq> tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range xa \<and>* P) and K (x = map pick new_obj_refs)) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (?P'167 s y untyped_cap new_obj_refs x and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range\<rbrakk> \<Longrightarrow> \<lbrace>?P'167 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)\<rbrace> update_available_range free_range (map pick new_obj_refs) uref (UntypedCap dev obj_range free_range) \<lbrace>\<lambda>rv s. \<exists>x\<subseteq>free_range - set (map pick new_obj_refs). set (map pick new_obj_refs) \<subseteq> tot_free_range \<and> cdl_current_domain s = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range x \<and>* P) s\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> (?P'167 s y untyped_cap new_obj_refs x and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs rv sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range; cdl_current_domain sa = minBound \<and> (\<exists>nfr\<subseteq>free_range - set (map pick new_obj_refs). cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa)\<rbrakk> \<Longrightarrow> \<exists>x\<subseteq>free_range - set (map pick new_obj_refs). set (map pick new_obj_refs) \<subseteq> tot_free_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range x \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:?tot_free_range179 s y untyped_cap new_obj_refs x. ptr \<mapsto>o Untyped) \<and>* ?P178 s y untyped_cap new_obj_refs x) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs sa nfr. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs); cdl_current_domain sa = minBound; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; pick ` set new_obj_refs \<subseteq> tot_free_range; nfr \<subseteq> free_range - pick ` set new_obj_refs; cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa\<rbrakk> \<Longrightarrow> \<exists>x\<subseteq>free_range - pick ` set new_obj_refs. cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range x \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:?tot_free_range179 s y untyped_cap new_obj_refs x. ptr \<mapsto>o Untyped) \<and>* ?P178 s y untyped_cap new_obj_refs x) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs sa nfr. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs); cdl_current_domain sa = minBound; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; pick ` set new_obj_refs \<subseteq> tot_free_range; nfr \<subseteq> free_range - pick ` set new_obj_refs; cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa\<rbrakk> \<Longrightarrow> nfr \<subseteq> free_range - pick ` set new_obj_refs \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:?tot_free_range179 s y untyped_cap new_obj_refs x. ptr \<mapsto>o Untyped) \<and>* ?P178 s y untyped_cap new_obj_refs x) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (8 subgoals):
 1. \<And>s new_obj_refs sa nfr. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs); cdl_current_domain sa = minBound; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; pick ` set new_obj_refs \<subseteq> tot_free_range; nfr \<subseteq> free_range - pick ` set new_obj_refs; cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa\<rbrakk> \<Longrightarrow> nfr \<subseteq> free_range - pick ` set new_obj_refs
 2. \<And>s new_obj_refs sa nfr. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs); cdl_current_domain sa = minBound; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; pick ` set new_obj_refs \<subseteq> tot_free_range; nfr \<subseteq> free_range - pick ` set new_obj_refs; cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) sa
 3. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 4. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 5. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:?tot_free_range179 s y untyped_cap new_obj_refs x. ptr \<mapsto>o Untyped) \<and>* ?P178 s y untyped_cap new_obj_refs x) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 6. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 7. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (7 subgoals):
 1. \<And>s new_obj_refs sa nfr. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; distinct (map pick new_obj_refs); cdl_current_domain sa = minBound; new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs; pick ` set new_obj_refs \<subseteq> tot_free_range; nfr \<subseteq> free_range - pick ` set new_obj_refs; cdl.lift ((SETSEPCONJ ptr:?tot_free_range179 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs). ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* ?P178 s () (UntypedCap dev obj_range free_range) new_obj_refs (map pick new_obj_refs)) sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* uref \<mapsto>c UntypedCap dev obj_range nfr \<and>* P) sa
 2. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 3. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 4. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:?tot_free_range179 s y untyped_cap new_obj_refs x. ptr \<mapsto>o Untyped) \<and>* ?P178 s y untyped_cap new_obj_refs x) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 5. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 6. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s y untyped_cap new_obj_refs x. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'165 s y untyped_cap new_obj_refs x\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (new_obj_refs = map (\<lambda>x. {x}) x \<and> untyped_is_device untyped_cap = dev)\<rbrace>
 2. \<And>s y untyped_cap new_obj_refs. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'153 s y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>\<lambda>rv. K (untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs)\<rbrace>
 3. \<And>s y untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s y untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs sa. (\<exists>x. length x = length slots \<and> distinct x \<and> set x \<subseteq> free_range \<and> ((\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) and K (x = map pick new_obj_refs \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range)) sa \<and> ?P'165 s y untyped_cap new_obj_refs x sa) \<and> ?P'153 s y untyped_cap new_obj_refs sa\<rbrace>
 4. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 5. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s () untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs s. length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> cdl_current_domain s = minBound \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> untyped_is_device untyped_cap = dev \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrace>
 2. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>?B20 s y\<rbrace>
 3. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s untyped_cap. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; untyped_cap = UntypedCap dev obj_range free_range\<rbrakk> \<Longrightarrow> \<lbrace>?P'206 s () untyped_cap\<rbrace> generate_object_ids (length slots) nt (available_range untyped_cap) \<lbrace>\<lambda>new_obj_refs s. length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> cdl_current_domain s = minBound \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> distinct (map pick new_obj_refs) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> pick ` set new_obj_refs \<subseteq> tot_free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> untyped_is_device untyped_cap = dev \<and> untyped_cap = UntypedCap dev obj_range free_range \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs\<rbrace>
 2. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. ?P'206 s y a and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 3. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'206 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>new_obj_refs s. cdl_current_domain s = minBound \<and> length new_obj_refs = length slots \<and> distinct (map pick new_obj_refs) \<and> pick ` set new_obj_refs \<subseteq> free_range \<and> pick ` set new_obj_refs \<subseteq> tot_free_range \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s\<rbrace>
 2. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. ?P'206 s y a and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 3. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'206 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>new_obj_refs s. (((((cdl_current_domain s = minBound \<and> length new_obj_refs = length slots) \<and> distinct (map pick new_obj_refs)) \<and> pick ` set new_obj_refs \<subseteq> free_range) \<and> pick ` set new_obj_refs \<subseteq> tot_free_range) \<and> new_obj_refs = map ((\<lambda>x. {x}) \<circ> pick) new_obj_refs) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s\<rbrace>
 2. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. ?P'206 s y a and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 3. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P212 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv s. ((((cdl_current_domain s = minBound \<and> length rv = length slots) \<and> distinct (map pick rv)) \<and> pick ` set rv \<subseteq> free_range) \<and> pick ` set rv \<subseteq> tot_free_range) \<and> rv = map ((\<lambda>x. {x}) \<circ> pick) rv\<rbrace>
 2. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'211 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P)\<rbrace>
 3. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. (\<lambda>b. ?P212 s y a b \<and> ?P'211 s y a b) and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 4. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'221 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv s. length rv = length slots \<and> distinct (map pick rv) \<and> pick ` set rv \<subseteq> free_range \<and> pick ` set rv \<subseteq> tot_free_range \<and> rv = map ((\<lambda>x. {x}) \<circ> pick) rv\<rbrace>
 2. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'211 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P)\<rbrace>
 3. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. (\<lambda>b. (cdl_current_domain b = minBound \<and> ?P'221 s y a b) \<and> ?P'211 s y a b) and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 4. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s rv sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; rv = map (\<lambda>x. {x}) (map pick rv) \<and> length rv = length slots \<and> set (map pick rv) \<subseteq> free_range \<and> distinct (map pick rv)\<rbrakk> \<Longrightarrow> length rv = length slots \<and> distinct (map pick rv) \<and> pick ` set rv \<subseteq> free_range \<and> pick ` set rv \<subseteq> tot_free_range \<and> rv = map ((\<lambda>x. {x}) \<circ> pick) rv
 2. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'211 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P)\<rbrace>
 3. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. (\<lambda>b. (cdl_current_domain b = minBound \<and> K (nt \<noteq> UntypedType) b) \<and> ?P'211 s y a b) and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 4. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s rv a. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; a \<in> set rv; rv = map (\<lambda>x. {pick x}) rv; length rv = length slots; pick ` set rv \<subseteq> free_range; distinct (map pick rv)\<rbrakk> \<Longrightarrow> pick a \<in> tot_free_range
 2. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'211 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P)\<rbrace>
 3. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. (\<lambda>b. (cdl_current_domain b = minBound \<and> K (nt \<noteq> UntypedType) b) \<and> ?P'211 s y a b) and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 4. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'211 s () (UntypedCap dev obj_range free_range)\<rbrace> generate_object_ids (length slots) nt free_range \<lbrace>\<lambda>rv. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P)\<rbrace>
 2. \<And>s y. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B17 s y\<rbrace> get_cap uref \<lbrace>\<lambda>a. (\<lambda>b. (cdl_current_domain b = minBound \<and> K (nt \<noteq> UntypedType) b) \<and> ?P'211 s y a b) and K (a = UntypedCap dev obj_range free_range)\<rbrace>
 3. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 s\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B17 s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids\<rbrakk> \<Longrightarrow> \<lbrace>?P'268 s\<rbrace> reset_untyped_cap uref \<lbrace>\<lambda>y s. (\<exists>y. opt_cap uref s = Some y) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s \<and> the (opt_cap uref s) = UntypedCap dev obj_range obj_range\<rbrace>, -
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> ?P'268 s sa)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids\<rbrakk> \<Longrightarrow> \<lbrace>?P'277 s\<rbrace> reset_untyped_cap uref \<lbrace>\<lambda>rv s. cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) s \<and> the (opt_cap uref s) = UntypedCap dev obj_range obj_range\<rbrace>, -
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> ?P'277 s sa)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; \<exists>fr. free_range \<subseteq> fr \<and> fr \<subseteq> obj_range \<and> cdl.lift (uref \<mapsto>c UntypedCap (?dev281 s) obj_range fr \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P281 s) sa\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa \<and> the (opt_cap uref sa) = UntypedCap dev obj_range obj_range
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap (?dev281 s) obj_range free_range \<and>* ?P281 s) sa)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev free_range free_range \<and>* P) s; \<not> has_kids; obj_range = free_range; cdl.lift (uref \<mapsto>c UntypedCap (?dev281 s) free_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P281 s) sa\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa \<and> the (opt_cap uref sa) = UntypedCap dev free_range free_range
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap (?dev281 s) obj_range free_range \<and>* ?P281 s) sa)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev free_range free_range \<and>* P) s; \<not> has_kids; obj_range = free_range; cdl.lift (uref \<mapsto>c UntypedCap (?dev281 s) free_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P281 s) sa\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev free_range free_range \<and>* P) s; \<not> has_kids; obj_range = free_range; cdl.lift (uref \<mapsto>c UntypedCap (?dev281 s) free_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* ?P281 s) sa\<rbrakk> \<Longrightarrow> the (opt_cap uref sa) = UntypedCap dev free_range free_range
 3. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap (?dev281 s) obj_range free_range \<and>* ?P281 s) sa)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev free_range free_range \<and>* P) s; \<not> has_kids; obj_range = free_range; cdl.lift (uref \<mapsto>c UntypedCap (?dev281 s) free_range free_range \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa\<rbrakk> \<Longrightarrow> the (opt_cap uref sa) = UntypedCap dev free_range free_range
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap (?dev281 s) obj_range free_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev free_range free_range \<and>* P) s; \<not> has_kids; obj_range = free_range; \<exists>cap'. opt_cap uref sa = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (UntypedCap (?dev281 s) free_range free_range)\<rbrakk> \<Longrightarrow> the (opt_cap uref sa) = UntypedCap dev free_range free_range
 2. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>sa. True \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap (?dev281 s) obj_range free_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> True \<and> (if has_kids then \<lambda>s. opt_cap uref s \<noteq> None \<longrightarrow> ((\<lambda>a. (cdl_current_domain a = minBound \<and> K (nt \<noteq> UntypedType) a) \<and> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) a) and K (the (opt_cap uref s) = UntypedCap dev obj_range free_range)) s else (\<lambda>s. True \<and> cdl_current_domain s = minBound \<and> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) s)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) sa\<rbrakk> \<Longrightarrow> (has_kids \<longrightarrow> (\<exists>y. opt_cap uref sa = Some y) \<longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa \<and> the (opt_cap uref sa) = UntypedCap dev obj_range free_range) \<and> (\<not> has_kids \<longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa\<rbrakk> \<Longrightarrow> (has_kids \<longrightarrow> (\<exists>y. opt_cap uref sa = Some y) \<longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa \<and> the (opt_cap uref sa) = UntypedCap dev obj_range free_range) \<and> (\<not> has_kids \<longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> (has_kids \<longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa) \<and> (\<not> has_kids \<longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); has_kids\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c - \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa
 2. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); \<not> has_kids\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); has_kids; (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) sc\<rbrakk> \<Longrightarrow> (\<And>* map sep_any_map_c slots) sc
 2. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); \<not> has_kids\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); has_kids\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) (map sep_any_map_c slots)
 2. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); \<not> has_kids\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); has_kids\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (zip (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) (map sep_any_map_c slots)). case x of (x, y) \<Rightarrow> \<forall>s. x s \<longrightarrow> y s
 2. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); has_kids\<rbrakk> \<Longrightarrow> length (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) = length (map sep_any_map_c slots)
 3. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range free_range); \<not> has_kids\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain sa = minBound; cdl.lift (uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* P) sa; opt_cap uref sa = Some (UntypedCap dev obj_range obj_range); \<not> has_kids\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* \<And>* map sep_any_map_c slots \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range obj_range); \<not> has_kids; (\<And>* map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) sc\<rbrakk> \<Longrightarrow> (\<And>* map sep_any_map_c slots) sc proof (prove)
goal (1 subgoal):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range obj_range); \<not> has_kids\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) (map sep_any_map_c slots) proof (prove)
goal (2 subgoals):
 1. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range obj_range); \<not> has_kids\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (zip (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) (map sep_any_map_c slots)). case x of (x, y) \<Rightarrow> \<forall>s. x s \<longrightarrow> y s
 2. \<And>sa s sb sc. \<lbrakk>default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; n = length slots; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain sa = minBound; opt_cap uref sa = Some (UntypedCap dev obj_range obj_range); \<not> has_kids\<rbrakk> \<Longrightarrow> length (map (\<lambda>dest_slot. dest_slot \<mapsto>c NullCap) slots) = length (map sep_any_map_c slots) proof (prove)
goal:
No subgoals!