theory Detype_C

lemma h_t_valid_ptr_clear_region:
  fixes p :: "'a :: c_type ptr"
  shows "typ_clear_region ptr bits hp,g \<Turnstile>\<^sub>t p =
   ({ptr_val p ..+ size_of (TYPE ('a))} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p)" unfolding h_t_valid_def apply (clarsimp simp: valid_footprint_def Let_def) apply (rule iffI) apply clarsimp apply (rule conjI) apply (clarsimp simp: disjoint_iff_not_equal) apply (drule intvlD) apply (clarsimp simp: size_of_def) apply (drule spec, drule (1) mp) apply (clarsimp simp: typ_clear_region_def) apply clarsimp apply (drule spec, drule (1) mp) apply (clarsimp simp: typ_clear_region_def split: if_split_asm) apply clarsimp apply (drule spec, drule (1) mp) apply (subgoal_tac "ptr_val p + of_nat y \<notin> {ptr..+2 ^ bits}") apply (simp add: typ_clear_region_out) apply clarsimp apply (drule intvlD) apply (clarsimp simp: disjoint_iff_not_equal ) apply (drule_tac x = "ptr_val p + of_nat y" in bspec) apply (rule intvlI) apply (simp add: size_of_def) apply (drule_tac x = "ptr + of_nat k" in bspec) apply (erule intvlI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_clear_region ptr bits hp,g \<Turnstile>\<^sub>t p = ({ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p) proof (prove)
goal (1 subgoal):
 1. (valid_footprint (typ_clear_region ptr bits hp) (ptr_val p) (typ_uinfo_t TYPE('a)) \<and> g p) = ({ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint hp (ptr_val p) (typ_uinfo_t TYPE('a)) \<and> g p) proof (prove)
goal (1 subgoal):
 1. (0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p) = ({ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p) proof (prove)
goal (2 subgoals):
 1. 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p
 2. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y)))
 2. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}
 2. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 3. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p; y \<in> {ptr_val p..+size_of TYPE('a)}; y \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 3. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p; y \<in> {ptr..+2 ^ bits}; \<exists>k. y = ptr_val p + word_of_nat k \<and> k < size_of TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 3. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p; ptr_val p + word_of_nat k \<in> {ptr..+2 ^ bits}; k < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 3. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>g p; ptr_val p + word_of_nat k \<in> {ptr..+2 ^ bits}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat k)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat k))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 3. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 2. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)); g p; y < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 2. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))
 2. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (1 subgoal):
 1. {ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))) \<and> g p \<Longrightarrow> 0 < size_td (typ_info_t TYPE('a)) \<and> (\<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))) \<and> g p proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y)); g p; y < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y)); ptr_val p + word_of_nat y \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y)) \<and> fst (typ_clear_region ptr bits hp (ptr_val p + word_of_nat y))
 2. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<notin> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)) \<and> fst (hp (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<notin> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)); fst (hp (ptr_val p + word_of_nat y)); ptr_val p + word_of_nat y \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr_val p + word_of_nat y)); fst (hp (ptr_val p + word_of_nat y)); \<exists>k. ptr_val p + word_of_nat y = ptr + word_of_nat k \<and> k < 2 ^ bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>\<forall>x\<in>{ptr_val p..+size_of TYPE('a)}. \<forall>y\<in>{ptr..+2 ^ bits}. x \<noteq> y; g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<in> {ptr_val p..+size_of TYPE('a)}
 2. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> y < size_of TYPE('a)
 2. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr + word_of_nat k \<in> {ptr..+2 ^ bits}
 2. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; ptr_val p + word_of_nat y \<noteq> ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>g p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; ptr_val p + word_of_nat y \<noteq> ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!