theory Finalise_R

lemma parency_m:
  assumes "m \<turnstile> p \<rightarrow> p'"
  shows "p \<noteq> slot \<longrightarrow> (if p' \<noteq> slot then n \<turnstile> p \<rightarrow> p' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)" using assms proof induct case (direct_parent c) thus ?case apply clarsimp apply (rule conjI) apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n_next_eq) apply clarsimp apply (subgoal_tac "mdbPrev s_node \<noteq> 0") prefer 2 apply (clarsimp simp: mdb_next_unfold) apply (drule prev_slot_next) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (erule m_parent_of, simp, simp) apply clarsimp apply clarsimp apply (drule dlist_next_src_unique) apply fastforce apply clarsimp apply simp apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n_next_eq) apply (drule subtree_parent) apply (clarsimp simp: parentOf_def) apply (drule subtree_parent) apply (erule (1) m_parent_of_next) apply clarsimp apply clarsimp done next case (trans_parent c c') thus ?case apply clarsimp apply (rule conjI) apply clarsimp apply (cases "c=slot") apply simp apply (erule impE) apply (erule subtree.trans_parent) apply fastforce apply (clarsimp simp: slot mdb_next_unfold) apply (clarsimp simp: slot mdb_next_unfold) apply (clarsimp simp: slot mdb_next_unfold) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n_next_eq) apply clarsimp apply (subgoal_tac "mdbPrev s_node \<noteq> 0") prefer 2 apply (clarsimp simp: mdb_next_unfold) apply (drule prev_slot_next) apply (clarsimp simp: mdb_next_unfold) apply assumption apply (erule m_parent_of, simp, simp) apply clarsimp apply (drule subtree_mdb_next) apply (drule trancl_trans) apply (erule r_into_trancl) apply simp apply clarsimp apply (drule dlist_next_src_unique) apply fastforce apply clarsimp apply simp apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n_next_eq) apply clarsimp apply (rule m_parent_of_next, erule subtree_parent, assumption, assumption) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<noteq> slot \<longrightarrow> (if p' \<noteq> slot then n \<turnstile> p \<rightarrow> p' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
using this:
m \<turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> slot \<longrightarrow> (if p' \<noteq> slot then n \<turnstile> p \<rightarrow> p' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c'' \<noteq> slot then n \<turnstile> p \<rightarrow> c'' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (state)
this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c'' \<noteq> slot then n \<turnstile> p \<rightarrow> c'' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
using this:
m \<turnstile> p \<leadsto> c
c \<noteq> 0
m \<turnstile> p parentOf c

goal (1 subgoal):
 1. p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> (c \<noteq> slot \<longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<rightarrow> c) \<and> (c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> p = mdbPrev s_node \<longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 2. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 5. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node \<leadsto> c; c \<noteq> 0; m \<turnstile> mdbPrev s_node parentOf c; c \<noteq> slot; p = mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> c
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; c \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> c \<noteq> mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> mdbNext s_node; mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> ?y63 \<leadsto> mdbNext s_node
 2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node; p = ?y63\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node; p = slot\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext s_node \<noteq> 0; p \<noteq> slot; c = mdbNext s_node; p = slot\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; c \<noteq> 0; m \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto> mdbNext s_node
 2. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node parentOf mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node parentOf mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node parentOf mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; m \<turnstile> mdbPrev s_node \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node parentOf mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node; m \<turnstile> mdbPrev s_node parentOf mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node parentOf mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> slot
 2. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> mdbPrev s_node parentOf slot; c = slot; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> mdbNext s_node proof (prove)
goal:
No subgoals! proof (state)
this:
p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c'' \<noteq> slot then n \<turnstile> p \<rightarrow> c'' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c'' \<noteq> slot then n \<turnstile> p \<rightarrow> c'' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (state)
this:
m \<turnstile> p \<rightarrow> c
p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> (if c'' \<noteq> slot then n \<turnstile> p \<rightarrow> c'' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
using this:
m \<turnstile> p \<rightarrow> c
p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)
m \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (1 subgoal):
 1. p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> (c' \<noteq> slot \<longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<rightarrow> c') \<and> (c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> slot \<longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c = slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c = slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot; n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> mdbNext s_node
 2. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node
 4. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot; n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 5. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 6. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot; n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 5. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot; n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> slot; m \<turnstile> slot \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = slot; n \<turnstile> p \<rightarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; n \<turnstile> p \<rightarrow> c; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c = mdbPrev s_node \<longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 5. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 5. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c = mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> c' = mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> c'
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c' \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; c \<noteq> slot; p = c'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; c \<noteq> slot; p = c'; m \<turnstile> c' \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; c \<noteq> slot; p = c'\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ ?z76
 2. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; c \<noteq> slot; p = c'; m \<turnstile> c' \<leadsto>\<^sup>+ ?z76\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; c \<noteq> slot; p = c'; m \<turnstile> c' \<leadsto>\<^sup>+ c'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; c' \<noteq> slot; p \<noteq> slot; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; m \<turnstile> c \<leadsto> mdbNext s_node; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> m \<turnstile> ?y85 \<leadsto> mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node; c = ?y85\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node; c = slot\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; mdbNext s_node \<noteq> 0; p \<noteq> slot; c \<noteq> slot; c' = mdbNext s_node; c = slot\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> c; p \<noteq> slot \<longrightarrow> (if c \<noteq> slot then n \<turnstile> p \<rightarrow> c else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node); m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = slot \<longrightarrow> p \<noteq> slot \<longrightarrow> m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; n \<turnstile> p \<rightarrow> mdbPrev s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto> mdbNext s_node
 2. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 3. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbNext s_node \<noteq> 0
 2. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> mdbPrev s_node; m \<turnstile> p parentOf slot; c' = slot; p \<noteq> slot; m \<turnstile> p \<rightarrow> mdbNext s_node; mdbPrev s_node \<noteq> 0; c = mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> mdbNext s_node proof (prove)
goal:
No subgoals! proof (state)
this:
p \<noteq> slot \<longrightarrow> (if c' \<noteq> slot then n \<turnstile> p \<rightarrow> c' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)

goal:
No subgoals!