theory Untyped_R

lemma n'_prev_eq:
  notes if_cong[cong del] if_weak_cong[cong]
  shows "n' \<turnstile> p \<leftarrow> p' = (if p' = site then p = parent
                         else if p = site then m \<turnstile> parent \<leftarrow> p'
                         else if p = parent then p' = site
                         else m \<turnstile> p \<leftarrow> p')" using parent site site_prev apply (simp add: n'_def n mdb_prev_def new_parent_def new_site_def split del: if_split) apply (clarsimp simp add: modify_map_if cong: if_cong split del: if_split) apply (cases "p' = site", simp) apply (simp cong: if_cong split del: if_split) apply (cases "p' = parent") apply clarsimp apply (rule conjI, clarsimp simp: mdb_prev_def) apply (clarsimp simp: mdb_prev_def) apply (simp cong: if_cong split del: if_split) apply (cases "p = site") apply (simp add: parent_prev) apply (cases "mdbNext parent_node = p'") apply simp apply (rule iffI) prefer 2 apply clarsimp apply (erule dlistEn) apply simp apply clarsimp apply (case_tac cte') apply clarsimp apply clarsimp apply clarsimp apply (insert site_next)[1] apply (rule valid_dlistEp [OF dlist, where p=p'], assumption) apply clarsimp apply clarsimp apply (simp cong: if_cong split del: if_split) apply (cases "p = parent") apply clarsimp apply (insert site_next) apply (cases "mdbNext parent_node = p'", clarsimp) apply clarsimp apply (rule valid_dlistEp [OF dlist, where p=p'], assumption) apply clarsimp apply clarsimp apply simp apply (cases "mdbNext parent_node = p'") prefer 2 apply (clarsimp simp: mdb_prev_def) apply (rule iffI, clarsimp) apply clarsimp apply (case_tac z) apply simp apply (rule iffI) apply (clarsimp simp: mdb_prev_def) apply (drule sym [where t=p']) apply (simp add: parent_next_prev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leftarrow> p' = (if p' = site then p = parent else if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then p' = site else m \<turnstile> p \<leftarrow> p') proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)
mdbPrev site_node = 0

goal (1 subgoal):
 1. n' \<turnstile> p \<leftarrow> p' = (if p' = site then p = parent else if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then p' = site else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. modify_map (m(site \<mapsto> CTE c' (MDB (mdbNext parent_node) parent True True), parent \<mapsto> CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node))) (mdbNext parent_node) (cteMDBNode_update (mdbPrev_update (\<lambda>a. site))) p' = Some z \<and> p = mdbPrev (cteMDBNode z)) = (if p' = site then p = parent else if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then p' = site else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else if p' = site then Some (CTE c' (MDB site parent True True)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else if p' = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p' = site then p = parent else if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else if p' = site then Some (CTE c' (MDB site parent True True)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else if p' = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p' = site then p = parent else if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' = parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p')
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' = parent; p \<noteq> parent\<rbrakk> \<Longrightarrow> (p = site \<longrightarrow> \<not> m \<turnstile> parent \<leftarrow> parent) \<and> (p \<noteq> site \<longrightarrow> (p = mdbPrev parent_node) = m \<turnstile> p \<leftarrow> parent)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' = parent; p \<noteq> parent\<rbrakk> \<Longrightarrow> p \<noteq> site \<longrightarrow> (p = mdbPrev parent_node) = m \<turnstile> p \<leftarrow> parent
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. (if p' = parent then Some (CTE parent_cap (mdbNext_update (\<lambda>a. site) parent_node)) else m p') = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p')
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) = (p' \<noteq> 0)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext parent_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE parent_cap parent_node)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node; m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext parent_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 5. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<And>cte'. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node; m (mdbNext (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbPrev (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext parent_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<And>cte'. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node; m (mdbNext parent_node) = Some cte'; parent = mdbPrev (cteMDBNode cte')\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. cte' = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (4 subgoals):
 1. \<And>cte' x1 x2. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p = site; mdbNext parent_node \<noteq> 0; p' = mdbNext parent_node; m (mdbNext parent_node) = Some cte'; parent = mdbPrev (cteMDBNode cte'); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. cte' = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 4. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node = p'; \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p' \<noteq> 0
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = site; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> site = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> site = mdbPrev (cteMDBNode z))) = (p' = mdbNext parent_node \<and> p' \<noteq> 0)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev node) = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> mdbPrev node; p' \<noteq> parent; p = mdbPrev node; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); site = mdbPrev node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev node) = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> mdbPrev node; p' \<noteq> parent; p = mdbPrev node; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); site = mdbPrev node; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (3 subgoals):
 1. \<And>cap node. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev node) = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> mdbPrev node; p' \<noteq> parent; p = mdbPrev node; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); site = mdbPrev node; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE cap node)) \<noteq> 0
 2. \<And>cap node cte'. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev node) = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> mdbPrev node; p' \<noteq> parent; p = mdbPrev node; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); site = mdbPrev node; mdbNext site_node = 0; m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = p'\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cap node cte'. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev node) = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> mdbPrev node; p' \<noteq> parent; p = mdbPrev node; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); site = mdbPrev node; mdbNext site_node = 0; m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = p'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = site then m \<turnstile> parent \<leftarrow> p' else if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p')
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = parent\<rbrakk> \<Longrightarrow> (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z))
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z))
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p = parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<longrightarrow> parent \<noteq> mdbPrev (cteMDBNode z))
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cap node. \<lbrakk>m (mdbPrev node) = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> mdbPrev node; p = mdbPrev node; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); parent = mdbPrev node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (3 subgoals):
 1. \<And>cap node. \<lbrakk>m (mdbPrev node) = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> mdbPrev node; p = mdbPrev node; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); parent = mdbPrev node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE cap node)) \<noteq> 0
 2. \<And>cap node cte'. \<lbrakk>m (mdbPrev node) = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> mdbPrev node; p = mdbPrev node; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); parent = mdbPrev node; m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = p'\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cap node cte'. \<lbrakk>m (mdbPrev node) = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> mdbPrev node; p = mdbPrev node; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some (CTE cap node); parent = mdbPrev node; m (mdbPrev (cteMDBNode (CTE cap node))) = Some cte'; mdbNext (cteMDBNode cte') = p'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (if mdbNext parent_node = p' then \<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z else \<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (if p = parent then False else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p'
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p'
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (\<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z))
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; \<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; mdbPrev (cteMDBNode z) \<noteq> site; mdbPrev (cteMDBNode z) \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> za = CTE cap node) \<and> mdbPrev (cteMDBNode z) = mdbPrev (cteMDBNode za)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; mdbPrev (cteMDBNode z) \<noteq> site; mdbPrev (cteMDBNode z) \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node \<noteq> p'; m p' = Some z; p = mdbPrev (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> za = CTE cap node) \<and> mdbPrev (cteMDBNode z) = mdbPrev (cteMDBNode za)
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'\<rbrakk> \<Longrightarrow> (\<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))) = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'; \<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z))\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leftarrow> p'
 2. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'; m \<turnstile> p \<leftarrow> p'\<rbrakk> \<Longrightarrow> \<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; mdbNext parent_node = p'; m \<turnstile> p \<leftarrow> p'\<rbrakk> \<Longrightarrow> \<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; p' \<noteq> site; p' \<noteq> parent; p \<noteq> site; p \<noteq> parent; mdbNext site_node = 0; m \<turnstile> p \<leftarrow> p'; p' = mdbNext parent_node\<rbrakk> \<Longrightarrow> \<exists>z. (mdbNext parent_node = p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = z) \<and> p = mdbPrev (cteMDBNode z)) \<and> (mdbNext parent_node \<noteq> p' \<longrightarrow> (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal:
No subgoals!