theory CSpace1_R

lemma is_chunk_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 " \<lbrakk>m x =Some (CTE a b);m' x = Some (CTE c d)\<rbrakk> \<Longrightarrow> is_chunk m a p p' \<Longrightarrow> is_chunk m' c p p'" apply (clarsimp simp:is_chunk_def) apply (drule_tac x= p'' in spec) 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 iffD1[OF dom,OF domI]) apply (clarsimp) apply (frule_tac x1 = p'' in iffD1[OF dom,OF domI]) apply clarsimp apply (frule_tac x = p'' in sameRegion,assumption) apply clarsimp apply (frule_tac x = x in sameRegion,assumption) apply clarsimp apply (case_tac y) apply (drule_tac fun_cong)+ apply fastforce apply simp apply (erule iffD1[OF connect_eqv_singleE',rotated -1]) 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. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); is_chunk m a p p'\<rbrakk> \<Longrightarrow> is_chunk m' c p p' proof (prove)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap'' proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p''\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p' = m' \<turnstile> p'' \<leadsto>\<^sup>* p'; x \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' n''. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' n'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' n''. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' n''); p'' \<in> dom m'\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. m' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' n'' y. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' n''); m' p'' = Some y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' n'' y. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' n''); m' p'' = Some y; cteMDBNode (CTE cap'' n'') = cteMDBNode y \<and> global.sameRegionAs (cteCap (CTE cap'' n'')) = global.sameRegionAs (cteCap y) \<and> (\<lambda>x. global.sameRegionAs x (cteCap (CTE cap'' n''))) = (\<lambda>x. global.sameRegionAs x (cteCap y))\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' y. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' (cteMDBNode y)); m' p'' = Some y; global.sameRegionAs cap'' = global.sameRegionAs (cteCap y); (\<lambda>x. global.sameRegionAs x cap'') = (\<lambda>x. global.sameRegionAs x (cteCap y))\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' y. \<lbrakk>m x = Some (CTE a b); 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 c d); global.sameRegionAs a cap''; m p'' = Some (CTE cap'' (cteMDBNode y)); m' p'' = Some y; global.sameRegionAs cap'' = global.sameRegionAs (cteCap y); (\<lambda>x. global.sameRegionAs x cap'') = (\<lambda>x. global.sameRegionAs x (cteCap y)); cteMDBNode (CTE a b) = cteMDBNode (CTE c d) \<and> global.sameRegionAs (cteCap (CTE a b)) = global.sameRegionAs (cteCap (CTE c d)) \<and> (\<lambda>x. global.sameRegionAs x (cteCap (CTE a b))) = (\<lambda>x. global.sameRegionAs x (cteCap (CTE c d)))\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' y. \<lbrakk>m x = Some (CTE a d); 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 c d); global.sameRegionAs c cap''; m p'' = Some (CTE cap'' (cteMDBNode y)); m' p'' = Some y; global.sameRegionAs cap'' = global.sameRegionAs (cteCap y); (\<lambda>x. global.sameRegionAs x cap'') = (\<lambda>x. global.sameRegionAs x (cteCap y)); b = d; global.sameRegionAs a = global.sameRegionAs c; (\<lambda>x. global.sameRegionAs x a) = (\<lambda>x. global.sameRegionAs x c)\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' y x1 x2. \<lbrakk>m x = Some (CTE a d); 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 c d); global.sameRegionAs c cap''; m p'' = Some (CTE cap'' (cteMDBNode y)); m' p'' = Some y; global.sameRegionAs cap'' = global.sameRegionAs (cteCap y); (\<lambda>x. global.sameRegionAs x cap'') = (\<lambda>x. global.sameRegionAs x (cteCap y)); b = d; global.sameRegionAs a = global.sameRegionAs c; (\<lambda>x. global.sameRegionAs x a) = (\<lambda>x. global.sameRegionAs x c); y = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (3 subgoals):
 1. \<And>p'' cap'' y x1 x2. \<lbrakk>m x = Some (CTE a d); 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 c d); global.sameRegionAs c cap''; m p'' = Some (CTE cap'' (cteMDBNode y)); m' p'' = Some y; b = d; y = CTE x1 x2; global.sameRegionAs cap'' (?x44 p'' cap'' y x1 x2) = global.sameRegionAs (cteCap y) (?x44 p'' cap'' y x1 x2); global.sameRegionAs (?x45 p'' cap'' y x1 x2) cap'' = global.sameRegionAs (?x45 p'' cap'' y x1 x2) (cteCap y); global.sameRegionAs a (?x46 p'' cap'' y x1 x2) = global.sameRegionAs c (?x46 p'' cap'' y x1 x2); global.sameRegionAs (?x47 p'' cap'' y x1 x2) a = global.sameRegionAs (?x47 p'' cap'' y x1 x2) c\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. y = CTE cap'' n'') \<and> global.sameRegionAs c cap''
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); 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''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); m \<turnstile> p \<leadsto>\<^sup>+ p''\<rbrakk> \<Longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p'
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (2 subgoals):
 1. \<And>p'' pa p'a. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap''); m \<turnstile> p \<leadsto>\<^sup>+ p''\<rbrakk> \<Longrightarrow> m' \<turnstile> pa \<leadsto> p'a = m \<turnstile> pa \<leadsto> p'a
 2. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' = m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
goal (1 subgoal):
 1. \<And>p'' pa p'a. \<lbrakk>m x = Some (CTE a b); m' x = Some (CTE c d); m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs a cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> pa \<leadsto> p'a = m' \<turnstile> pa \<leadsto> p'a proof (prove)
goal:
No subgoals!