theory Finalise_R

lemma mdb_chunked_n:
  "mdb_chunked n" using chunked apply (clarsimp simp: mdb_chunked_def) apply (drule n_cap)+ apply (clarsimp split: if_split_asm) apply (case_tac "p=slot", clarsimp) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (clarsimp simp: is_chunk_def) apply (simp add: n_trancl_eq n_rtrancl_eq) apply (rule conjI) apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked n proof (prove)
using this:
mdb_chunked m

goal (1 subgoal):
 1. mdb_chunked n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap na 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)); n p = Some (CTE cap na); n p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap na 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)); global.sameRegionAs cap cap'; p \<noteq> p'; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap); \<exists>cap'a node'. m p' = Some (CTE cap'a node') \<and> (if p' = slot then cap' = capability.NullCap else cap'a = cap')\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' cap'a node'. \<lbrakk>m p' = Some (CTE cap' node'); \<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)); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap'a node')) \<and> cap = capability.NullCap; p = slot \<or> (\<exists>node'. m p = Some (CTE cap'a node')) \<and> cap'a = cap\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' cap'a node'. \<lbrakk>m p' = Some (CTE cap' node'); \<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)); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap'a node')) \<and> cap = capability.NullCap; p = slot \<or> (\<exists>node'. m p = Some (CTE cap'a node')) \<and> cap'a = cap; p \<noteq> slot\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); \<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)); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a)\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); \<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> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); \<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> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. n \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> n \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. n \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> n \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap'')); m \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p'; \<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 cap cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap'')); m \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; 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 cap cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap'')); m \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p'; global.sameRegionAs cap cap''; m p'' = Some (CTE cap'' n'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap'')); m \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p'; global.sameRegionAs cap cap''; \<exists>cap' node'. n p'' = Some (CTE cap' node') \<and> (if p'' = slot then cap' = capability.NullCap else cap' = cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<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 cap' cap''))\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<and> p'' \<noteq> slot \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p' \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p; \<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 cap' cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p' \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; 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 cap' cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p' \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p; global.sameRegionAs cap' cap''; m p'' = Some (CTE cap'' n'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m p' = Some (CTE cap' node'); global.sameRegionAs cap cap'; p \<noteq> p'; p' \<noteq> slot; p \<noteq> slot; m p = Some (CTE cap node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<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 cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p' \<leadsto>\<^sup>+ p''; p'' \<noteq> slot; m \<turnstile> p'' \<leadsto>\<^sup>* p; global.sameRegionAs cap' cap''; \<exists>cap' node'. n p'' = Some (CTE cap' node') \<and> (if p'' = slot then cap' = capability.NullCap else cap' = cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'' proof (prove)
goal:
No subgoals!