theory CNodeInv_R

lemma (in mdb_swap) prev_not0_into_dom:
  assumes np: "n p = Some cte"
  and n0: "mdbPrev (cteMDBNode cte) \<noteq> 0"
  shows "mdbPrev (cteMDBNode cte) \<in> dom m" proof - note p_next_qe_src = mdb_ptr_src.p_next_qe note annoying_simps [simp del]
    = next_dest_prev_src  next_dest_prev_src_sym prev_dest_next_src prev_dest_next_src_sym note really_annoying_simps [simp del] = word_neq_0_conv from np have "p \<in> dom n" by (rule domI) then obtain ctep where mp: "m p = Some ctep" by (clarsimp simp add: dom_n_m) show ?thesis proof (cases rule: swap_ptr_cases [where p = p]) case p_src_prev thus ?thesis using mp np n0 src dest apply simp apply (frule n_src_prev) apply (auto simp: elim: dlistEp) done next case p_src thus ?thesis using mp np n0 src dest apply (clarsimp simp add: dest2_node_prev) apply safe apply simp+ apply (erule dlistEp, fastforce) apply simp done next case p_src_next thus ?thesis using mp np n0 src dest apply simp apply (frule n_src_next) apply (auto simp: elim: dlistEp) done next case p_dest_prev thus ?thesis using mp np n0 src dest apply simp apply (frule n_dest_prev) apply (auto elim: dlistEp) done next case p_dest thus ?thesis using mp np n0 src dest apply (clarsimp simp: n_dest) apply (erule dlistEp, fastforce) apply simp done next case p_dest_next thus ?thesis using mp np n0 src dest apply simp apply (frule n_dest_next) apply (auto simp: elim: dlistEp) done next case p_other thus ?thesis using mp np n0 src dest by (auto simp: n_other elim: dlistEp) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
m ?p' = Some (CTE ?cap' ?node') \<Longrightarrow> (mdbNext ?node' = mdbNext src_node) = (src = ?p' \<or> mdbNext src_node = 0 \<and> mdbNext ?node' = 0)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
(mdbNext dest_node = src) = (mdbPrev src_node = dest)
(src = mdbNext dest_node) = (mdbPrev src_node = dest)
(mdbPrev dest_node = src) = (mdbNext src_node = dest)
(src = mdbPrev dest_node) = (mdbNext src_node = dest)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
(?w \<noteq> 0) = (0 < ?w)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (chain)
picking this:
n p = Some cte proof (prove)
using this:
n p = Some cte

goal (1 subgoal):
 1. p \<in> dom n proof (state)
this:
p \<in> dom n

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (chain)
picking this:
p \<in> dom n proof (prove)
using this:
p \<in> dom n

goal (1 subgoal):
 1. (\<And>ctep. m p = Some ctep \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m p = Some ctep

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (7 subgoals):
 1. p = mdbPrev src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = src \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 6. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 7. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = mdbPrev src_node

goal (7 subgoals):
 1. p = mdbPrev src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = src \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 6. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 7. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbPrev src_node

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbPrev src_node
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbPrev src_node; m (mdbPrev src_node) = Some ctep; n (mdbPrev src_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbPrev src_node; m (mdbPrev src_node) = Some ctep; n (mdbPrev src_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<exists>cte'. n (mdbPrev src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node then mdbNext src_node else dest) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext dest_node = mdbPrev src_node \<or> src = mdbNext dest_node then src else mdbPrev (cteMDBNode ctep))\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (6 subgoals):
 1. p = src \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 6. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (6 subgoals):
 1. p = src \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 6. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = src

goal (6 subgoals):
 1. p = src \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 6. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = src

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = src
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = src; (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); ctep = CTE src_cap src_node; cte = CTE dcap dest2_node\<rbrakk> \<Longrightarrow> (dest = mdbNext src_node \<longrightarrow> (\<exists>y. m (mdbNext src_node) = Some y)) \<and> (dest \<noteq> mdbNext src_node \<longrightarrow> (\<exists>y. m (mdbPrev dest_node) = Some y)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = src; (if mdbNext src_node = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) \<noteq> 0; m src = Some (CTE src_cap src_node); m (mdbNext src_node) = Some (CTE dest_cap dest_node); ctep = CTE src_cap src_node; cte = CTE dcap (mdb_swap.dest2_node src_node (mdbNext src_node) dest_node); dest = mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbNext src_node) = Some y
 2. \<lbrakk>p = src; (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); ctep = CTE src_cap src_node; cte = CTE dcap dest2_node; dest \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbPrev dest_node) = Some y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = src; mdbPrev dest_node \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); ctep = CTE src_cap src_node; cte = CTE dcap dest2_node; dest \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbPrev dest_node) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>p = src; mdbPrev dest_node \<noteq> 0; m src = Some (CTE src_cap src_node); ctep = CTE src_cap src_node; cte = CTE dcap dest2_node; dest \<noteq> mdbNext src_node; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbPrev dest_node) = Some y proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (5 subgoals):
 1. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (5 subgoals):
 1. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = mdbNext src_node

goal (5 subgoals):
 1. p = mdbNext src_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 5. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbNext src_node

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbNext src_node
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbNext src_node; m (mdbNext src_node) = Some ctep; n (mdbNext src_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbNext src_node; m (mdbNext src_node) = Some ctep; n (mdbNext src_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<exists>cte'. n (mdbNext src_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node \<or> mdbNext src_node = mdbPrev dest_node then src else mdbNext (cteMDBNode ctep)) \<and> mdbPrev (cteMDBNode cte') = (if dest = mdbNext src_node then mdbPrev src_node else dest)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (4 subgoals):
 1. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (4 subgoals):
 1. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = mdbPrev dest_node

goal (4 subgoals):
 1. p = mdbPrev dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 4. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbPrev dest_node

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbPrev dest_node
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbPrev dest_node; m (mdbPrev dest_node) = Some ctep; n (mdbPrev dest_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbPrev dest_node; m (mdbPrev dest_node) = Some ctep; n (mdbPrev dest_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<exists>cte'. n (mdbPrev dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if dest = mdbNext src_node then mdbNext dest_node else src) \<and> mdbPrev (cteMDBNode cte') = (if mdbNext src_node = mdbPrev dest_node \<or> dest = mdbNext src_node then dest else mdbPrev (cteMDBNode ctep))\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (3 subgoals):
 1. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (3 subgoals):
 1. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = dest

goal (3 subgoals):
 1. p = dest \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 3. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = dest

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = dest
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = dest; mdbPrev src_node \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); ctep = CTE dest_cap dest_node; cte = CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)); mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbPrev src_node) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>p = dest; mdbPrev src_node \<noteq> 0; m dest = Some (CTE dest_cap dest_node); ctep = CTE dest_cap dest_node; cte = CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)); mdbPrev src_node \<noteq> dest; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>y. m (mdbPrev src_node) = Some y proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (2 subgoals):
 1. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (2 subgoals):
 1. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p = mdbNext dest_node

goal (2 subgoals):
 1. p = mdbNext dest_node \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m
 2. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbNext dest_node

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p = mdbNext dest_node
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbNext dest_node; m (mdbNext dest_node) = Some ctep; n (mdbNext dest_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbNext dest_node; m (mdbNext dest_node) = Some ctep; n (mdbNext dest_node) = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<exists>cte'. n (mdbNext dest_node) = Some cte' \<and> mdbNext (cteMDBNode cte') = (if src = mdbNext dest_node \<or> mdbNext dest_node = mdbPrev src_node then dest else mdbNext (cteMDBNode ctep)) \<and> mdbPrev (cteMDBNode cte') = (if src = mdbNext dest_node then mdbPrev dest_node else src)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal (1 subgoal):
 1. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
p \<noteq> mdbPrev src_node
p \<noteq> src
p \<noteq> mdbNext src_node
p \<noteq> mdbPrev dest_node
p \<noteq> dest
p \<noteq> mdbNext dest_node

goal (1 subgoal):
 1. \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p \<noteq> mdbPrev src_node
p \<noteq> src
p \<noteq> mdbNext src_node
p \<noteq> mdbPrev dest_node
p \<noteq> dest
p \<noteq> mdbNext dest_node

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (prove)
using this:
p \<noteq> mdbPrev src_node
p \<noteq> src
p \<noteq> mdbNext src_node
p \<noteq> mdbPrev dest_node
p \<noteq> dest
p \<noteq> mdbNext dest_node
m p = Some ctep
n p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<in> dom m proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal:
No subgoals! proof (state)
this:
mdbPrev (cteMDBNode cte) \<in> dom m

goal:
No subgoals!