theory CSpace1_R

lemma subtree_Null_update:
  assumes "no_0 m" "valid_dlist m"
  assumes null: "m p = Some (CTE NullCap node)"
  assumes node: "mdbPrev node = 0"
  assumes init: "mdbNext (cteMDBNode cte) = 0"
  shows "m \<turnstile> c \<rightarrow> c' = m (p \<mapsto> cte) \<turnstile> c \<rightarrow> c'" proof assume "m \<turnstile> c \<rightarrow> c'" thus "m (p \<mapsto> cte) \<turnstile> c \<rightarrow> c'" using null init proof induct case direct_parent thus ?case apply - apply (rule subtree.direct_parent) apply (clarsimp simp add: mdb_next_unfold parentOf_def) apply assumption apply (simp add: parentOf_def) apply (rule conjI) apply clarsimp apply clarsimp done next case (trans_parent y z) have "m \<turnstile> c \<rightarrow> y" "m \<turnstile> y \<leadsto> z" "z \<noteq> 0" "m \<turnstile> c parentOf z" by fact+ with trans_parent.prems show ?case apply - apply (rule subtree.trans_parent) apply (erule (1) trans_parent.hyps) apply (clarsimp simp: mdb_next_unfold parentOf_def) apply (drule (1) subtree_not_Null) apply simp apply assumption apply (fastforce simp: parentOf_def) done qed next assume m: "m (p \<mapsto> cte) \<turnstile> c \<rightarrow> c'" thus "m \<turnstile> c \<rightarrow> c'" using assms m proof induct case (direct_parent x) thus ?case apply - apply (cases "c=p") apply (clarsimp simp: mdb_next_unfold) apply (rule subtree.direct_parent) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (cases "p\<noteq>x") apply (clarsimp simp: parentOf_def  split: if_split_asm) apply clarsimp apply (clarsimp simp: mdb_next_unfold) apply (case_tac z) apply clarsimp apply (clarsimp simp: no_0_def valid_dlist_def Let_def) apply (erule_tac x=c in allE) apply clarsimp done next case (trans_parent x y) have "m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x" "m(p \<mapsto> cte) \<turnstile> x \<leadsto> y"
         "y \<noteq> 0" "m(p \<mapsto> cte) \<turnstile> c parentOf y" by fact+ with trans_parent.prems show ?case apply - apply (cases "p=x") apply clarsimp apply (clarsimp simp: mdb_next_unfold) apply (frule (5) trans_parent.hyps) apply (rule subtree.trans_parent) apply assumption apply (clarsimp simp: mdb_next_unfold) apply assumption apply (clarsimp simp: parentOf_def simp del: fun_upd_apply) apply (cases "p=y") apply clarsimp apply (clarsimp simp: mdb_next_unfold) apply (clarsimp simp: valid_dlist_def Let_def) apply (erule_tac x=x in allE) apply (clarsimp simp: no_0_def) apply (case_tac "p\<noteq>c") apply clarsimp apply clarsimp apply (erule (1) Null_not_subtree) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' = m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' proof (state)
goal (2 subgoals):
 1. m \<turnstile> c \<rightarrow> c' \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'
 2. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' \<Longrightarrow> m \<turnstile> c \<rightarrow> c' proof (state)
this:
m \<turnstile> c \<rightarrow> c'

goal (2 subgoals):
 1. m \<turnstile> c \<rightarrow> c' \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'
 2. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' \<Longrightarrow> m \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m \<turnstile> c \<rightarrow> c'
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<leadsto> c'_
c'_ \<noteq> 0
m \<turnstile> c parentOf c'_
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> c parentOf c'; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> c \<leadsto> c'_
c'_ \<noteq> 0
m \<turnstile> c parentOf c'_
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<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 p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<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 p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'_
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; m \<turnstile> c parentOf c'_; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> c'_ \<noteq> 0
 3. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; m \<turnstile> c parentOf c'_; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<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 p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> c'_ \<noteq> 0
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; m \<turnstile> c parentOf c'_; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<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 p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf c'_ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; \<exists>cte' cte. m c'_ = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> (c = p \<longrightarrow> (c'_ = p \<longrightarrow> isMDBParentOf cte cte) \<and> (c'_ \<noteq> p \<longrightarrow> (\<exists>ctea. m c'_ = Some ctea \<and> isMDBParentOf cte ctea))) \<and> (c \<noteq> p \<longrightarrow> c'_ = p \<longrightarrow> (\<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' cte)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; \<exists>cte' cte. m c'_ = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> c = p \<longrightarrow> (c'_ = p \<longrightarrow> isMDBParentOf cte cte) \<and> (c'_ \<noteq> p \<longrightarrow> (\<exists>ctea. m c'_ = Some ctea \<and> isMDBParentOf cte ctea))
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; \<exists>cte' cte. m c'_ = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> c \<noteq> p \<longrightarrow> c'_ = p \<longrightarrow> (\<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'_; c'_ \<noteq> 0; \<exists>cte' cte. m c'_ = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> c \<noteq> p \<longrightarrow> c'_ = p \<longrightarrow> (\<exists>cte'. m c = Some cte' \<and> isMDBParentOf cte' cte) proof (prove)
goal:
No subgoals! proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'_

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (state)
this:
m \<turnstile> c \<rightarrow> y
\<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y
m \<turnstile> y \<leadsto> z
z \<noteq> 0
m \<turnstile> c parentOf z
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. (m \<turnstile> c \<rightarrow> y &&& m \<turnstile> y \<leadsto> z) &&& z \<noteq> 0 &&& m \<turnstile> c parentOf z proof (state)
this:
m \<turnstile> c \<rightarrow> y
m \<turnstile> y \<leadsto> z
z \<noteq> 0
m \<turnstile> c parentOf z

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> c \<rightarrow> c'; \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> c parentOf c''; m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'' proof (chain)
picking this:
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0
m \<turnstile> c \<rightarrow> y
m \<turnstile> y \<leadsto> z
z \<noteq> 0
m \<turnstile> c parentOf z proof (prove)
using this:
m p = Some (CTE capability.NullCap node)
mdbNext (cteMDBNode cte) = 0
m \<turnstile> c \<rightarrow> y
m \<turnstile> y \<leadsto> z
z \<noteq> 0
m \<turnstile> c parentOf z

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> z proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c \<rightarrow> ?c'6
 2. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> ?c'6 \<leadsto> z
 3. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> z \<noteq> 0
 4. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> y \<leadsto> z
 2. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> z \<noteq> 0
 3. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal (3 subgoals):
 1. \<And>cte' ctea. \<lbrakk>mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> p; mdbNext node \<noteq> 0; m p = Some (CTE capability.NullCap node); z = mdbNext node; m (mdbNext node) = Some ctea; m c = Some cte'; isMDBParentOf cte' ctea; y = p\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> z \<noteq> 0
 3. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal (3 subgoals):
 1. \<And>cte' ctea. \<lbrakk>mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> p; mdbNext node \<noteq> 0; z = mdbNext node; m (mdbNext node) = Some ctea; m c = Some cte'; isMDBParentOf cte' ctea; y = p; False\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> z \<noteq> 0
 3. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> z \<noteq> 0
 2. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.NullCap node); mdbNext (cteMDBNode cte) = 0; m \<turnstile> c \<rightarrow> y; m \<turnstile> y \<leadsto> z; z \<noteq> 0; m \<turnstile> c parentOf z\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> c parentOf z proof (prove)
goal:
No subgoals! proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> z

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

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

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c' \<Longrightarrow> m \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> c' proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c'; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<leadsto> x
x \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf x
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c'; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> c \<leadsto> x
x \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf x
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c = p\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x
 2. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> x
 2. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> x \<noteq> 0
 3. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> x \<noteq> 0
 2. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p; p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x
 2. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p; \<not> p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; c \<noteq> p; \<not> p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(x \<mapsto> cte) \<turnstile> c \<leadsto> x; x \<noteq> 0; m(x \<mapsto> cte) \<turnstile> c parentOf x; no_0 m; valid_dlist m; m x = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = x then Some cte else m a) \<turnstile> c \<rightarrow> x; c \<noteq> x; p = x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf x proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; m(mdbNext (cteMDBNode z) \<mapsto> cte) \<turnstile> c parentOf mdbNext (cteMDBNode z); no_0 m; valid_dlist m; m (mdbNext (cteMDBNode z)) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext (cteMDBNode z) then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext (cteMDBNode z); c \<noteq> mdbNext (cteMDBNode z); p = mdbNext (cteMDBNode z); m c = Some z; x = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; m(mdbNext (cteMDBNode z) \<mapsto> cte) \<turnstile> c parentOf mdbNext (cteMDBNode z); no_0 m; valid_dlist m; m (mdbNext (cteMDBNode z)) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext (cteMDBNode z) then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext (cteMDBNode z); c \<noteq> mdbNext (cteMDBNode z); p = mdbNext (cteMDBNode z); m c = Some z; x = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext x2 \<noteq> 0; m(mdbNext x2 \<mapsto> cte) \<turnstile> c parentOf mdbNext x2; no_0 m; valid_dlist m; m (mdbNext x2) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext x2 then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext x2; c \<noteq> mdbNext x2; p = mdbNext x2; m c = Some (CTE x1 x2); x = mdbNext x2\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf mdbNext x2 proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext x2 \<noteq> 0; m(mdbNext x2 \<mapsto> cte) \<turnstile> c parentOf mdbNext x2; m 0 = None; \<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m (mdbNext x2) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext x2 then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext x2; c \<noteq> mdbNext x2; p = mdbNext x2; m c = Some (CTE x1 x2); x = mdbNext x2\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf mdbNext x2 proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext x2 \<noteq> 0; m(mdbNext x2 \<mapsto> cte) \<turnstile> c parentOf mdbNext x2; m 0 = None; m (mdbNext x2) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext x2 then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext x2; c \<noteq> mdbNext x2; p = mdbNext x2; m c = Some (CTE x1 x2); x = mdbNext x2; \<forall>cte. m c = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = c)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = c))\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf mdbNext x2 proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<rightarrow> x

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x
\<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> x
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
y \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf y
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. (m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x &&& m(p \<mapsto> cte) \<turnstile> x \<leadsto> y) &&& y \<noteq> 0 &&& m(p \<mapsto> cte) \<turnstile> c parentOf y proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
y \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf y

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'; \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'; m(p \<mapsto> cte) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf c''; no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> c''\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> c'' proof (chain)
picking this:
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
y \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf y proof (prove)
using this:
no_0 m
valid_dlist m
m p = Some (CTE capability.NullCap node)
mdbPrev node = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y
m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
y \<noteq> 0
m(p \<mapsto> cte) \<turnstile> c parentOf y

goal (1 subgoal):
 1. m \<turnstile> c \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p = x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y
 2. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m; m x = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = x then Some cte else m a) \<turnstile> c \<rightarrow> y; m(x \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(x \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(x \<mapsto> cte) \<turnstile> c parentOf y; p = x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y
 2. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> y proof (prove)
goal (4 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c \<rightarrow> ?c'20
 2. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> ?c'20 \<leadsto> y
 3. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> y \<noteq> 0
 4. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto> y
 2. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> y \<noteq> 0
 3. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> y \<noteq> 0
 2. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; m(p \<mapsto> cte) \<turnstile> c parentOf y; p \<noteq> x; m \<turnstile> c \<rightarrow> x\<rbrakk> \<Longrightarrow> m \<turnstile> c parentOf y proof (prove)
goal (1 subgoal):
 1. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p = y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>no_0 m; valid_dlist m; m y = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = y then Some cte else m a) \<turnstile> c \<rightarrow> y; m(y \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(y \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; y \<noteq> x; m \<turnstile> c \<rightarrow> x; (if c = y then Some cte else m c) = Some cte'; isMDBParentOf cte' cte; p = y\<rbrakk> \<Longrightarrow> False
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' z. \<lbrakk>no_0 m; valid_dlist m; m (mdbNext (cteMDBNode z)) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext (cteMDBNode z) then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext (cteMDBNode z); m(mdbNext (cteMDBNode z) \<mapsto> cte) \<turnstile> c \<rightarrow> x; mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode z) \<noteq> x; m \<turnstile> c \<rightarrow> x; (if c = mdbNext (cteMDBNode z) then Some cte else m c) = Some cte'; isMDBParentOf cte' cte; p = mdbNext (cteMDBNode z); m x = Some z; y = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' z. \<lbrakk>no_0 m; \<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m (mdbNext (cteMDBNode z)) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext (cteMDBNode z) then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext (cteMDBNode z); m(mdbNext (cteMDBNode z) \<mapsto> cte) \<turnstile> c \<rightarrow> x; mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode z) \<noteq> x; m \<turnstile> c \<rightarrow> x; (if c = mdbNext (cteMDBNode z) then Some cte else m c) = Some cte'; isMDBParentOf cte' cte; p = mdbNext (cteMDBNode z); m x = Some z; y = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' z. \<lbrakk>no_0 m; m (mdbNext (cteMDBNode z)) = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = mdbNext (cteMDBNode z) then Some cte else m a) \<turnstile> c \<rightarrow> mdbNext (cteMDBNode z); m(mdbNext (cteMDBNode z) \<mapsto> cte) \<turnstile> c \<rightarrow> x; mdbNext (cteMDBNode z) \<noteq> 0; mdbNext (cteMDBNode z) \<noteq> x; m \<turnstile> c \<rightarrow> x; (if c = mdbNext (cteMDBNode z) then Some cte else m c) = Some cte'; isMDBParentOf cte' cte; p = mdbNext (cteMDBNode z); m x = Some z; y = mdbNext (cteMDBNode z); \<forall>cte. m x = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = x)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = x))\<rbrakk> \<Longrightarrow> False
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y; p \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y; \<not> p \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' ctea. \<lbrakk>no_0 m; valid_dlist m; m p = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> y; m(p \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; p \<noteq> x; m \<turnstile> c \<rightarrow> x; (m(p \<mapsto> cte)) y = Some ctea; (m(p \<mapsto> cte)) c = Some cte'; isMDBParentOf cte' ctea; p \<noteq> y; \<not> p \<noteq> c\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m y = Some cte \<and> m c = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>no_0 m; valid_dlist m; m c = Some (CTE capability.NullCap node); mdbPrev node = 0; mdbNext (cteMDBNode cte) = 0; (\<lambda>a. if a = c then Some cte else m a) \<turnstile> c \<rightarrow> y; m(c \<mapsto> cte) \<turnstile> c \<rightarrow> x; m(c \<mapsto> cte) \<turnstile> x \<leadsto> y; y \<noteq> 0; c \<noteq> x; m \<turnstile> c \<rightarrow> x; m y = Some ctea; isMDBParentOf cte ctea; c \<noteq> y; p = c\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<rightarrow> y

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

goal:
No subgoals!