theory CNodeInv_R

lemma chunked':
  "mdb_chunked m'" using chunked apply (clarsimp simp: mdb_chunked_def) apply (drule m'_cap)+ apply (clarsimp simp: m'_trancl_eq sameRegion_cap'_src split: if_split_asm) apply (erule_tac x=src in allE) apply (erule_tac x="s_d_swap p' src dest" in allE) apply (clarsimp simp: src s_d_swap_other) apply (rule conjI) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def split: if_split_asm) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def sameRegionAs_parent_eq split: if_split_asm) apply (simp add: s_d_swap_other) apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (clarsimp simp: src sameRegionAs_parent_eq) apply (rule conjI) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def sameRegionAs_parent_eq split: if_split_asm) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def sameRegionAs_parent_eq split: if_split_asm) apply (simp add: s_d_swap_other) apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply clarsimp apply (rule conjI) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def sameRegionAs_parent_eq split: if_split_asm) apply (clarsimp simp: is_chunk_def m'_rtrancl_eq m'_trancl_eq s_d_swap_other) apply (erule_tac x="s_d_swap p'' src dest" in allE) apply clarsimp apply (drule_tac p="s_d_swap p'' src dest" in m_cap) apply (clarsimp simp: s_d_swap_def sameRegionAs_parent_eq split: if_split_asm) done

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

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