theory CNodeInv_R

lemma mdb_chunked_update_final:
  assumes chunked: "mdb_chunked m"
         and slot: "m slot = Some (CTE cap node)"
         and Fin1: "\<And>x cte. m x = Some cte \<Longrightarrow> x \<noteq> slot
                        \<Longrightarrow> \<not> sameRegionAs cap (cteCap cte)"
         and Fin2: "\<And>x cte. m x = Some cte \<Longrightarrow> x \<noteq> slot
                        \<Longrightarrow> \<not> sameRegionAs cap' (cteCap cte)"
         and Fin3: "\<And>x cte. m x = Some cte \<Longrightarrow> x \<noteq> slot
                        \<Longrightarrow> sameRegionAs (cteCap cte) cap
                        \<Longrightarrow> isUntypedCap (cteCap cte)"
         and Fin4: "\<And>x cte. m x = Some cte \<Longrightarrow> x \<noteq> slot
                        \<Longrightarrow> sameRegionAs (cteCap cte) cap'
                        \<Longrightarrow> isUntypedCap (cteCap cte)"
         and capR: "capRange cap = capRange cap'"
  shows            "mdb_chunked (m (slot \<mapsto> CTE cap' node))"
           (is "mdb_chunked ?m'") proof - note trancl[simp] = trancl_cap_upd [where m=m, OF slot] note rtrancl[simp] = rtrancl_cap_upd [where m=m, OF slot] have sameRegionAs:
    "\<And>x cte. \<lbrakk> m x = Some cte; x \<noteq> slot; sameRegionAs (cteCap cte) cap' \<rbrakk>
              \<Longrightarrow> sameRegionAs (cteCap cte) cap" apply (frule(2) Fin4) apply (clarsimp simp: sameRegionAs_def3 capR) apply (clarsimp simp: isCap_simps) done have is_chunk:
    "\<And>x cap n p p'. \<lbrakk> is_chunk m cap p p'; m x = Some (CTE cap n); x \<noteq> slot \<rbrakk> \<Longrightarrow>
                        is_chunk ?m' cap p p'" apply (simp add: is_chunk_def split del: if_split) apply (erule allEI) apply (clarsimp simp: slot) apply (frule(1) Fin3, simp) apply (clarsimp simp: sameRegionAs_def3 capR) apply (clarsimp simp: isCap_simps) done have not_chunk: "\<And>p. \<lbrakk> m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot \<rbrakk> \<Longrightarrow> \<not> is_chunk m cap slot p" apply (simp add: is_chunk_def) apply (rule_tac x=p in exI) apply clarsimp apply (frule(1) Fin1) apply simp done show ?thesis using chunked apply (simp add: mdb_chunked_def split del: if_split) apply (erule allEI, erule allEI) apply (clarsimp split del: if_split) apply (clarsimp simp: slot split: if_split_asm) apply (frule(1) Fin2[OF _ not_sym], simp) apply (frule(1) sameRegionAs, clarsimp+) apply (simp add: not_chunk is_chunk) apply (simp add: is_chunk) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (state)
goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (state)
this:
m(slot \<mapsto> CTE ?cap node) \<turnstile> ?p \<leadsto>\<^sup>+ ?p' = m \<turnstile> ?p \<leadsto>\<^sup>+ ?p'

goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (state)
this:
m(slot \<mapsto> CTE ?cap node) \<turnstile> ?p \<leadsto>\<^sup>* ?p' = m \<turnstile> ?p \<leadsto>\<^sup>* ?p'

goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m x = Some cte; x \<noteq> slot; global.sameRegionAs (cteCap cte) cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap cte) cap proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m x = Some cte; x \<noteq> slot; global.sameRegionAs (cteCap cte) cap'; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap cte) cap proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>m x = Some cte; x \<noteq> slot; isUntypedCap (cteCap cte); isIRQControlCap (cteCap cte); isIRQHandlerCap cap'; capRange cap' = {} \<or> \<not> capRange cap' \<subseteq> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> isIRQHandlerCap cap proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?x = Some ?cte; ?x \<noteq> slot; global.sameRegionAs (cteCap ?cte) cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap ?cte) cap

goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (prove)
goal (1 subgoal):
 1. \<And>x cap n p p'. \<lbrakk>is_chunk m cap p p'; m x = Some (CTE cap n); x \<noteq> slot\<rbrakk> \<Longrightarrow> is_chunk (m(slot \<mapsto> CTE cap' node)) cap p p' proof (prove)
goal (1 subgoal):
 1. \<And>x cap n p p'. \<lbrakk>\<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 x = Some (CTE cap n); x \<noteq> slot\<rbrakk> \<Longrightarrow> \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (if p'' = slot then Some (CTE cap' node) else m p'') = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>x cap n p p' p''. \<lbrakk>m x = Some (CTE cap n); x \<noteq> slot; m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (if p'' = slot then Some (CTE cap' node) else m p'') = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>x capa n p p'. \<lbrakk>m x = Some (CTE capa n); x \<noteq> slot; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> slot \<leadsto>\<^sup>* p'; global.sameRegionAs capa cap\<rbrakk> \<Longrightarrow> global.sameRegionAs capa cap' proof (prove)
goal (1 subgoal):
 1. \<And>x capa n p p'. \<lbrakk>m x = Some (CTE capa n); x \<noteq> slot; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> slot \<leadsto>\<^sup>* p'; global.sameRegionAs capa cap; isUntypedCap (cteCap (CTE capa n))\<rbrakk> \<Longrightarrow> global.sameRegionAs capa cap' proof (prove)
goal (1 subgoal):
 1. \<And>x capa n p p'. \<lbrakk>m x = Some (CTE capa n); x \<noteq> slot; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> slot \<leadsto>\<^sup>* p'; isUntypedCap capa; isIRQControlCap capa; isIRQHandlerCap cap; capRange cap' = {} \<or> \<not> capRange cap' \<subseteq> capRange capa\<rbrakk> \<Longrightarrow> isIRQHandlerCap cap' proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>is_chunk m ?cap ?p ?p'; m ?x = Some (CTE ?cap ?n); ?x \<noteq> slot\<rbrakk> \<Longrightarrow> is_chunk (m(slot \<mapsto> CTE cap' node)) ?cap ?p ?p'

goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<not> is_chunk m cap slot p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p''. m \<turnstile> slot \<leadsto>\<^sup>+ p'' \<and> m \<turnstile> p'' \<leadsto>\<^sup>* p \<and> (\<forall>cap''. (\<forall>n''. m p'' \<noteq> Some (CTE cap'' n'')) \<or> \<not> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto>\<^sup>+ p \<and> m \<turnstile> p \<leadsto>\<^sup>* p \<and> (\<forall>cap''. (\<forall>n''. m p \<noteq> Some (CTE cap'' n'')) \<or> \<not> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>p cap'' n''. \<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot; global.sameRegionAs cap cap''; m p = Some (CTE cap'' n'')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p cap'' n''. \<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ p; p \<noteq> slot; global.sameRegionAs cap cap''; m p = Some (CTE cap'' n''); \<not> global.sameRegionAs cap (cteCap (CTE cap'' n''))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m \<turnstile> slot \<leadsto>\<^sup>+ ?p; ?p \<noteq> slot\<rbrakk> \<Longrightarrow> \<not> is_chunk m cap slot ?p

goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (prove)
goal (1 subgoal):
 1. mdb_chunked (m(slot \<mapsto> CTE cap' node)) proof (prove)
using this:
mdb_chunked m

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

goal:
No subgoals!