theory CSpace1_R

lemma descendants_of_update_ztc:
  assumes c: "\<And>x. \<lbrakk> m \<turnstile> x \<rightarrow> slot; \<not> P \<rbrakk> \<Longrightarrow>
                  \<exists>cte'. m x = Some cte'
                    \<and> capMasterCap (cteCap cte') \<noteq> capMasterCap (cteCap cte)
                    \<and> sameRegionAs (cteCap cte') (cteCap cte)"
  assumes m: "m slot = Some cte"
  assumes z: "isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap"
  defines "cap' \<equiv> cteCap cte"
  assumes F: "\<And>x cte'. \<lbrakk> m x = Some cte'; x \<noteq> slot; P \<rbrakk>
               \<Longrightarrow> isUntypedCap (cteCap cte') \<or> capClass (cteCap cte') \<noteq> PhysicalClass
                    \<or> capUntypedPtr (cteCap cte') \<noteq> capUntypedPtr cap'"
  assumes pu: "capRange cap' = capRange cap \<and> capUntypedPtr cap' = capUntypedPtr cap"
  assumes a: "capAligned cap'"
  assumes t: "isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'"
  assumes n: "no_loops m"
  defines "m' \<equiv> m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte)"
  shows "((c \<noteq> slot \<or> P) \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m')
           \<and> (P \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m)" proof (simp add: descendants_of'_def subset_iff,
       simp only: all_simps(6)[symmetric], intro conjI allI) note isMDBParentOf_CTE[simp] have utp: "capUntypedPtr cap' \<in> capRange cap'" using t a by (auto elim!: capAligned_capUntypedPtr simp: isCap_simps) have ztc_parent: "\<And>cap cap'. isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
                            \<Longrightarrow> sameRegionAs cap cap'
                            \<Longrightarrow> capUntypedPtr cap = capUntypedPtr cap'
                                 \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap'" by (auto simp: isCap_simps sameRegionAs_def3) have ztc_child: "\<And>cap cap'. isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
                            \<Longrightarrow> sameRegionAs cap' cap
                            \<Longrightarrow> capClass cap' = PhysicalClass \<and>
                                  (isUntypedCap cap' \<or> capUntypedPtr cap' = capUntypedPtr cap)" by (auto simp: isCap_simps sameRegionAs_def3) have notparent: "\<And>x cte'. \<lbrakk> m x = Some cte'; x \<noteq> slot; P \<rbrakk>
                               \<Longrightarrow> \<not> isMDBParentOf cte cte'" using t utp apply clarsimp apply (drule_tac cte'=cte' in F, simp+) apply (simp add: cap'_def) apply (cases cte, case_tac cte', clarsimp) apply (frule(1) ztc_parent, clarsimp) done have notparent2: "\<And>x cte'. \<lbrakk> m x = Some cte'; x \<noteq> slot; P \<rbrakk>
                               \<Longrightarrow> \<not> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte'" using z utp apply clarsimp apply (drule_tac cte'=cte' in F, simp+) apply (cases cte, case_tac cte', clarsimp) apply (frule(1) ztc_parent) apply (clarsimp simp: pu) done fix x { assume cx: "m \<turnstile> c \<rightarrow> x" and cP: "c \<noteq> slot \<or> P" hence c_neq_x [simp]: "c \<noteq> x" by (clarsimp simp: n no_loops_no_subtree) from cx c_neq_x cP m have s_neq_c [simp]: "c \<noteq> slot" apply (clarsimp simp del: c_neq_x) apply (drule subtree_parent) apply (clarsimp simp: parentOf_def notparent) done have parent: "\<And>x cte'. \<lbrakk> m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot \<rbrakk>
                                \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)" using t z pu apply - apply (cases P) apply (frule(2) F) apply (clarsimp simp: cap'_def) apply (case_tac cte') apply (rename_tac capability mdbnode) apply (case_tac cte) apply clarsimp apply (frule(1) ztc_child) apply (case_tac "isUntypedCap capability") apply (simp add: isCap_simps) apply (clarsimp simp: sameRegionAs_def3 isCap_simps) apply simp apply (frule(1) c, clarsimp) apply (clarsimp simp: cap'_def) apply (case_tac cte') apply (case_tac cte) apply clarsimp apply (erule sameRegionAsE) apply (clarsimp simp: sameRegionAs_def3 isCap_simps)+ done from cx have "m' \<turnstile> c \<rightarrow> x" proof induct case (direct_parent c') hence "m \<turnstile> c \<rightarrow> c'" by (rule subtree.direct_parent) with direct_parent m show ?case apply - apply (rule subtree.direct_parent) apply (clarsimp simp add: mdb_next_unfold m'_def m) apply assumption apply (clarsimp simp: parentOf_def) apply (clarsimp simp add: m'_def) apply (erule(2) parent) apply simp done next case (trans_parent c' c'') moreover from trans_parent have "m \<turnstile> c \<rightarrow> c''" by - (rule subtree.trans_parent) ultimately show ?case using  z m pu t apply - apply (erule subtree.trans_parent) apply (clarsimp simp: mdb_next_unfold m'_def m) apply assumption apply (clarsimp simp: parentOf_def m'_def) apply (erule(2) parent) apply simp done qed } thus "(c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> x \<longrightarrow> m' \<turnstile> c \<rightarrow> x" by blast { assume subcx: "m' \<turnstile> c \<rightarrow> x" and P: "P" have mdb_next_eq: "\<And>x y. m' \<turnstile> x \<leadsto> y = m \<turnstile> x \<leadsto> y" by (simp add: mdb_next_unfold m'_def m) have mdb_next_eq_trans: "\<And>x y. m' \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y" apply (rule arg_cong[where f="\<lambda>S. v \<in> S\<^sup>+" for v]) apply (simp add: set_eq_iff mdb_next_eq) done have subtree_neq: "\<And>x y. m' \<turnstile> x \<rightarrow> y \<Longrightarrow> x \<noteq> y" apply clarsimp apply (drule subtree_mdb_next) apply (clarsimp simp: mdb_next_eq_trans n no_loops_trancl_simp) done have parent2: "\<And>x cte'. \<lbrakk> m x = Some cte'; isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte);
                                         x \<noteq> slot \<rbrakk>
                                \<Longrightarrow> isMDBParentOf cte' cte" using t z pu P apply (drule_tac cte'=cte' in F, simp, simp) apply (simp add: cap'_def) apply (cases cte) apply (case_tac cte') apply (rename_tac cap' node') apply (clarsimp) apply (frule(1) ztc_child) apply (case_tac "isUntypedCap cap'") apply (simp add:isCap_simps) apply (clarsimp simp: isCap_simps sameRegionAs_def3) apply clarsimp done from subcx have "m \<turnstile> c \<rightarrow> x" proof induct case (direct_parent c') thus ?case using subtree_neq [OF subtree.direct_parent [OF direct_parent(1-3)]] apply - apply (rule subtree.direct_parent) apply (clarsimp simp: mdb_next_unfold m'_def m split: if_split_asm) apply assumption apply (insert z m t pu) apply (simp add: cap'_def) apply (simp add: m'_def parentOf_def split: if_split_asm) apply (clarsimp simp: parent2) apply (clarsimp simp add: notparent2 [OF _ _ P]) done next case (trans_parent c' c'') thus ?case using subtree_neq [OF subtree.trans_parent [OF trans_parent(1, 3-5)]] apply - apply (erule subtree.trans_parent) apply (clarsimp simp: mdb_next_unfold m'_def m split: if_split_asm) apply assumption apply (insert z m t pu) apply (simp add: cap'_def) apply (simp add: m'_def parentOf_def split: if_split_asm) apply (clarsimp simp: parent2) apply (clarsimp simp: notparent2 [OF _ _ P]) done qed } thus "P \<longrightarrow> m' \<turnstile> c \<rightarrow> x \<longrightarrow> m \<turnstile> c \<rightarrow> x" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (c \<noteq> slot \<or> P \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m') \<and> (P \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m) proof (state)
goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
isMDBParentOf (CTE ?cap ?node) ?cte = (\<exists>cap' node'. ?cte = CTE cap' node' \<and> global.sameRegionAs ?cap cap' \<and> mdbRevocable ?node \<and> (capBadge ?cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'))

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. global.capUntypedPtr cap' \<in> capRange cap' proof (prove)
using this:
isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'
capAligned cap'

goal (1 subgoal):
 1. global.capUntypedPtr cap' \<in> capRange cap' proof (state)
this:
global.capUntypedPtr cap' \<in> capRange cap'

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>cap cap'. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap = global.capUntypedPtr cap' \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' proof (state)
this:
\<lbrakk>isZombie ?cap \<or> isCNodeCap ?cap \<or> isThreadCap ?cap; global.sameRegionAs ?cap ?cap'\<rbrakk> \<Longrightarrow> global.capUntypedPtr ?cap = global.capUntypedPtr ?cap' \<and> capClass ?cap' = PhysicalClass \<and> \<not> isUntypedCap ?cap'

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>cap cap'. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.sameRegionAs cap' cap\<rbrakk> \<Longrightarrow> capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap) proof (state)
this:
\<lbrakk>isZombie ?cap \<or> isCNodeCap ?cap \<or> isThreadCap ?cap; global.sameRegionAs ?cap' ?cap\<rbrakk> \<Longrightarrow> capClass ?cap' = PhysicalClass \<and> (isUntypedCap ?cap' \<or> global.capUntypedPtr ?cap' = global.capUntypedPtr ?cap)

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte cte' proof (prove)
using this:
isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'
global.capUntypedPtr cap' \<in> capRange cap'

goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; global.capUntypedPtr cap' \<in> capRange cap'; isMDBParentOf cte cte'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>x \<noteq> slot; P; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; global.capUntypedPtr cap' \<in> capRange cap'; isMDBParentOf cte cte'; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>x \<noteq> slot; P; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); global.capUntypedPtr (cteCap cte) \<in> capRange (cteCap cte); isMDBParentOf cte cte'; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 x1a x2a. \<lbrakk>x \<noteq> slot; P; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; global.capUntypedPtr x1 \<in> capRange x1; capClass x1a = PhysicalClass \<longrightarrow> isUntypedCap x1a \<or> global.capUntypedPtr x1a \<noteq> global.capUntypedPtr x1; cte = CTE x1 x2; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?x = Some ?cte'; ?x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte ?cte'

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte' proof (prove)
using this:
isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
global.capUntypedPtr cap' \<in> capRange cap'

goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte' proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; x \<noteq> slot; P; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.capUntypedPtr cap' \<in> capRange cap'; isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>x \<noteq> slot; P; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.capUntypedPtr cap' \<in> capRange cap'; isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte'; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 x1a x2a. \<lbrakk>x \<noteq> slot; P; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.capUntypedPtr cap' \<in> capRange cap'; capClass x1a = PhysicalClass \<longrightarrow> isUntypedCap x1a \<or> global.capUntypedPtr x1a \<noteq> global.capUntypedPtr cap'; cte = CTE x1 x2; global.sameRegionAs cap x1a; mdbRevocable x2; (capBadge cap, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 x1a x2a. \<lbrakk>x \<noteq> slot; P; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; global.capUntypedPtr cap' \<in> capRange cap'; capClass x1a = PhysicalClass \<longrightarrow> isUntypedCap x1a \<or> global.capUntypedPtr x1a \<noteq> global.capUntypedPtr cap'; cte = CTE x1 x2; global.sameRegionAs cap x1a; mdbRevocable x2; (capBadge cap, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); global.capUntypedPtr cap = global.capUntypedPtr x1a \<and> capClass x1a = PhysicalClass \<and> \<not> isUntypedCap x1a\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?x = Some ?cte'; ?x \<noteq> slot; P\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) ?cte'

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
m \<turnstile> c \<rightarrow> x
c \<noteq> slot \<or> P

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
using this:
m \<turnstile> c \<rightarrow> x
c \<noteq> slot \<or> P

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

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (chain)
picking this:
m \<turnstile> c \<rightarrow> x
c \<noteq> x
c \<noteq> slot \<or> P
m slot = Some cte proof (prove)
using this:
m \<turnstile> c \<rightarrow> x
c \<noteq> x
c \<noteq> slot \<or> P
m slot = Some cte

goal (1 subgoal):
 1. c \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> slot \<rightarrow> x; slot \<noteq> x; P; m slot = Some cte; c = slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<noteq> x; P; m slot = Some cte; c = slot; m \<turnstile> slot parentOf x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
c \<noteq> slot

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
using this:
isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'
isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap

goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; P; isUntypedCap (cteCap cte') \<or> capClass (cteCap cte') \<noteq> PhysicalClass \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte' x1 x2. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte' capability mdbnode. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; cte' = CTE capability mdbnode\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x cte' capability mdbnode x1 x2. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; cte' = CTE capability mdbnode; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass \<and> (isUntypedCap capability \<or> global.capUntypedPtr capability = global.capUntypedPtr x1)\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (3 subgoals):
 1. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass \<and> (isUntypedCap capability \<or> global.capUntypedPtr capability = global.capUntypedPtr x1); isUntypedCap capability\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass \<and> (isUntypedCap capability \<or> global.capUntypedPtr capability = global.capUntypedPtr x1); \<not> isUntypedCap capability\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 3. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (3 subgoals):
 1. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; (\<exists>v0 v1 v2. x1 = capability.Zombie v0 v1 v2) \<or> (\<exists>v0 v1 v2 v3. x1 = capability.CNodeCap v0 v1 v2 v3) \<or> (\<exists>v0. x1 = capability.ThreadCap v0); (\<exists>v0 v1 v2. cap = capability.Zombie v0 v1 v2) \<or> (\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<or> (\<exists>v0. cap = capability.ThreadCap v0); P; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass; \<exists>d v0 v1 f. capability = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass \<and> (isUntypedCap capability \<or> global.capUntypedPtr capability = global.capUntypedPtr x1); \<not> isUntypedCap capability\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 3. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (2 subgoals):
 1. \<And>x capability mdbnode x1 x2. \<lbrakk>m x = Some (CTE capability mdbnode); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass capability = PhysicalClass \<longrightarrow> isUntypedCap capability \<or> global.capUntypedPtr capability \<noteq> global.capUntypedPtr cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs capability x1; mdbRevocable mdbnode; (capBadge capability, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); capClass capability = PhysicalClass \<and> (isUntypedCap capability \<or> global.capUntypedPtr capability = global.capUntypedPtr x1); \<not> isUntypedCap capability\<rbrakk> \<Longrightarrow> global.sameRegionAs capability cap \<and> (capBadge capability, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; \<not> P\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange cap' = capRange cap; global.capUntypedPtr cap' = global.capUntypedPtr cap; capMasterCap (cteCap cte') \<noteq> capMasterCap (cteCap cte); global.sameRegionAs (cteCap cte') (cteCap cte)\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; capMasterCap (cteCap cte') \<noteq> capMasterCap (cteCap cte); global.sameRegionAs (cteCap cte') (cteCap cte)\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte' x1 x2. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; capMasterCap (cteCap cte') \<noteq> capMasterCap (cteCap cte); global.sameRegionAs (cteCap cte') (cteCap cte); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte' x1 x2 x1a x2a. \<lbrakk>m x = Some cte'; isMDBParentOf cte' cte; m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; capMasterCap (cteCap cte') \<noteq> capMasterCap (cteCap cte); global.sameRegionAs (cteCap cte') (cteCap cte); cte' = CTE x1 x2; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 x1a x2a. \<lbrakk>m x = Some (CTE x1 x2); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1a \<or> isCNodeCap x1a \<or> isThreadCap x1a; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange x1a = capRange cap; global.capUntypedPtr x1a = global.capUntypedPtr cap; capMasterCap x1 \<noteq> capMasterCap x1a; cte = CTE x1a x2a; global.sameRegionAs x1 x1a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2a) proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2 x1a x2a. \<lbrakk>m x = Some (CTE x1 x2); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1a \<or> isCNodeCap x1a \<or> isThreadCap x1a; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange x1a = capRange cap; global.capUntypedPtr x1a = global.capUntypedPtr cap; capMasterCap x1 \<noteq> capMasterCap x1a; cte = CTE x1a x2a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capMasterCap x1 = capMasterCap x1a; \<not> isNullCap x1; \<not> isZombie x1; \<not> isUntypedCap x1; \<not> isArchPageCap x1\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2a)
 2. \<And>x x1 x2 x1a x2a. \<lbrakk>m x = Some (CTE x1 x2); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1a \<or> isCNodeCap x1a \<or> isThreadCap x1a; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange x1a = capRange cap; global.capUntypedPtr x1a = global.capUntypedPtr cap; capMasterCap x1 \<noteq> capMasterCap x1a; cte = CTE x1a x2a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capRange x1a \<noteq> {}; capRange x1a \<subseteq> capRange x1; isUntypedCap x1\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2a)
 3. \<And>x x1 x2 x1a x2a. \<lbrakk>m x = Some (CTE x1 x2); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1a \<or> isCNodeCap x1a \<or> isThreadCap x1a; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange x1a = capRange cap; global.capUntypedPtr x1a = global.capUntypedPtr cap; capMasterCap x1 \<noteq> capMasterCap x1a; cte = CTE x1a x2a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); capRange x1a \<noteq> {}; capRange x1a \<subseteq> capRange x1; isArchPageCap x1; isArchPageCap x1a\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2a)
 4. \<And>x x1 x2 x1a x2a. \<lbrakk>m x = Some (CTE x1 x2); m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; isZombie x1a \<or> isCNodeCap x1a \<or> isThreadCap x1a; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; \<not> P; capRange x1a = capRange cap; global.capUntypedPtr x1a = global.capUntypedPtr cap; capMasterCap x1 \<noteq> capMasterCap x1a; cte = CTE x1a x2a; mdbRevocable x2; (capBadge x1, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2a); isIRQControlCap x1; isIRQHandlerCap x1a\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2a) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?x = Some ?cte'; isMDBParentOf ?cte' cte; m \<turnstile> ?x \<rightarrow> slot; ?x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf ?cte' (cteCap_update (\<lambda>_. cap) cte)

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (chain)
picking this:
m \<turnstile> c \<rightarrow> x proof (prove)
using this:
m \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. m' \<turnstile> c \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> c parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> c parentOf c'

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' proof (state)
this:
m \<turnstile> c \<rightarrow> c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (chain)
picking this:
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> c parentOf c'
m slot = Some cte
m \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> c parentOf c'
m slot = Some cte
m \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. m' \<turnstile> c \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<leadsto> c'
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m slot = Some cte; m \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c' proof (prove)
goal (1 subgoal):
 1. \<And>cte' ctea. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m slot = Some cte; m \<turnstile> c \<rightarrow> c'; m c' = Some ctea; m c = Some cte'; isMDBParentOf cte' ctea\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m' c' = Some cte \<and> m' c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m \<turnstile> c \<leadsto> slot; slot \<noteq> 0; m \<turnstile> c \<rightarrow> slot; m slot = Some cte; m c = Some cte'; isMDBParentOf cte' cte; c' = slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m \<turnstile> c \<leadsto> slot; slot \<noteq> 0; m \<turnstile> c \<rightarrow> slot; m slot = Some cte; isMDBParentOf cte' cte; c' = slot\<rbrakk> \<Longrightarrow> c \<noteq> slot proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (chain)
picking this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c'' proof (prove)
using this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<rightarrow> c''

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (chain)
picking this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''
m \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''
m \<turnstile> c \<rightarrow> c''

goal (1 subgoal):
 1. m' \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m \<turnstile> c parentOf c''
m \<turnstile> c \<rightarrow> c''
isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
m slot = Some cte
capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap
isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'

goal (1 subgoal):
 1. m' \<turnstile> c \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> m' \<turnstile> c' \<leadsto> c''
 2. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m \<turnstile> c \<rightarrow> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'\<rbrakk> \<Longrightarrow> m' \<turnstile> c parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> slot; slot \<noteq> 0; m \<turnstile> c \<rightarrow> slot; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; capRange cap' = capRange cap; global.capUntypedPtr cap' = global.capUntypedPtr cap; m slot = Some cte; m c = Some cte'; isMDBParentOf cte' cte; c'' = slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> slot; slot \<noteq> 0; m \<turnstile> c \<rightarrow> slot; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; capRange cap' = capRange cap; global.capUntypedPtr cap' = global.capUntypedPtr cap; m slot = Some cte; isMDBParentOf cte' cte; c'' = slot\<rbrakk> \<Longrightarrow> c \<noteq> slot proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> c \<rightarrow> c''

goal:
No subgoals! proof (state)
this:
m' \<turnstile> c \<rightarrow> x

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
\<lbrakk>m \<turnstile> c \<rightarrow> x; c \<noteq> slot \<or> P\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> x

goal (2 subgoals):
 1. \<And>t. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> t \<longrightarrow> m' \<turnstile> c \<rightarrow> t
 2. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
using this:
\<lbrakk>m \<turnstile> c \<rightarrow> x; c \<noteq> slot \<or> P\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. (c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> x \<longrightarrow> m' \<turnstile> c \<rightarrow> x proof (state)
this:
(c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> x \<longrightarrow> m' \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
(c = slot \<longrightarrow> P) \<longrightarrow> m \<turnstile> c \<rightarrow> x \<longrightarrow> m' \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
m' \<turnstile> c \<rightarrow> x
P

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x y. m' \<turnstile> x \<leadsto> y = m \<turnstile> x \<leadsto> y proof (state)
this:
m' \<turnstile> ?x \<leadsto> ?y = m \<turnstile> ?x \<leadsto> ?y

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x y. m' \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>x y. mdb_next_rel m' = mdb_next_rel m proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> ?x \<leadsto>\<^sup>+ ?y = m \<turnstile> ?x \<leadsto>\<^sup>+ ?y

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x y. m' \<turnstile> x \<rightarrow> y \<Longrightarrow> x \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>y. m' \<turnstile> y \<rightarrow> y \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. m' \<turnstile> y \<leadsto>\<^sup>+ y \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> ?x \<rightarrow> ?y \<Longrightarrow> ?x \<noteq> ?y

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
using this:
isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'
isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap
capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap
P

goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>m x = Some cte'; isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap; P; isUntypedCap (cteCap cte') \<or> capClass (cteCap cte') \<noteq> PhysicalClass \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte'. \<lbrakk>isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte' x1 x2. \<lbrakk>isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte' x1 x2 x1a x2a. \<lbrakk>isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x cte' x1 x2 cap' node'. \<lbrakk>isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte); x \<noteq> slot; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; P; capClass (cteCap cte') = PhysicalClass \<longrightarrow> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte') \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; cte' = CTE cap' node'\<rbrakk> \<Longrightarrow> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap); isUntypedCap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap); \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; (\<exists>v0 v1 v2. x1 = capability.Zombie v0 v1 v2) \<or> (\<exists>v0 v1 v2 v3. x1 = capability.CNodeCap v0 v1 v2 v3) \<or> (\<exists>v0. x1 = capability.ThreadCap v0); (\<exists>v0 v1 v2. cap = capability.Zombie v0 v1 v2) \<or> (\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<or> (\<exists>v0. cap = capability.ThreadCap v0); P; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass; \<exists>d v0 v1 f. cap' = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)
 2. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap); \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 cap' node'. \<lbrakk>x \<noteq> slot; isZombie x1 \<or> isCNodeCap x1 \<or> isThreadCap x1; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; P; capClass cap' = PhysicalClass \<longrightarrow> isUntypedCap cap' \<or> global.capUntypedPtr cap' \<noteq> global.capUntypedPtr cap; cte = CTE x1 x2; global.sameRegionAs cap' cap; capRange x1 = capRange cap; global.capUntypedPtr x1 = global.capUntypedPtr cap; mdbRevocable node'; (capBadge cap', capBadge cap) \<in> capBadge_ordering (mdbFirstBadged x2); capClass cap' = PhysicalClass \<and> (isUntypedCap cap' \<or> global.capUntypedPtr cap' = global.capUntypedPtr cap); \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' x1 \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>m ?x = Some ?cte'; isMDBParentOf ?cte' (cteCap_update (\<lambda>_. cap) cte); ?x \<noteq> slot\<rbrakk> \<Longrightarrow> isMDBParentOf ?cte' cte

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (chain)
picking this:
m' \<turnstile> c \<rightarrow> x proof (prove)
using this:
m' \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
this:
m' \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> c parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> c parentOf c'

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m' \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> c parentOf c'
c \<noteq> c'

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'
 2. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> c parentOf c'; c \<noteq> c'; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<noteq> slot; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> c \<leadsto> slot; slot \<noteq> 0; c' = slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; \<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)\<rbrakk> \<Longrightarrow> \<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' cte
 2. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; c = slot; \<exists>ctea. m c' = Some ctea \<and> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) ctea\<rbrakk> \<Longrightarrow> \<exists>ctea. m c' = Some ctea \<and> isMDBParentOf cte ctea proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; c = slot; \<exists>ctea. m c' = Some ctea \<and> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) ctea\<rbrakk> \<Longrightarrow> \<exists>ctea. m c' = Some ctea \<and> isMDBParentOf cte ctea proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
this:
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m' \<turnstile> c parentOf c''

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m' \<turnstile> c parentOf c''

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> c \<rightarrow> c'
m \<turnstile> c \<rightarrow> c'
m' \<turnstile> c' \<leadsto> c''
c'' \<noteq> 0
m' \<turnstile> c parentOf c''
c \<noteq> c''

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie cap' \<or> isCNodeCap cap' \<or> isThreadCap cap'; capRange cap' = capRange cap \<and> global.capUntypedPtr cap' = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> c \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> c parentOf c''; c \<noteq> c''; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); capRange (cteCap cte) = capRange cap \<and> global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<noteq> slot; isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> c \<rightarrow> c'; m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> c' \<leadsto> slot; slot \<noteq> 0; c'' = slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; \<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' (cteCap_update (\<lambda>_. cap) cte)\<rbrakk> \<Longrightarrow> \<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' cte
 2. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> slot \<rightarrow> c'; m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; c'' \<noteq> slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; c = slot; \<exists>ctea. m c'' = Some ctea \<and> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) ctea\<rbrakk> \<Longrightarrow> \<exists>ctea. m c'' = Some ctea \<and> isMDBParentOf cte ctea proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isZombie cap \<or> isCNodeCap cap \<or> isThreadCap cap; m slot = Some cte; isZombie (cteCap cte) \<or> isCNodeCap (cteCap cte) \<or> isThreadCap (cteCap cte); m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> slot \<rightarrow> c'; m(slot \<mapsto> cteCap_update (\<lambda>_. cap) cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; c'' \<noteq> slot; capRange (cteCap cte) = capRange cap; global.capUntypedPtr (cteCap cte) = global.capUntypedPtr cap; c = slot; \<exists>ctea. m c'' = Some ctea \<and> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) ctea\<rbrakk> \<Longrightarrow> \<exists>ctea. m c'' = Some ctea \<and> isMDBParentOf cte ctea proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<rightarrow> c''

goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (state)
this:
\<lbrakk>m' \<turnstile> c \<rightarrow> x; P\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. \<And>t. P \<longrightarrow> m' \<turnstile> c \<rightarrow> t \<longrightarrow> m \<turnstile> c \<rightarrow> t proof (prove)
using this:
\<lbrakk>m' \<turnstile> c \<rightarrow> x; P\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. P \<longrightarrow> m' \<turnstile> c \<rightarrow> x \<longrightarrow> m \<turnstile> c \<rightarrow> x proof (state)
this:
P \<longrightarrow> m' \<turnstile> c \<rightarrow> x \<longrightarrow> m \<turnstile> c \<rightarrow> x

goal:
No subgoals!