theory Detype_C

lemma valid_footprint_typ_region_bytes:
  assumes neq_byte: "td \<noteq> typ_uinfo_t TYPE (word8)"
  shows "valid_footprint (typ_region_bytes ptr bits hp) p td =
   ({p ..+ size_td td} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> valid_footprint hp p td)" 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_region_bytes_def list_map_le_singleton neq_byte
                          neq_types_not_typ_slice_eq) apply clarsimp apply (drule spec, drule (1) mp) apply (clarsimp simp: typ_region_bytes_def list_map_le_singleton neq_byte
                         neq_types_not_typ_slice_eq
                  split: if_split_asm) apply clarsimp apply (drule spec, drule (1) mp) apply (subgoal_tac "p + of_nat y \<notin> {ptr..+2 ^ bits}") apply (simp add: typ_bytes_region_out) apply clarsimp apply (drule intvlD) apply (clarsimp simp: disjoint_iff_not_equal ) apply (drule_tac x = "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. valid_footprint (typ_region_bytes ptr bits hp) p td = ({p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint hp p td) proof (prove)
goal (1 subgoal):
 1. (0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)))) = ({p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y)))) proof (prove)
goal (2 subgoals):
 1. 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) \<Longrightarrow> {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y)))
 2. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y)))
 2. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}
 2. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 3. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)); y \<in> {p..+size_td td}; y \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 3. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)); y \<in> {ptr..+2 ^ bits}; \<exists>k. y = p + word_of_nat k \<and> k < size_td td\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 3. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)); p + word_of_nat k \<in> {ptr..+2 ^ bits}; k < size_td td\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 3. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>p + word_of_nat k \<in> {ptr..+2 ^ bits}; k < size_td td; list_map (typ_slice_t td k) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat k)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat k))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 3. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < size_td td; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 2. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)); y < size_td td\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 2. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))
 2. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (1 subgoal):
 1. {p..+size_td td} \<inter> {ptr..+2 ^ bits} = {} \<and> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))) \<Longrightarrow> 0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; \<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y)); y < size_td td\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y)); p + word_of_nat y \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (typ_region_bytes ptr bits hp (p + word_of_nat y)) \<and> fst (typ_region_bytes ptr bits hp (p + word_of_nat y))
 2. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> p + word_of_nat y \<notin> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)) \<and> fst (hp (p + word_of_nat y))\<rbrakk> \<Longrightarrow> p + word_of_nat y \<notin> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)); fst (hp (p + word_of_nat y)); p + word_of_nat y \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>{p..+size_td td} \<inter> {ptr..+2 ^ bits} = {}; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (p + word_of_nat y)); fst (hp (p + word_of_nat y)); \<exists>k. 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>{p..+size_td td}. \<forall>y\<in>{ptr..+2 ^ bits}. x \<noteq> y; y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); 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>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> p + word_of_nat y \<in> {p..+size_td td}
 2. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits\<rbrakk> \<Longrightarrow> y < size_td td
 2. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; \<forall>ya\<in>{ptr..+2 ^ bits}. p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); 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>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; p + word_of_nat y \<noteq> ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>y < size_td td; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (hp (ptr + word_of_nat k)); fst (hp (ptr + word_of_nat k)); p + word_of_nat y = ptr + word_of_nat k; k < 2 ^ bits; p + word_of_nat y \<noteq> ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!