theory CSpace_I

lemma mdb_chunked_init:
  assumes x: "m x = Some cte"
  assumes no_m: "no_mdb cte"
  assumes no_c: "caps_no_overlap' m (capRange cap)"
  assumes no_v: "fresh_virt_cap_class (capClass cap) m"
  assumes no_0: "no_0 m"
  assumes dlist: "valid_dlist m"
  assumes chain: "mdb_chain_0 m"
  assumes chunked: "mdb_chunked m"
  assumes valid: "valid_objs' s" "m = ctes_of s" "s \<turnstile>' cap"
  shows "mdb_chunked (m(x \<mapsto> CTE cap initMDBNode))" unfolding mdb_chunked_def proof clarify fix p p' c c' n n' define m' where "m' \<equiv> m (x \<mapsto> CTE cap initMDBNode)" assume p: "m' p = Some (CTE c n)" assume p': "m' p' = Some (CTE c' n')" assume r: "sameRegionAs c c'" assume neq: "p \<noteq> p'" note no_region = caps_no_overlap'_no_region [OF no_c valid no_v] from chain x no_0 have chain': "mdb_chain_0 m'" unfolding m'_def apply - apply (rule mdb_chain_0_update, clarsimp) apply clarsimp apply (drule rtranclD) apply (erule disjE, clarsimp) apply clarsimp apply (drule tranclD) apply (clarsimp simp: mdb_next_unfold) apply clarsimp apply assumption apply assumption done moreover from x no_0 have x0 [simp]: "x \<noteq> 0" by clarsimp with no_0 have "no_0 m'" unfolding m'_def by (rule no_0_update) ultimately have nl: "no_loops m'" by (rule mdb_chain_0_no_loops) from p p' r neq no_region have px: "p \<noteq> x" by (clarsimp simp: m'_def) blast moreover from p p' r neq no_region have p'x: "p' \<noteq> x" by (clarsimp simp: m'_def) blast ultimately have m:
   "(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
    (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and>
    (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)" using chunked p p' neq r unfolding mdb_chunked_def m'_def by simp from x no_m px [symmetric] dlist no_0 have npx: "\<not> m \<turnstile> p \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) from x no_m p'x [symmetric] dlist no_0 have np'x: "\<not> m \<turnstile> p' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) show "(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
        (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and>
        (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)" proof (cases "m \<turnstile> p \<leadsto>\<^sup>+ p'") case True with m have ch: "is_chunk m c p p'" by simp from True npx have "m' \<turnstile> p \<leadsto>\<^sup>+ p'" unfolding m'_def by (rule mdb_trancl_other_update) moreover with nl have "\<not> m' \<turnstile> p' \<leadsto>\<^sup>+ p" apply clarsimp apply (drule (1) trancl_trans) apply (simp add: no_loops_def) done moreover have "is_chunk m' c p p'" unfolding is_chunk_def proof clarify fix p'' assume "m' \<turnstile> p \<leadsto>\<^sup>+ p''" with npx have "m \<turnstile> p \<leadsto>\<^sup>+ p''" unfolding m'_def by - (rule mdb_trancl_update_other) moreover then have p''x: "p'' \<noteq> x" using dlist x no_m no_0 apply clarsimp apply (drule tranclD2) apply clarsimp apply (frule vdlist_nextD0, simp, assumption) apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) done moreover assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p'" { moreover from x no_m p''x [symmetric] dlist no_0 have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) ultimately have "m \<turnstile> p'' \<leadsto>\<^sup>* p'" unfolding m'_def by (rule mdb_rtrancl_update_other) } ultimately have "\<exists>cap'' n''.
            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''" using ch by (simp add: is_chunk_def) with p''x show "\<exists>cap'' n''.
             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''" by (simp add: m'_def) qed ultimately show ?thesis by simp next case False with m have p'p: "m \<turnstile> p' \<leadsto>\<^sup>+ p" by simp with m have ch: "is_chunk m c' p' p" by simp from p'p np'x have "m' \<turnstile> p' \<leadsto>\<^sup>+ p" unfolding m'_def by (rule mdb_trancl_other_update) moreover with nl have "\<not> m' \<turnstile> p \<leadsto>\<^sup>+ p'" apply clarsimp apply (drule (1) trancl_trans) apply (simp add: no_loops_def) done moreover have "is_chunk m' c' p' p" unfolding is_chunk_def proof clarify fix p'' assume "m' \<turnstile> p' \<leadsto>\<^sup>+ p''" with np'x have "m \<turnstile> p' \<leadsto>\<^sup>+ p''" unfolding m'_def by - (rule mdb_trancl_update_other) moreover then have p''x: "p'' \<noteq> x" using dlist x no_m no_0 apply clarsimp apply (drule tranclD2) apply clarsimp apply (frule vdlist_nextD0, simp, assumption) apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) done moreover assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p" { moreover from x no_m p''x [symmetric] dlist no_0 have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) ultimately have "m \<turnstile> p'' \<leadsto>\<^sup>* p" unfolding m'_def by (rule mdb_rtrancl_update_other) } ultimately have "\<exists>cap'' n''.
            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''" using ch by (simp add: is_chunk_def) with p''x show "\<exists>cap'' n''.
             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''" by (simp add: m'_def) qed ultimately show ?thesis by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked (m(x \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<forall>p p' capa cap' n n'. (m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n) \<longrightarrow> (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n') \<longrightarrow> global.sameRegionAs capa cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
m' \<equiv> m(x \<mapsto> CTE cap initMDBNode)

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
m' p = Some (CTE c n)

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
m' p' = Some (CTE c' n')

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
global.sameRegionAs c c'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
p \<noteq> p'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
\<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
mdb_chain_0 m
m x = Some cte
no_0 m proof (prove)
using this:
mdb_chain_0 m
m x = Some cte
no_0 m

goal (1 subgoal):
 1. mdb_chain_0 m' proof (prove)
using this:
mdb_chain_0 m
m x = Some cte
no_0 m

goal (1 subgoal):
 1. mdb_chain_0 (m(x \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 (m(x \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode (CTE cap initMDBNode)), x) \<notin> (mdb_next_rel m)\<^sup>*
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m; m \<turnstile> 0 \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m; 0 = x \<or> 0 \<noteq> x \<and> m \<turnstile> 0 \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m; 0 \<noteq> x \<and> m \<turnstile> 0 \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m; x \<noteq> 0; m \<turnstile> 0 \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m; x \<noteq> 0; \<exists>z. m \<turnstile> 0 \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 4. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> x \<noteq> 0
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 3. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> no_0 m
 2. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; m x = Some cte; no_0 m\<rbrakk> \<Longrightarrow> mdb_chain_0 m proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_chain_0 m'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
mdb_chain_0 m'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
m x = Some cte
no_0 m proof (prove)
using this:
m x = Some cte
no_0 m

goal (1 subgoal):
 1. x \<noteq> 0 proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
no_0 m
x \<noteq> 0 proof (prove)
using this:
no_0 m
x \<noteq> 0

goal (1 subgoal):
 1. no_0 m' proof (prove)
using this:
no_0 m
x \<noteq> 0

goal (1 subgoal):
 1. no_0 (m(x \<mapsto> CTE cap initMDBNode)) proof (state)
this:
no_0 m'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
mdb_chain_0 m'
no_0 m' proof (prove)
using this:
mdb_chain_0 m'
no_0 m'

goal (1 subgoal):
 1. no_loops m' proof (state)
this:
no_loops m'

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
m' p = Some (CTE c n)
m' p' = Some (CTE c' n')
global.sameRegionAs c c'
p \<noteq> p'
\<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
using this:
m' p = Some (CTE c n)
m' p' = Some (CTE c' n')
global.sameRegionAs c c'
p \<noteq> p'
\<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c

goal (1 subgoal):
 1. p \<noteq> x proof (state)
this:
p \<noteq> x

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (state)
this:
p \<noteq> x

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
m' p = Some (CTE c n)
m' p' = Some (CTE c' n')
global.sameRegionAs c c'
p \<noteq> p'
\<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
using this:
m' p = Some (CTE c n)
m' p' = Some (CTE c' n')
global.sameRegionAs c c'
p \<noteq> p'
\<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c

goal (1 subgoal):
 1. p' \<noteq> x proof (state)
this:
p' \<noteq> x

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
p \<noteq> x
p' \<noteq> x proof (prove)
using this:
p \<noteq> x
p' \<noteq> x

goal (1 subgoal):
 1. (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p) proof (prove)
using this:
p \<noteq> x
p' \<noteq> x
mdb_chunked m
m' p = Some (CTE c n)
m' p' = Some (CTE c' n')
p \<noteq> p'
global.sameRegionAs c c'

goal (1 subgoal):
 1. (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p) proof (prove)
using this:
p \<noteq> x
p' \<noteq> x
\<forall>p p' cap cap' n n'. m p = Some (CTE cap n) \<longrightarrow> 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(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE c n)
(m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE c' n')
p \<noteq> p'
global.sameRegionAs c c'

goal (1 subgoal):
 1. (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p) proof (state)
this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
m x = Some cte
no_mdb cte
x \<noteq> p
valid_dlist m
no_0 m proof (prove)
using this:
m x = Some cte
no_mdb cte
x \<noteq> p
valid_dlist m
no_0 m

goal (1 subgoal):
 1. (p, x) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(p, x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (chain)
picking this:
m x = Some cte
no_mdb cte
x \<noteq> p'
valid_dlist m
no_0 m proof (prove)
using this:
m x = Some cte
no_mdb cte
x \<noteq> p'
valid_dlist m
no_0 m

goal (1 subgoal):
 1. (p', x) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(p', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>p p' capa cap' n n'. \<lbrakk>(m(x \<mapsto> CTE cap initMDBNode)) p = Some (CTE capa n); (m(x \<mapsto> CTE cap initMDBNode)) p' = Some (CTE cap' n'); global.sameRegionAs capa cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) capa p p') \<and> (m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk (m(x \<mapsto> CTE cap initMDBNode)) cap' p' p) proof (prove)
goal (1 subgoal):
 1. (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ p'

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
m \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
m \<turnstile> p \<leadsto>\<^sup>+ p'

goal (1 subgoal):
 1. is_chunk m c p p' proof (state)
this:
is_chunk m c p p'

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ p'
(p, x) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p'
(p, x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p'
(p, x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
this:
m' \<turnstile> p \<leadsto>\<^sup>+ p'

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
m' \<turnstile> p \<leadsto>\<^sup>+ p'

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
no_loops m'
m' \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
no_loops m'
m' \<turnstile> p \<leadsto>\<^sup>+ p'

goal (1 subgoal):
 1. (p', p) \<notin> (mdb_next_rel m')\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m'; m' \<turnstile> p \<leadsto>\<^sup>+ p'; m' \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m'; m' \<turnstile> p' \<leadsto>\<^sup>+ p; m' \<turnstile> p \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
(p', p) \<notin> (mdb_next_rel m')\<^sup>+

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
(p', p) \<notin> (mdb_next_rel m')\<^sup>+

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (prove)
goal (1 subgoal):
 1. is_chunk m' c p p' proof (prove)
goal (1 subgoal):
 1. \<forall>p''. m' \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m' \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'') proof (state)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m' \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
(p, x) \<notin> (mdb_next_rel m)\<^sup>*
m' \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
using this:
(p, x) \<notin> (mdb_next_rel m)\<^sup>*
m' \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
using this:
(p, x) \<notin> (mdb_next_rel m)\<^sup>*
m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ p'' proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ p'' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. p'' \<noteq> x proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p''
valid_dlist m
m x = Some cte
no_mdb cte
no_0 m

goal (1 subgoal):
 1. p'' \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ x; valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; \<exists>z. m \<turnstile> p \<leadsto>\<^sup>* z \<and> m \<turnstile> z \<leadsto> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; m \<turnstile> p \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; m \<turnstile> p \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> x; m \<turnstile> z \<leftarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
p'' \<noteq> x

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
p'' \<noteq> x

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
m x = Some cte
no_mdb cte
x \<noteq> p''
valid_dlist m
no_0 m proof (prove)
using this:
m x = Some cte
no_mdb cte
x \<noteq> p''
valid_dlist m
no_0 m

goal (1 subgoal):
 1. (p'', x) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p'
(p'', x) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p'
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> p'' \<leadsto>\<^sup>* p' proof (prove)
using this:
m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p'' \<leadsto>\<^sup>* p'
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> p'' \<leadsto>\<^sup>* p' proof (state)
this:
m \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
m \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
m \<turnstile> p \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p'

goal (1 subgoal):
 1. \<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p'
is_chunk m c p p'

goal (1 subgoal):
 1. \<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (chain)
picking this:
p'' \<noteq> x
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (prove)
using this:
p'' \<noteq> x
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap''

goal (1 subgoal):
 1. \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap'' proof (state)
this:
\<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c cap''

goal:
No subgoals! proof (state)
this:
is_chunk m' c p p'

goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>+ 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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)
 2. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
m' \<turnstile> p \<leadsto>\<^sup>+ p'
(p', p) \<notin> (mdb_next_rel m')\<^sup>+
is_chunk m' c p p' proof (prove)
using this:
m' \<turnstile> p \<leadsto>\<^sup>+ p'
(p', p) \<notin> (mdb_next_rel m')\<^sup>+
is_chunk m' c p p'

goal (1 subgoal):
 1. (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
(p, p') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
(p, p') \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
using this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
(p, p') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. m \<turnstile> p' \<leadsto>\<^sup>+ p proof (state)
this:
m \<turnstile> p' \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
m \<turnstile> p' \<leadsto>\<^sup>+ p proof (prove)
using this:
(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)
m \<turnstile> p' \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. is_chunk m c' p' p proof (state)
this:
is_chunk m c' p' p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
m \<turnstile> p' \<leadsto>\<^sup>+ p
(p', x) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p
(p', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m' \<turnstile> p' \<leadsto>\<^sup>+ p proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p
(p', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p proof (state)
this:
m' \<turnstile> p' \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
m' \<turnstile> p' \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
no_loops m'
m' \<turnstile> p' \<leadsto>\<^sup>+ p proof (prove)
using this:
no_loops m'
m' \<turnstile> p' \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m')\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m'; m' \<turnstile> p' \<leadsto>\<^sup>+ p; m' \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m'; m' \<turnstile> p \<leadsto>\<^sup>+ p'; m' \<turnstile> p' \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
(p, p') \<notin> (mdb_next_rel m')\<^sup>+

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
(p, p') \<notin> (mdb_next_rel m')\<^sup>+

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (prove)
goal (1 subgoal):
 1. is_chunk m' c' p' p proof (prove)
goal (1 subgoal):
 1. \<forall>p''. m' \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m' \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'') proof (state)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m' \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
(p', x) \<notin> (mdb_next_rel m)\<^sup>*
m' \<turnstile> p' \<leadsto>\<^sup>+ p'' proof (prove)
using this:
(p', x) \<notin> (mdb_next_rel m)\<^sup>*
m' \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. m \<turnstile> p' \<leadsto>\<^sup>+ p'' proof (prove)
using this:
(p', x) \<notin> (mdb_next_rel m)\<^sup>*
m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. m \<turnstile> p' \<leadsto>\<^sup>+ p'' proof (state)
this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
m \<turnstile> p' \<leadsto>\<^sup>+ p'' proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''

goal (1 subgoal):
 1. p'' \<noteq> x proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''
valid_dlist m
m x = Some cte
no_mdb cte
no_0 m

goal (1 subgoal):
 1. p'' \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p' \<leadsto>\<^sup>+ x; valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; \<exists>z. m \<turnstile> p' \<leadsto>\<^sup>* z \<and> m \<turnstile> z \<leadsto> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; m \<turnstile> p' \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>valid_dlist m; m x = Some cte; no_mdb cte; no_0 m; p'' = x; m \<turnstile> p' \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> x; m \<turnstile> z \<leftarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
p'' \<noteq> x

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
p'' \<noteq> x

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
m x = Some cte
no_mdb cte
x \<noteq> p''
valid_dlist m
no_0 m proof (prove)
using this:
m x = Some cte
no_mdb cte
x \<noteq> p''
valid_dlist m
no_0 m

goal (1 subgoal):
 1. (p'', x) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p
(p'', x) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m' \<turnstile> p'' \<leadsto>\<^sup>* p
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> p'' \<leadsto>\<^sup>* p proof (prove)
using this:
m(x \<mapsto> CTE cap initMDBNode) \<turnstile> p'' \<leadsto>\<^sup>* p
(p'', x) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> p'' \<leadsto>\<^sup>* p proof (state)
this:
m \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
m \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p

goal (1 subgoal):
 1. \<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (prove)
using this:
m \<turnstile> p' \<leadsto>\<^sup>+ p''
p'' \<noteq> x
m \<turnstile> p'' \<leadsto>\<^sup>* p
is_chunk m c' p' p

goal (1 subgoal):
 1. \<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap''

goal (1 subgoal):
 1. \<And>p''. \<lbrakk>m' \<turnstile> p' \<leadsto>\<^sup>+ p''; m' \<turnstile> p'' \<leadsto>\<^sup>* p\<rbrakk> \<Longrightarrow> \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (chain)
picking this:
p'' \<noteq> x
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (prove)
using this:
p'' \<noteq> x
\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap''

goal (1 subgoal):
 1. \<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap'' proof (state)
this:
\<exists>cap'' n''. m' p'' = Some (CTE cap'' n'') \<and> global.sameRegionAs c' cap''

goal:
No subgoals! proof (state)
this:
is_chunk m' c' p' p

goal (1 subgoal):
 1. (p, p') \<notin> (mdb_next_rel m)\<^sup>+ \<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' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (chain)
picking this:
m' \<turnstile> p' \<leadsto>\<^sup>+ p
(p, p') \<notin> (mdb_next_rel m')\<^sup>+
is_chunk m' c' p' p proof (prove)
using this:
m' \<turnstile> p' \<leadsto>\<^sup>+ p
(p, p') \<notin> (mdb_next_rel m')\<^sup>+
is_chunk m' c' p' p

goal (1 subgoal):
 1. (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p) proof (state)
this:
(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)

goal:
No subgoals! proof (state)
this:
(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)

goal:
No subgoals!