theory CSpace_I

lemma (in mdb_ptr) descendants_of_init':
  assumes n: "no_mdb (CTE cap node)"
  shows
  "descendants_of' p' (m(p \<mapsto> CTE c initMDBNode)) =
   descendants_of' p' m" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (rule iffI) apply (erule subtree.induct) apply (frule no_mdb_not_target [where p=p]) apply simp apply (simp add: no_mdb_def) apply (rule valid_dlist_init[OF dlist, OF m_p n]) apply (insert no_0)[1] apply (clarsimp simp: no_0_def) apply (clarsimp simp: mdb_next_unfold split: if_split_asm) apply (rule direct_parent) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (clarsimp simp: parentOf_def split: if_split_asm) apply (frule no_mdb_not_target [where p=p]) apply simp apply (simp add: no_mdb_def) apply (rule valid_dlist_init[OF dlist, OF m_p n]) apply (insert no_0)[1] apply (clarsimp simp: no_0_def) apply (subgoal_tac "p' \<noteq> p") apply (erule trans_parent) apply (clarsimp simp: mdb_next_unfold split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def m_p split: if_split_asm) apply clarsimp apply (drule subtree_mdb_next)+ apply (drule tranclD)+ apply clarsimp apply (insert n)[1] apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) apply (erule subtree.induct) apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) apply (rule dlist) apply (rule no_0) apply (subgoal_tac "p'\<noteq>p") prefer 2 apply (insert n)[1] apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) apply (rule direct_parent) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (clarsimp simp: parentOf_def) apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) apply (rule dlist) apply (rule no_0) apply (subgoal_tac "c'\<noteq>p") prefer 2 apply (insert n)[1] apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) apply (subgoal_tac "p'\<noteq>p") apply (erule trans_parent) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (clarsimp simp: parentOf_def) apply clarsimp apply (drule subtree_mdb_next) apply (drule tranclD) apply clarsimp apply (insert n) apply (clarsimp simp: mdb_next_unfold no_mdb_def m_p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p' (m(p \<mapsto> CTE c initMDBNode)) = descendants_of' p' m proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p' (m(p \<mapsto> CTE c initMDBNode))) = (x \<in> descendants_of' p' m) proof (prove)
goal (1 subgoal):
 1. \<And>x. m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x = m \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x. m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x \<Longrightarrow> m \<turnstile> p' \<rightarrow> x
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (7 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> (m(p \<mapsto> CTE c initMDBNode)) p = Some (?cte8 x c')
 2. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_mdb (?cte8 x c')
 3. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 4. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 5. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 6. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 7. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (6 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_mdb (CTE c initMDBNode)
 2. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 3. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 4. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 5. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 6. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 3. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 4. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 5. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 4. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; no_0 m\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 4. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> mdbNext (cteMDBNode z)
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<leadsto> mdbNext (cteMDBNode z)
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 3. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf mdbNext (cteMDBNode z)
 4. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 5. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) \<noteq> 0
 2. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf mdbNext (cteMDBNode z)
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 4. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p' parentOf mdbNext (cteMDBNode z); mdbNext (cteMDBNode z) \<noteq> p; p' \<noteq> p; m p' = Some z\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf mdbNext (cteMDBNode z)
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (6 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> (m(p \<mapsto> CTE c initMDBNode)) p = Some (?cte41 x c' c'')
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_mdb (?cte41 x c' c'')
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 4. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 5. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 6. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_mdb (CTE c initMDBNode)
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 4. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 5. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 4. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; no_0 m\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE c initMDBNode))
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' \<rightarrow> c''
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf c''
 4. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 5. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf c''
 3. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 4. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> p' parentOf c''
 2. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 3. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p parentOf c''; c'' \<noteq> p; p' = p\<rbrakk> \<Longrightarrow> False
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p parentOf c''; c'' \<noteq> p; p' = p; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<leadsto>\<^sup>+ c'; m \<turnstile> p \<leadsto>\<^sup>+ c'\<rbrakk> \<Longrightarrow> False
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p parentOf c''; c'' \<noteq> p; p' = p; \<exists>z. (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<leadsto> z \<and> (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> z \<leadsto>\<^sup>* c'; \<exists>z. m \<turnstile> p \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* c'\<rbrakk> \<Longrightarrow> False
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c' c'' z za. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p parentOf c''; c'' \<noteq> p; p' = p; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<leadsto> z; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> z \<leadsto>\<^sup>* c'; m \<turnstile> p \<leadsto> za; m \<turnstile> za \<leadsto>\<^sup>* c'\<rbrakk> \<Longrightarrow> False
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>c' c'' z za. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>a. if a = p then Some (CTE c initMDBNode) else m a \<turnstile> p parentOf c''; c'' \<noteq> p; p' = p; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<leadsto> z; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> z \<leadsto>\<^sup>* c'; m \<turnstile> p \<leadsto> za; m \<turnstile> za \<leadsto>\<^sup>* c'; no_mdb (CTE cap node)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. \<And>x. m \<turnstile> p' \<rightarrow> x \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 m
 3. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 4. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'\<rbrakk> \<Longrightarrow> no_0 m
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; no_mdb (CTE cap node)\<rbrakk> \<Longrightarrow> p' \<noteq> p
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<leadsto> c'
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'
 4. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p' \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p' parentOf c'; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 m
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''\<rbrakk> \<Longrightarrow> no_0 m
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c''
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> c' \<noteq> p proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p\<rbrakk> \<Longrightarrow> c' \<noteq> p
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; no_mdb (CTE cap node)\<rbrakk> \<Longrightarrow> c' \<noteq> p
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c''
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p proof (prove)
goal (4 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> c' \<leadsto> c''
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''
 4. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' parentOf c''
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p' \<rightarrow> c'; m(p \<mapsto> CTE c initMDBNode) \<turnstile> p' \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p' parentOf c''; c'' \<noteq> p; c' \<noteq> p\<rbrakk> \<Longrightarrow> p' \<noteq> p proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' = p; m \<turnstile> p \<leadsto>\<^sup>+ c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' = p; \<exists>z. m \<turnstile> p \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c' c'' z. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' = p; m \<turnstile> p \<leadsto> z; m \<turnstile> z \<leadsto>\<^sup>* c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c' c'' z. \<lbrakk>(\<lambda>a. if a = p then Some (CTE c initMDBNode) else m a) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c'' \<noteq> p; c' \<noteq> p; p' = p; m \<turnstile> p \<leadsto> z; m \<turnstile> z \<leadsto>\<^sup>* c'; no_mdb (CTE cap node)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!