theory CSpace1_R

lemma mdb_chunked_preserve_oneway:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes sameRegion:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'
  \<and> sameRegionAs (cteCap cte) = sameRegionAs (cteCap cte')
  \<and> (\<lambda>x. sameRegionAs x (cteCap cte)) = (\<lambda>x. sameRegionAs x (cteCap cte'))"
  assumes node:"\<And>p. mdb_next m p = mdb_next m' p"
  shows
  "mdb_chunked m \<Longrightarrow> mdb_chunked m'" apply (clarsimp simp:mdb_chunked_def) apply (drule_tac x=p in spec) apply (drule_tac x=p' in spec) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply clarsimp apply (case_tac ya) apply (case_tac y) apply (frule_tac x = p in sameRegion,assumption) apply (frule_tac x = p' in sameRegion,assumption) apply clarsimp apply (erule impE) apply (drule fun_cong)+ apply fastforce apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'") apply (subgoal_tac "m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p") apply (frule_tac m = m and
              x = p and c = cap and p = p and p'=p' in is_chunk_preserve[rotated -1]) apply (simp add:dom) apply (rule sameRegion) apply simp+ apply (rule node) apply assumption apply (frule_tac x = p' and c = cap' and p = p' and p'=p in is_chunk_preserve[rotated -1]) apply (rule dom) apply (rule sameRegion) apply assumption+ apply (rule node) apply assumption apply clarsimp apply (rule connect_eqv_singleE) apply (clarsimp simp:mdb_next_rel_def node) apply (rule connect_eqv_singleE) apply (clarsimp simp:mdb_next_rel_def node) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked m \<Longrightarrow> mdb_chunked m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>\<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p))\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p))\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m' p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); p \<in> dom m; m' p = Some (CTE cap n)\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); p \<in> dom m; m' p = Some (CTE cap n); p' \<in> dom m; m' p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' y ya. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. y = CTE cap n) \<longrightarrow> (\<forall>cap'. (\<exists>n'. ya = CTE cap' n') \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some y; m p' = Some ya\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' y ya x1 x2. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. y = CTE cap n) \<longrightarrow> (\<forall>cap'. (\<exists>n'. ya = CTE cap' n') \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some y; m p' = Some ya; ya = CTE x1 x2\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' y ya x1 x2 x1a x2a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. y = CTE cap n) \<longrightarrow> (\<forall>cap'. (\<exists>n'. ya = CTE cap' n') \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some y; m p' = Some ya; ya = CTE x1 x2; y = CTE x1a x2a\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' y ya x1 x2 x1a x2a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. y = CTE cap n) \<longrightarrow> (\<forall>cap'. (\<exists>n'. ya = CTE cap' n') \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some y; m p' = Some ya; ya = CTE x1 x2; y = CTE x1a x2a; cteMDBNode y = cteMDBNode (CTE cap n) \<and> global.sameRegionAs (cteCap y) = global.sameRegionAs (cteCap (CTE cap n)) \<and> (\<lambda>x. global.sameRegionAs x (cteCap y)) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap n)))\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' y ya x1 x2 x1a x2a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. y = CTE cap n) \<longrightarrow> (\<forall>cap'. (\<exists>n'. ya = CTE cap' n') \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some y; m p' = Some ya; ya = CTE x1 x2; y = CTE x1a x2a; cteMDBNode y = cteMDBNode (CTE cap n) \<and> global.sameRegionAs (cteCap y) = global.sameRegionAs (cteCap (CTE cap n)) \<and> (\<lambda>x. global.sameRegionAs x (cteCap y)) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap n))); cteMDBNode ya = cteMDBNode (CTE cap' n') \<and> global.sameRegionAs (cteCap ya) = global.sameRegionAs (cteCap (CTE cap' n')) \<and> (\<lambda>x. global.sameRegionAs x (cteCap ya)) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap' n')))\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; global.sameRegionAs cap x1 \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap')\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap x1
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a (?x46 p p' cap n cap' n' x1 x1a) = global.sameRegionAs cap (?x46 p p' cap n cap' n' x1 x1a); global.sameRegionAs (?x48 p p' cap n cap' n' x1 x1a) x1a = global.sameRegionAs (?x48 p p' cap n cap' n' x1 x1a) cap; global.sameRegionAs x1 (?x50 p p' cap n cap' n' x1 x1a) = global.sameRegionAs cap' (?x50 p p' cap n cap' n' x1 x1a); global.sameRegionAs (?x52 p p' cap n cap' n' x1 x1a) x1 = global.sameRegionAs (?x52 p p' cap n cap' n' x1 x1a) cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap x1
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (x \<in> dom m) = (x \<in> dom m')
 2. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m p = Some (CTE (?a78 p p' cap n cap' n' x1 x1a) (?b78 p p' cap n cap' n' x1 x1a))
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m (?a78 p p' cap n cap' n' x1 x1a) p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 7. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m p = Some (CTE (?a78 p p' cap n cap' n' x1 x1a) (?b78 p p' cap n cap' n' x1 x1a))
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m (?a78 p p' cap n cap' n' x1 x1a) p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x80 p p' cap n cap' n' x1 x1a x cte cte') = Some cte
 2. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x80 p p' cap n cap' n' x1 x1a x cte cte') = Some cte'
 3. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m p = Some (CTE (?a78 p p' cap n cap' n' x1 x1a) (?b78 p p' cap n cap' n' x1 x1a))
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m (?a78 p p' cap n cap' n' x1 x1a) p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 7. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m p = Some (CTE (?a78 p p' cap n cap' n' x1 x1a) (?b78 p p' cap n cap' n' x1 x1a))
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m (?a78 p p' cap n cap' n' x1 x1a) p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m p = Some (CTE (?a78 p p' cap n cap' n' x1 x1a) (?b78 p p' cap n cap' n' x1 x1a))
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m (?a78 p p' cap n cap' n' x1 x1a) p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> (x \<in> dom (?m85 p p' cap n cap' n' x1 x1a)) = (x \<in> dom m')
 2. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; ?m85 p p' cap n cap' n' x1 x1a x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> mdb_next (?m85 p p' cap n cap' n' x1 x1a) pa = mdb_next m' pa
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> ?m85 p p' cap n cap' n' x1 x1a p' = Some (CTE (?a85 p p' cap n cap' n' x1 x1a) (?b85 p p' cap n cap' n' x1 x1a))
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk (?m85 p p' cap n cap' n' x1 x1a) (?a85 p p' cap n cap' n' x1 x1a) p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 7. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte' \<and> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> m p' = Some (CTE (?a85 p p' cap n cap' n' x1 x1a) (?b85 p p' cap n cap' n' x1 x1a))
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk m (?a85 p p' cap n cap' n' x1 x1a) p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x88 p p' cap n cap' n' x1 x1a x cte cte') = Some cte
 2. \<And>p p' cap n cap' n' x1 x1a x cte cte'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x88 p p' cap n cap' n' x1 x1a x cte cte') = Some cte'
 3. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> m p' = Some (CTE (?a85 p p' cap n cap' n' x1 x1a) (?b85 p p' cap n cap' n' x1 x1a))
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk m (?a85 p p' cap n cap' n' x1 x1a) p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 6. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 7. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a pa. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> m p' = Some (CTE (?a85 p p' cap n cap' n' x1 x1a) (?b85 p p' cap n cap' n' x1 x1a))
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk m (?a85 p p' cap n cap' n' x1 x1a) p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 5. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'\<rbrakk> \<Longrightarrow> m p' = Some (CTE (?a85 p p' cap n cap' n' x1 x1a) (?b85 p p' cap n cap' n' x1 x1a))
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk m (?a85 p p' cap n cap' n' x1 x1a) p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 4. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m x1a p p' = is_chunk m' cap p p'; is_chunk m x1 p' p = is_chunk m' cap' p' p\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' cap p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' cap' p' p)
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 3. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p = m' \<turnstile> p' \<leadsto>\<^sup>+ p
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n' x1 x1a pa p'a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p); m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> pa \<leadsto> p'a = m' \<turnstile> pa \<leadsto> p'a
 2. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' x1 x1a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' = m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n' x1 x1a pa p'a. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m' p = Some (CTE cap n); m' p' = Some (CTE cap' n'); m p = Some (CTE x1a n); m p' = Some (CTE x1 n'); global.sameRegionAs x1a = global.sameRegionAs cap; (\<lambda>x. global.sameRegionAs x x1a) = (\<lambda>x. global.sameRegionAs x cap); global.sameRegionAs x1 = global.sameRegionAs cap'; (\<lambda>x. global.sameRegionAs x x1) = (\<lambda>x. global.sameRegionAs x cap'); (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m x1a p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m x1 p' p)\<rbrakk> \<Longrightarrow> m \<turnstile> pa \<leadsto> p'a = m' \<turnstile> pa \<leadsto> p'a proof (prove)
goal:
No subgoals!