theory Finalise_R

lemma m_tranclD:
  "m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow>
  if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p'
  else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
  else n \<turnstile> p \<leadsto>\<^sup>+ p'" using no_0_n apply - apply (erule trancl_induct) apply clarsimp apply (rule conjI) apply clarsimp apply (rule r_into_trancl) apply (clarsimp simp: n_next_eq) apply clarsimp apply (rule conjI) apply (insert m_slot_next)[1] apply (clarsimp simp: mdb_next_unfold) apply clarsimp apply (rule r_into_trancl) apply (clarsimp simp: n_next_eq) apply (rule context_conjI) apply (clarsimp simp: mdb_next_unfold) apply (drule prev_slot_next) apply (clarsimp simp: mdb_next_unfold) apply clarsimp apply (rule conjI) apply clarsimp apply (rule conjI) apply clarsimp apply (drule prev_slot_next) apply (drule trancl_trans, erule r_into_trancl) apply simp apply clarsimp apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp add: n_next_eq) apply clarsimp apply (rule conjI) apply clarsimp apply (erule rtrancl_trans) apply (rule r_into_rtrancl) apply (simp add: n_next_eq) apply (rule conjI) apply clarsimp apply (rule context_conjI) apply (clarsimp simp: mdb_next_unfold) apply (drule prev_slot_next) apply (clarsimp simp: mdb_next_unfold) apply clarsimp apply clarsimp apply (simp split: if_split_asm) apply (clarsimp simp: mdb_next_unfold slot) apply (erule trancl_trans) apply (rule r_into_trancl) apply (clarsimp simp add: n_next_eq) apply (rule context_conjI) apply (clarsimp simp: mdb_next_unfold) apply (drule prev_slot_next) apply (clarsimp simp: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p' else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
no_0 n

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p' else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ p'; no_0 n\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p' else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> (y = slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node)) \<and> (y \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y))
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y = slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node)
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y)
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y)
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; mdbPrev s_node \<noteq> 0; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto> mdbNext s_node
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y)
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> y \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y)
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot\<rbrakk> \<Longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y)
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot\<rbrakk> \<Longrightarrow> p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot; m \<turnstile> slot \<leadsto> mdbNext s_node\<rbrakk> \<Longrightarrow> p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto> y; y \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> y
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> mdbPrev s_node \<leadsto> y; y \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> y = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> mdbPrev s_node \<leadsto> y; y \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<And>y. \<lbrakk>no_0 n; m \<turnstile> mdbPrev s_node \<leadsto> y; y \<noteq> slot; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> y = mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> mdbPrev s_node \<leadsto> y; y \<noteq> slot; p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> y = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; m \<turnstile> mdbPrev s_node \<leadsto> y; y \<noteq> slot; p = mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> y = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z else if z = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> (z = slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node)) \<and> (z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z)) proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z = slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node)
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node)
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node; p = slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node; p = slot; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>no_0 n; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node; p = slot; m \<turnstile> mdbPrev s_node \<leadsto> slot; m \<turnstile> slot \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* mdbPrev s_node else n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbPrev s_node \<leadsto> mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> z \<noteq> slot \<longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> (p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z) \<and> (p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z) proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p = slot \<longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* z
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto>\<^sup>* z
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto> z
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> (y = mdbPrev s_node \<longrightarrow> mdbPrev s_node \<noteq> 0 \<and> z = mdbNext s_node) \<and> (y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0)
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y = mdbPrev s_node \<longrightarrow> mdbPrev s_node \<noteq> 0 \<and> z = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> z = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<And>z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; z \<noteq> slot; p = slot; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> z = mdbNext s_node
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 4. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; z \<noteq> slot; p = slot; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> z = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; z \<noteq> slot; p = slot; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> z = mdbNext s_node
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 3. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; z \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> y \<noteq> mdbPrev s_node \<longrightarrow> y = slot \<longrightarrow> z = 0
 2. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* y else if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; if y = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node else n \<turnstile> p \<leadsto>\<^sup>+ y; z \<noteq> slot; p \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ slot; m \<turnstile> slot \<leadsto> z; y = slot; n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z
 2. \<And>y z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> slot; n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> slot; n \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; y \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0 \<and> z = mdbNext s_node proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z\<rbrakk> \<Longrightarrow> mdbPrev s_node \<noteq> 0
 2. \<And>z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> z = mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> z = mdbNext s_node proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<noteq> slot; p \<noteq> slot; no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> mdbPrev s_node \<leadsto> z; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> z = mdbNext s_node proof (prove)
goal:
No subgoals!