theory Retype_R

lemma retype_state_relation:
  notes data_map_insert_def[simp del]
  assumes  sr:   "(s, s') \<in> state_relation"
      and  vs:   "valid_pspace s" "valid_mdb s"
      and  et:   "valid_etcbs s" "valid_list s"
      and vs':   "pspace_aligned' s'" "pspace_distinct' s'"
      and  pn:   "pspace_no_overlap_range_cover ptr sz s"
      and pn':   "pspace_no_overlap' ptr sz s'"
      and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n"
      and  ko:   "makeObjectKO dev ty = Some ko"
      and api:   "obj_bits_api (APIType_map2 ty) us \<le> sz"
      and orr:   "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko"
      and num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n"
  shows
  "(ekheap_update
              (\<lambda>_. foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a)
                    (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s))
            s
           \<lparr>kheap :=
              foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us))
               (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>,
           update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us))
            (s'\<lparr>ksPSpace :=
                  foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko)
                   (ksPSpace s')\<rparr>))
          \<in> state_relation"
  (is "(ekheap_update (\<lambda>_. ?eps) s\<lparr>kheap := ?ps\<rparr>, update_gs _ _ _ (s'\<lparr>ksPSpace := ?ps'\<rparr>))
       \<in> state_relation") proof (rule state_relation_null_filterE[OF sr refl _ _ _ _ _ _ _ vs'], simp_all add: trans_state_update[symmetric] del: trans_state_update) have cover':"range_cover ptr sz (objBitsKO ko) m" by (rule range_cover_rel[OF cover objBits_le_obj_bits_api[OF ko] num_r]) have al':"is_aligned ptr (objBitsKO ko)" using cover' by (simp add:range_cover_def) have sz:"sz < word_bits" using cover' by (simp add:range_cover_def word_bits_def) let ?t = "s\<lparr>kheap := ?ps\<rparr>" let ?tp = "APIType_map2 ty" let ?al = "retype_addrs ptr ?tp n us" let ?t' = "update_gs ?tp us (set ?al) (s'\<lparr>ksPSpace := ?ps'\<rparr>)" note pad' = retype_aligned_distinct' [OF vs' pn' cover'] thus pa': "pspace_aligned' (s'\<lparr>ksPSpace := ?ps'\<rparr>)"
   and pd': "pspace_distinct' (s'\<lparr>ksPSpace := ?ps'\<rparr>)" by simp_all note pa'' = pa'[simplified foldr_upd_app_if[folded data_map_insert_def]] note pd'' = pd'[simplified foldr_upd_app_if[folded data_map_insert_def]] note not_unt = makeObjectKO_Untyped [OF ko] show "null_filter (caps_of_state ?t) = null_filter (caps_of_state s)" apply (rule null_filter_caps_of_state_foldr[folded data_map_insert_def]) apply (simp add: not_unt) apply (rule ballI) apply (erule pspace_no_overlapD2 [OF pn _ cover vs(1)]) done have nc_dis: "distinct (new_cap_addrs m ptr ko)" by (rule new_cap_addrs_distinct [OF cover']) note nc_al = bspec [OF new_cap_addrs_aligned [OF al']] note nc_al' = nc_al[unfolded objBits_def] show "null_filter' (map_to_ctes ?ps') = null_filter' (ctes_of s')" apply (rule null_filter_ctes_retype [OF ko vs' pa'' pd'']) apply (simp add: nc_al) apply clarsimp apply (drule subsetD [OF new_cap_addrs_subset [OF cover']]) apply (insert pspace_no_overlap_disjoint'[OF vs'(1) pn']) apply (drule orthD1) apply (simp add:ptr_add_def field_simps) apply clarsimp done show "valid_objs s" using vs by (clarsimp simp: valid_pspace_def) show "valid_mdb s" using vs by (clarsimp) show "valid_list s" using et by (clarsimp) show "mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)" using vs by (clarsimp simp: valid_mdb_def) have pspr: "pspace_relation (kheap s) (ksPSpace s')" using sr by (simp add: state_relation_def) thus "pspace_relation ?ps ?ps'" by (rule retype_pspace_relation [OF _ vs vs' pn pn' ko cover orr num_r,
        folded data_map_insert_def]) have "ekheap_relation (ekheap (s)) (ksPSpace s')" using sr by (simp add: state_relation_def) thus "ekheap_relation ?eps ?ps'" by (fold fun_upd_apply) (rule retype_ekheap_relation[OF _ pspr vs et(1) vs' pn pn' ko cover orr num_r]) have pn2: "\<forall>a\<in>set ?al. kheap s a = None" by (rule ccontr) (clarsimp simp: pspace_no_overlapD1[OF pn _ cover vs(1)]) from sr have gr: "ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')" by (rule state_relationE) show "ghost_relation ?ps (gsUserPages ?t') (gsCNodes ?t')" proof (cases ?tp) case Untyped thus ?thesis by (simp add: not_unt) next note data_map_insert_def[simp] case TCBObject from pn2 have [simp]: "ups_of_heap ?ps = ups_of_heap (kheap s)" by - (rule ext, induct (?al),
            simp_all add: ups_of_heap_def default_object_def TCBObject) from pn2 have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al),
            simp_all add: cns_of_heap_def default_object_def TCBObject) note data_map_insert_def[simp del] from gr show ?thesis by (simp add: ghost_relation_of_heap, simp add: TCBObject update_gs_def) next case EndpointObject from pn2 have [simp]: "ups_of_heap ?ps = ups_of_heap (kheap s)" by - (rule ext, induct (?al),
            simp_all add: ups_of_heap_def default_object_def data_map_insert_def EndpointObject) from pn2 have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al),
            simp_all add: cns_of_heap_def default_object_def data_map_insert_def EndpointObject) from gr show ?thesis by (simp add: ghost_relation_of_heap,
          simp add: EndpointObject update_gs_def) next note data_map_insert_def[simp] case NotificationObject from pn2 have [simp]: "ups_of_heap ?ps = ups_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: ups_of_heap_def
                                      default_object_def NotificationObject) from pn2 have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: cns_of_heap_def
                                      default_object_def NotificationObject) note data_map_insert_def[simp del] from gr show ?thesis by (simp add: ghost_relation_of_heap,
          simp add: NotificationObject update_gs_def) next case CapTableObject note data_map_insert_def[simp] from pn2 have [simp]: "ups_of_heap ?ps = ups_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: ups_of_heap_def
                                      default_object_def CapTableObject) have [simp]: "cns_of_heap ?ps = (\<lambda>x. if x \<in> set ?al then Some us
                                         else cns_of_heap (kheap s) x)" by (rule ext, induct (?al),
          simp_all add: cns_of_heap_def wf_empty_bits wf_unique default_object_def CapTableObject) note data_map_insert_def[simp del] from gr show ?thesis by (simp add: ghost_relation_of_heap,
          simp add: CapTableObject update_gs_def ext) next case (ArchObject ao) from pn2 have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)" by - (rule ext, induct (?al), simp_all add: cns_of_heap_def data_map_insert_def
                                      default_object_def ArchObject) from pn2 gr show ?thesis apply (clarsimp simp add: ghost_relation_of_heap) apply (rule conjI[rotated]) apply (simp add: ArchObject update_gs_def split: aobject_type.splits) apply (thin_tac "cns_of_heap h = g" for h g) apply (drule sym) apply (rule ext) apply (induct (?al)) apply (simp add: update_gs_def ArchObject split: aobject_type.splits) apply (simp add: update_gs_def ArchObject default_object_def
                       default_arch_object_def ups_of_heap_def
                       data_map_insert_def
                split: aobject_type.splits) done qed show "\<exists>f' g' h'. ?t' =
          s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'),
             gsCNodes := h' (gsCNodes s')\<rparr>" apply (clarsimp simp: update_gs_def
                   split: Structures_A.apiobject_type.splits) apply (intro conjI impI) apply (subst ex_comm, rule_tac x=id in exI,
                subst ex_comm, rule_tac x=id in exI, fastforce)+ apply (subst ex_comm, rule_tac x=id in exI) apply (subst ex_comm) apply (rule_tac x="\<lambda>cns x. if x\<in>set ?al then Some us else cns x" in exI,
            simp) apply (rule_tac x="\<lambda>x. foldr (\<lambda>addr. data_map_insert addr ko)
                                  (new_cap_addrs m ptr ko) x" in exI, simp) apply clarsimp apply (rule_tac x="\<lambda>x. foldr (\<lambda>addr. data_map_insert addr ko)
                                 (new_cap_addrs m ptr ko) x" in exI) apply (subst ex_comm, rule_tac x=id in exI) apply (simp split: aobject_type.splits) apply (intro conjI impI) apply (rule_tac x="\<lambda>cns x. if x \<in> set ?al then Some ARMSmallPage
                                     else cns x" in exI, simp) apply (rule_tac x="\<lambda>cns x. if x \<in> set ?al then Some ARMLargePage
                                    else cns x" in exI, simp) apply (rule_tac x="\<lambda>cns x. if x \<in> set ?al then Some ARMSection
                                   else cns x" in exI, simp) apply (rule_tac x="\<lambda>cns x. if x \<in> set ?al then Some ARMSuperSection
                                  else cns x" in exI, simp) apply (rule_tac x=id in exI, simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s\<lparr>ekheap := foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s), kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>, update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) \<in> state_relation proof (state)
goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO ko) m proof (state)
this:
range_cover ptr sz (objBitsKO ko) m

goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) proof (prove)
using this:
range_cover ptr sz (objBitsKO ko) m

goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) proof (state)
this:
is_aligned ptr (objBitsKO ko)

goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. sz < word_bits proof (prove)
using this:
range_cover ptr sz (objBitsKO ko) m

goal (1 subgoal):
 1. sz < word_bits proof (state)
this:
sz < word_bits

goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (state)
this:
pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)

goal (12 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
A total of 12 subgoals... proof (prove)
using this:
pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)

goal (1 subgoal):
 1. pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) &&& pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) proof (state)
this:
pspace_aligned' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)
pspace_distinct' (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)

goal (10 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
pspace_aligned' (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs m ptr ko) then Some ko else ksPSpace s' x\<rparr>)

goal (10 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
pspace_distinct' (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs m ptr ko) then Some ko else ksPSpace s' x\<rparr>)

goal (10 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)

goal (10 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)
 3. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 4. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 6. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 7. valid_list s
 8. valid_objs s
 9. valid_mdb s
 10. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s) proof (prove)
goal (2 subgoals):
 1. APIType_map2 ty \<noteq> Structures_A.apiobject_type.Untyped
 2. \<forall>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<Longrightarrow> x \<notin> dom (kheap s) proof (prove)
goal:
No subgoals! proof (state)
this:
null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\<rparr>)) = null_filter (caps_of_state s)

goal (9 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 3. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. valid_list s
 7. valid_objs s
 8. valid_mdb s
 9. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. distinct (new_cap_addrs m ptr ko) proof (state)
this:
distinct (new_cap_addrs m ptr ko)

goal (9 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 3. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. valid_list s
 7. valid_objs s
 8. valid_mdb s
 9. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
?x \<in> set (new_cap_addrs ?n1 ptr ko) \<Longrightarrow> is_aligned ?x (objBitsKO ko)

goal (9 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 3. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. valid_list s
 7. valid_objs s
 8. valid_mdb s
 9. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
?x \<in> set (new_cap_addrs ?n1 ptr ko) \<Longrightarrow> is_aligned ?x (objBitsKO ko)

goal (9 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')
 3. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 5. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. valid_list s
 7. valid_objs s
 8. valid_mdb s
 9. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s') proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set (new_cap_addrs m ptr ko). is_aligned x (objBitsKO ko)
 2. \<forall>x\<in>set (new_cap_addrs m ptr ko). ksPSpace s' x = None proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (new_cap_addrs m ptr ko). ksPSpace s' x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (new_cap_addrs m ptr ko) \<Longrightarrow> ksPSpace s' x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<Longrightarrow> ksPSpace s' x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s') = {}\<rbrakk> \<Longrightarrow> ksPSpace s' x = None proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<Longrightarrow> ?x13 x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; ?x13 x \<notin> dom (ksPSpace s')\<rbrakk> \<Longrightarrow> ksPSpace s' x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; x \<notin> dom (ksPSpace s')\<rbrakk> \<Longrightarrow> ksPSpace s' x = None proof (prove)
goal:
No subgoals! proof (state)
this:
null_filter' (map_to_ctes (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))) = null_filter' (ctes_of s')

goal (8 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. valid_list s
 6. valid_objs s
 7. valid_mdb s
 8. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. valid_objs s proof (prove)
using this:
valid_pspace s
valid_mdb s

goal (1 subgoal):
 1. valid_objs s proof (state)
this:
valid_objs s

goal (7 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. valid_list s
 6. valid_mdb s
 7. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. valid_mdb s proof (prove)
using this:
valid_pspace s
valid_mdb s

goal (1 subgoal):
 1. valid_mdb s proof (state)
this:
valid_mdb s

goal (6 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. valid_list s
 6. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. valid_list s proof (prove)
using this:
valid_etcbs s
valid_list s

goal (1 subgoal):
 1. valid_list s proof (state)
this:
valid_list s

goal (5 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (prove)
using this:
valid_pspace s
valid_mdb s

goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) proof (state)
this:
mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)

goal (4 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') proof (state)
this:
pspace_relation (kheap s) (ksPSpace s')

goal (4 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 4. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (state)
this:
pspace_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))

goal (3 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. ekheap_relation (ekheap s) (ksPSpace s') proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. ekheap_relation (ekheap s) (ksPSpace s') proof (state)
this:
ekheap_relation (ekheap s) (ksPSpace s')

goal (3 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 3. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
using this:
ekheap_relation (ekheap s) (ksPSpace s')

goal (1 subgoal):
 1. ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (state)
this:
ekheap_relation (foldr (\<lambda>p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))

goal (2 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (state)
this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (2 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
(s, s') \<in> state_relation proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (state)
this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (2 subgoals):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (6 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.Untyped \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = Structures_A.apiobject_type.Untyped

goal (6 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.Untyped \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 6. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
using this:
APIType_map2 ty = Structures_A.apiobject_type.Untyped

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = Structures_A.apiobject_type.TCBObject

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s) proof (state)
this:
ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s)

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s) proof (state)
this:
cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s)

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (5 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 5. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (prove)
using this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (4 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (4 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = Structures_A.apiobject_type.EndpointObject

goal (4 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s) proof (state)
this:
ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s)

goal (4 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s) proof (state)
this:
cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s)

goal (4 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 4. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (prove)
using this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = Structures_A.apiobject_type.NotificationObject

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s) proof (state)
this:
ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s)

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s) proof (state)
this:
cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s)

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (3 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 3. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (prove)
using this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = Structures_A.apiobject_type.CapTableObject

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s) proof (state)
this:
ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = ups_of_heap (kheap s)

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some us else cns_of_heap (kheap s) x) proof (state)
this:
cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some us else cns_of_heap (kheap s) x)

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
data_map_insert ?x ?y ?m \<equiv> ?m(?x \<mapsto> ?y)

goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))
 2. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (prove)
using this:
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (state)
this:
APIType_map2 ty = ArchObject ao

goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None

goal (1 subgoal):
 1. cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s) proof (state)
this:
cns_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = cns_of_heap (kheap s)

goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (chain)
picking this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') proof (prove)
using this:
\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')

goal (1 subgoal):
 1. ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; ups_of_heap (kheap s) = gsUserPages s'; cns_of_heap (kheap s) = gsCNodes s'\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) \<and> gsCNodes s' = gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; ups_of_heap (kheap s) = gsUserPages s'; cns_of_heap (kheap s) = gsCNodes s'\<rbrakk> \<Longrightarrow> gsCNodes s' = gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))
 2. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; ups_of_heap (kheap s) = gsUserPages s'; cns_of_heap (kheap s) = gsCNodes s'\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; ups_of_heap (kheap s) = gsUserPages s'; cns_of_heap (kheap s) = gsCNodes s'\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; ups_of_heap (kheap s) = gsUserPages s'\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>a\<in>set (retype_addrs ptr (APIType_map2 ty) n us). kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a\<in>set []. kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) [] (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set []) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x
 2. \<And>a list x. \<lbrakk>\<And>x. \<lbrakk>\<forall>a\<in>set list. kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) list (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set list) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x; \<forall>a\<in>set (a # list). kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (a # list) (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set (a # list)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>a list x. \<lbrakk>\<And>x. \<lbrakk>\<forall>a\<in>set list. kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) list (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set list) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x; \<forall>a\<in>set (a # list). kheap s a = None; gsUserPages s' = ups_of_heap (kheap s)\<rbrakk> \<Longrightarrow> ups_of_heap (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (a # list) (kheap s)) x = gsUserPages (update_gs (APIType_map2 ty) us (set (a # list)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)) x proof (prove)
goal:
No subgoals! proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal:
No subgoals! proof (state)
this:
ghost_relation (foldr (\<lambda>p. data_map_insert p (default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (gsUserPages (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>))) (gsCNodes (update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>)))

goal (1 subgoal):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr> proof (prove)
goal (1 subgoal):
 1. (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) \<longrightarrow> (\<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) \<and> (APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<longrightarrow> (\<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) \<and> (APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<longrightarrow> (\<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) \<and> (APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<longrightarrow> (\<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) \<and> (APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<longrightarrow> (\<exists>f' g' h'. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) \<and> (\<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>)) proof (prove)
goal (6 subgoals):
 1. ty = Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) \<Longrightarrow> \<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. APIType_map2 ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> \<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 3. APIType_map2 ty = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> \<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 4. APIType_map2 ty = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> \<exists>f' g' h'. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 5. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> \<exists>f' g' h'. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 6. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> \<exists>f' g' h'. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> \<exists>x h'. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := x (ksPSpace s'), gsUserPages := id (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>
 2. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> \<exists>y x. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := x (ksPSpace s'), gsUserPages := id (gsUserPages s'), gsCNodes := y (gsCNodes s')\<rparr>
 2. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (2 subgoals):
 1. APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> \<exists>x. gsCNodes_update (\<lambda>cns x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else cns x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := x (ksPSpace s'), gsCNodes := \<lambda>x. if x \<in> set (retype_addrs ptr Structures_A.apiobject_type.CapTableObject n us) then Some us else gsCNodes s' x\<rparr>
 2. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<forall>x6. APIType_map2 ty = ArchObject x6 \<longrightarrow> (\<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> \<exists>f' g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> \<exists>g' h'. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> \<exists>x. (case x6 of SmallPageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSmallPage else ups x) | LargePageObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMLargePage else ups x) | SectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSection else ups x) | SuperSectionObj \<Rightarrow> gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some ARMSuperSection else ups x) | _ \<Rightarrow> id) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s'), gsCNodes := id (gsCNodes s')\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x6. APIType_map2 ty = ArchObject x6 \<Longrightarrow> (x6 = SmallPageObj \<longrightarrow> (\<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SmallPageObj) n us) then Some ARMSmallPage else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = LargePageObj \<longrightarrow> (\<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject LargePageObj) n us) then Some ARMLargePage else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = SectionObj \<longrightarrow> (\<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SectionObj) n us) then Some ARMSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = SuperSectionObj \<longrightarrow> (\<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SuperSectionObj) n us) then Some ARMSuperSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = PageTableObj \<longrightarrow> (\<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = PageDirectoryObj \<longrightarrow> (\<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) \<and> (x6 = ASIDPoolObj \<longrightarrow> (\<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>)) proof (prove)
goal (7 subgoals):
 1. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SmallPageObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SmallPageObj) n us) then Some ARMSmallPage else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 2. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = LargePageObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject LargePageObj) n us) then Some ARMLargePage else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 3. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SectionObj) n us) then Some ARMSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 4. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SuperSectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SuperSectionObj) n us) then Some ARMSuperSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 5. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageTableObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 6. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 7. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr> proof (prove)
goal (6 subgoals):
 1. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = LargePageObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject LargePageObj) n us) then Some ARMLargePage else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 2. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SectionObj) n us) then Some ARMSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 3. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SuperSectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SuperSectionObj) n us) then Some ARMSuperSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 4. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageTableObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 5. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 6. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr> proof (prove)
goal (5 subgoals):
 1. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SectionObj) n us) then Some ARMSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 2. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SuperSectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SuperSectionObj) n us) then Some ARMSuperSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 3. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageTableObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 4. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 5. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = SuperSectionObj\<rbrakk> \<Longrightarrow> \<exists>x. gsUserPages_update (\<lambda>ups x. if x \<in> set (retype_addrs ptr (ArchObject SuperSectionObj) n us) then Some ARMSuperSection else ups x) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 2. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageTableObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 3. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 4. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageTableObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 2. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = PageDirectoryObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr>
 3. \<And>x6. \<lbrakk>APIType_map2 ty = ArchObject x6; x6 = ASIDPoolObj\<rbrakk> \<Longrightarrow> \<exists>x. s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr> = s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'), gsUserPages := x (gsUserPages s')\<rparr> proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>f' g' h'. update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\<rparr>) = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s')\<rparr>

goal:
No subgoals!