theory CSpace_R

lemma chunked' [simp]:
  "mdb_chunked n'" using src dest apply (clarsimp simp: mdb_chunked_def) apply (drule n'_cap)+ apply (clarsimp simp: n'_trancl_eq) apply (clarsimp split: if_split_asm) prefer 3 apply (frule (3) mdb_chunkedD, rule chunked) apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp simp: is_chunk_def n'_trancl_eq n_rtrancl_eq' n_dest' new_dest_def) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply clarsimp apply (erule_tac x=src in allE) apply simp apply (erule sameRegion_src_c') apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (frule_tac p=p'' in m_cap') apply clarsimp apply clarsimp apply (clarsimp simp: is_chunk_def n'_trancl_eq n_rtrancl_eq' n_dest' new_dest_def) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply clarsimp apply (erule_tac x=src in allE) apply simp apply (erule sameRegion_src_c') apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (frule_tac p=p'' in m_cap') apply clarsimp apply (case_tac "p' = src") apply simp apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq') apply (erule disjE) apply (simp add: n_dest' new_dest_def) apply clarsimp apply (drule (1) trancl_rtrancl_trancl) apply simp apply clarsimp apply (drule c'_new) apply (erule (1) notE) apply (case_tac "p=src") apply clarsimp apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq') apply (erule disjE) apply (clarsimp simp: n_dest' new_dest_def) apply clarsimp apply (drule (1) trancl_rtrancl_trancl) apply simp apply (case_tac "isIRQControlCap src_cap") apply (drule (2) irq_control_src) apply simp apply (drule not_irq_parentD) apply clarsimp apply (frule (2) ut_src) apply clarsimp apply (subgoal_tac "src \<in> descendants_of' p m") prefer 2 apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp apply fastforce apply (frule_tac m=m and p=p and p'=src in mdb_chunkedD, assumption+) apply (clarsimp simp: descendants_of'_def) apply (drule subtree_parent) apply (clarsimp simp: parentOf_def isMDBParentOf_def split: if_split_asm) apply simp apply (rule chunked) apply clarsimp apply (erule disjE) apply clarsimp apply (rule conjI) prefer 2 apply clarsimp apply (drule (1) trancl_trans, simp) apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq' split: if_split_asm) apply (clarsimp simp: n_dest' new_dest_def) apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap') apply clarsimp apply clarsimp apply (rule conjI) apply clarsimp apply (drule (1) trancl_trans, simp) apply (clarsimp simp: descendants_of'_def) apply (drule subtree_mdb_next) apply (drule (1) trancl_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked n' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdb_chunked n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE cap n); n' p' = Some (CTE cap' n'a); 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 n cap' n'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node'); \<exists>node'. if p' = dest then cap' = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE cap' node')\<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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; if p = dest then cap = c' \<and> dest_node = node' else m p = Some (CTE cap node'); if p' = dest then cap' = c' \<and> dest_node = node'a else m p' = Some (CTE cap' node'a)\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p))) \<and> (p' \<noteq> dest \<longrightarrow> (p = dest \<longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)) \<and> (p \<noteq> dest \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p))) proof (prove)
goal (3 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; m p' = Some (CTE cap' node'a)\<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 n' cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; m p' = Some (CTE cap' node'a)\<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 n' cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p)
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; m p' = Some (CTE cap' node'a); (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 n' cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p)
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p)
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; m p' = Some (CTE cap' node'a); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p; m \<turnstile> p \<leadsto>\<^sup>+ p'; is_chunk m cap p p'\<rbrakk> \<Longrightarrow> is_chunk n' cap p p'
 2. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> (p'' = dest \<longrightarrow> (p = src \<longrightarrow> p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> global.sameRegionAs cap c') \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> global.sameRegionAs cap c')) \<and> (p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> (p = src \<longrightarrow> p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> global.sameRegionAs cap c') \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> global.sameRegionAs cap c')
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 4. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 5. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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>+ src \<longrightarrow> p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> global.sameRegionAs cap c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 4. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 5. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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>+ src; p' \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 4. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 5. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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>+ src; p' \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p'; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m src = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 4. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 5. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (5 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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>+ src; p' \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p'; global.sameRegionAs cap src_cap\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')
 3. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 4. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 5. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; \<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''); p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p'\<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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; p'' \<noteq> dest; 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 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''; 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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'; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p'; global.sameRegionAs cap cap''; m p'' = Some (CTE cap'' n''); \<exists>node'. if p'' = dest then cap'' = dest_cap \<and> n' p'' = Some (CTE c' node') else n' p'' = Some (CTE cap'' node')\<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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' cap' p' p
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; m p' = Some (CTE cap' node'a); m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p'; m \<turnstile> p' \<leadsto>\<^sup>+ p; is_chunk m cap' p' p\<rbrakk> \<Longrightarrow> is_chunk n' cap' p' p
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> (p'' = dest \<longrightarrow> (p' = src \<longrightarrow> p \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> global.sameRegionAs cap' c') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> p \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> global.sameRegionAs cap' c')) \<and> (p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<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' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> (p' = src \<longrightarrow> p \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> global.sameRegionAs cap' c') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> p \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> global.sameRegionAs cap' c')
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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>+ src \<longrightarrow> p \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> global.sameRegionAs cap' c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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>+ src; p \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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>+ src; p \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p; m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> m \<turnstile> src \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m src = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p p' cap cap' node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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>+ src; p \<noteq> src; m \<turnstile> src \<leadsto>\<^sup>* p; global.sameRegionAs cap' src_cap\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' c'
 2. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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> p'' \<noteq> dest \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<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' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; \<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''); p'' \<noteq> dest; m \<turnstile> p' \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; p'' \<noteq> dest; 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 cap' cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; p'' \<noteq> dest; m \<turnstile> p' \<leadsto>\<^sup>+ p''; 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' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap' node' node'a p'' cap'' n''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap cap'; p \<noteq> p'; p \<noteq> dest; m p = Some (CTE cap node'); p' \<noteq> dest; 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; p'' \<noteq> dest; m \<turnstile> p' \<leadsto>\<^sup>+ p''; m \<turnstile> p'' \<leadsto>\<^sup>* p; global.sameRegionAs cap' cap''; m p'' = Some (CTE cap'' n''); \<exists>node'. if p'' = dest then cap'' = dest_cap \<and> n' p'' = Some (CTE c' node') else n' p'' = Some (CTE cap'' node')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' = src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; p' = src\<rbrakk> \<Longrightarrow> is_chunk n' src_cap src dest
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; n' \<turnstile> src \<leadsto>\<^sup>+ p''; n' \<turnstile> p'' \<leadsto>\<^sup>* dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' = dest \<or> p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' = dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 3. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest; m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' src_cap; p'' \<noteq> dest; m \<turnstile> p'' \<leadsto>\<^sup>* src; m \<turnstile> src \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> p' = src \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (p' = src \<longrightarrow> is_chunk n' cap' src dest) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m p' = Some (CTE cap' node'a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p' cap' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs c' cap'; dest \<noteq> p'; p' \<noteq> src; \<not> global.sameRegionAs c' cap'\<rbrakk> \<Longrightarrow> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n' c' dest p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap' p' dest)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p = src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> is_chunk n' src_cap src dest
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' \<turnstile> src \<leadsto>\<^sup>+ p''; n' \<turnstile> p'' \<leadsto>\<^sup>* dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' = dest \<or> p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' = dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p'' = dest then True else m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest \<and> m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> src \<leadsto>\<^sup>+ p''; p'' \<noteq> dest; m \<turnstile> p'' \<leadsto>\<^sup>* src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p'' \<noteq> dest; m \<turnstile> p'' \<leadsto>\<^sup>* src; m \<turnstile> src \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isIRQControlCap src_cap\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; \<not> isIRQControlCap src_cap\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; p = src\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; \<not> isIRQControlCap src_cap\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; \<not> isIRQControlCap src_cap\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> (p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (p = src \<longrightarrow> is_chunk n' cap src dest) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap \<and> untypedRange cap \<inter> untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> src \<in> descendants_of' p m proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> src \<in> descendants_of' p m
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; (untypedRange src_cap \<subseteq> untypedRange cap \<or> untypedRange cap \<subseteq> untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange cap = {}) \<and> (untypedRange src_cap \<subset> untypedRange cap \<longrightarrow> src \<in> descendants_of' p m \<and> untypedRange src_cap \<inter> usableUntypedRange cap = {}) \<and> (untypedRange cap \<subset> untypedRange src_cap \<longrightarrow> p \<in> descendants_of' src m \<and> untypedRange cap \<inter> usableUntypedRange src_cap = {}) \<and> (untypedRange src_cap = untypedRange cap \<longrightarrow> p \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {} \<or> src \<in> descendants_of' p m \<and> usableUntypedRange cap = {} \<or> src = p)\<rbrakk> \<Longrightarrow> src \<in> descendants_of' p m
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; untypedRange src_cap \<subseteq> untypedRange cap \<or> untypedRange cap = untypedRange src_cap \<or> untypedRange src_cap \<inter> untypedRange cap = {}; untypedRange src_cap \<subset> untypedRange cap \<longrightarrow> src \<in> descendants_of' p m \<and> untypedRange src_cap \<inter> usableUntypedRange cap = {}; \<not> untypedRange cap \<subset> untypedRange src_cap; untypedRange src_cap = untypedRange cap \<longrightarrow> src \<in> descendants_of' p m \<and> usableUntypedRange cap = {}\<rbrakk> \<Longrightarrow> src \<in> descendants_of' p m
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> global.sameRegionAs cap src_cap
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p \<noteq> src
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> mdb_chunked m
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; m \<turnstile> p \<rightarrow> src\<rbrakk> \<Longrightarrow> global.sameRegionAs cap src_cap
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p \<noteq> src
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> mdb_chunked m
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (4 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> global.sameRegionAs cap src_cap
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p \<noteq> src
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> mdb_chunked m
 4. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p \<noteq> src
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> mdb_chunked m
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> mdb_chunked m
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p)\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<or> m \<turnstile> src \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p)
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> p \<leadsto>\<^sup>+ src; m \<turnstile> src \<leadsto>\<^sup>+ p; is_chunk m src_cap src p\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node' p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* src \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; n' \<turnstile> p \<leadsto>\<^sup>+ p''; n' \<turnstile> p'' \<leadsto>\<^sup>* dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (3 subgoals):
 1. \<And>p cap node' p''. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* src \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' = dest\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' dest = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p cap node' p''. \<lbrakk>m \<turnstile> p'' \<leadsto>\<^sup>* src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* src \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 3. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node' p''. \<lbrakk>m \<turnstile> p'' \<leadsto>\<^sup>* src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* src \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node' p''. \<lbrakk>m \<turnstile> p'' \<leadsto>\<^sup>* src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* src \<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 cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node' p'' cap'' n''. \<lbrakk>m \<turnstile> p'' \<leadsto>\<^sup>* src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' \<noteq> dest; 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 cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (2 subgoals):
 1. \<And>p cap node' p'' cap'' n''. \<lbrakk>m \<turnstile> p'' \<leadsto>\<^sup>* src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> src \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs src_cap cap'')); m \<turnstile> p \<leadsto>\<^sup>+ src; p'' \<noteq> dest; m \<turnstile> p \<leadsto>\<^sup>+ p''; global.sameRegionAs cap cap''; \<exists>node'. if p'' = dest then cap'' = dest_cap \<and> n' p'' = Some (CTE c' node') else n' p'' = Some (CTE cap'' node')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. n' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> (m \<turnstile> src \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n' c' dest p) proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest) \<and> is_chunk n' c' dest p proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk n' cap p dest
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal (2 subgoals):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ src; is_chunk m cap p src\<rbrakk> \<Longrightarrow> is_chunk n' cap p dest
 2. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; descendants_of' src m = {}; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; src \<in> descendants_of' p m; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; m \<turnstile> p \<rightarrow> src; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> src \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal (1 subgoal):
 1. \<And>p cap node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); global.sameRegionAs cap c'; p \<noteq> dest; m p = Some (CTE cap node'); p \<noteq> src; isUntypedCap src_cap; \<forall>x. \<not> m \<turnstile> src \<rightarrow> x; capRange c' \<noteq> {}; isUntypedCap cap; untypedRange cap \<inter> untypedRange src_cap \<noteq> {}; m \<turnstile> p \<leadsto>\<^sup>+ src \<longrightarrow> is_chunk m cap p src; is_chunk m src_cap src p; m \<turnstile> p \<leadsto>\<^sup>+ src; m \<turnstile> src \<leadsto>\<^sup>+ src\<rbrakk> \<Longrightarrow> is_chunk n' c' dest p proof (prove)
goal:
No subgoals!