theory Finalise_R

lemma valid_dlist_n:
  "valid_dlist n" using dlist apply (clarsimp simp: valid_dlist_def2 [OF no_0_n]) apply (simp add: n_next_eq n_prev_eq m_slot_next m_slot_prev cong: if_cong) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp simp: next_slot_prev prev_slot_next) apply (fastforce dest!: dlist_prev_src_unique) apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp simp: valid_dlist_def2 [OF no_0]) apply (case_tac "mdbNext s_node = 0") apply simp apply (subgoal_tac "m \<turnstile> slot \<leadsto> c'") prefer 2 apply fastforce apply (clarsimp simp: mdb_next_unfold slot) apply (frule next_slot_prev) apply (drule (1) dlist_prev_src_unique, simp) apply simp apply clarsimp apply (rule conjI, clarsimp) apply (fastforce dest: dlist_next_src_unique) apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp simp: valid_dlist_def2 [OF no_0]) apply (clarsimp simp: mdb_prev_def slot) apply (clarsimp simp: valid_dlist_def2 [OF no_0]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist n proof (prove)
using this:
valid_dlist m

goal (1 subgoal):
 1. valid_dlist n proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto> c' = n \<turnstile> c \<leftarrow> c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> (c = mdbPrev s_node \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> slot = m \<turnstile> slot \<leftarrow> mdbNext s_node) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> mdbPrev s_node \<leftarrow> c')) \<and> (c \<noteq> mdbPrev s_node \<longrightarrow> (c = slot \<longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> slot \<leftarrow> c') \<and> (c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')))) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>valid_dlist m; mdbPrev s_node \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> (c' = mdbNext s_node \<longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto> slot = m \<turnstile> slot \<leftarrow> mdbNext s_node) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> mdbPrev s_node \<leftarrow> c')
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> c \<noteq> mdbPrev s_node \<longrightarrow> (c = slot \<longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> slot \<leftarrow> c') \<and> (c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'))) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>valid_dlist m; mdbPrev s_node \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> mdbPrev s_node \<leftarrow> c'
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> c \<noteq> mdbPrev s_node \<longrightarrow> (c = slot \<longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> slot \<leftarrow> c') \<and> (c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'))) proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> c \<noteq> mdbPrev s_node \<longrightarrow> (c = slot \<longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> slot \<leftarrow> c') \<and> (c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'))) proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> (c = slot \<longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> c' \<noteq> slot \<longrightarrow> \<not> m \<turnstile> slot \<leftarrow> c') \<and> (c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'))) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>valid_dlist m; c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0; m \<turnstile> slot \<leadsto> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> c'
 3. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 4. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0\<rbrakk> \<Longrightarrow> m \<turnstile> slot \<leadsto> c'
 2. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0; m \<turnstile> slot \<leadsto> c'\<rbrakk> \<Longrightarrow> False
 3. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 4. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node = 0; m \<turnstile> slot \<leadsto> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; m \<turnstile> slot \<leftarrow> c'; mdbNext s_node \<noteq> 0; m \<turnstile> slot \<leftarrow> mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c' \<noteq> 0; c' \<noteq> mdbNext s_node; c' \<noteq> slot; mdbNext s_node \<noteq> 0; m \<turnstile> slot \<leftarrow> mdbNext s_node; c' = mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> c \<noteq> slot \<longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> (c' = mdbNext s_node \<longrightarrow> (c, mdbNext s_node) \<notin> mdb_next_rel m) \<and> (c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')) proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>valid_dlist m; c \<noteq> 0; mdbNext s_node \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; m \<turnstile> c \<leadsto> mdbNext s_node\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c') proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot\<rbrakk> \<Longrightarrow> c' \<noteq> mdbNext s_node \<longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c') proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; c' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> (c' = slot \<longrightarrow> (c, slot) \<notin> mdb_next_rel m) \<and> (c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c') proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>valid_dlist m; c \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; m \<turnstile> c \<leadsto> slot\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; c' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); c \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; m \<turnstile> c \<leftarrow> slot\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; c' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0; c \<noteq> mdbPrev s_node; c \<noteq> slot; c' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> c' \<noteq> slot \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c' proof (prove)
goal:
No subgoals!