theory Finalise_R

lemma n_tranclD:
  "n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> p' \<noteq> slot" apply (erule trancl_induct) apply (clarsimp simp add: n_next_eq split: if_split_asm) apply (rule mdb_chain_0D) apply (rule chain) apply (clarsimp simp: slot) apply (blast intro: trancl_trans prev_slot_next) apply fastforce apply (clarsimp simp: n_next_eq split: if_split_asm) apply (erule trancl_trans) apply (blast intro: trancl_trans prev_slot_next) apply (fastforce intro: trancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> p' \<noteq> slot proof (prove)
goal (2 subgoals):
 1. \<And>y. n \<turnstile> p \<leadsto> y \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (4 subgoals):
 1. p = slot \<Longrightarrow> m \<turnstile> slot \<leadsto>\<^sup>+ 0
 2. \<lbrakk>p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y. \<lbrakk>p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 4. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (5 subgoals):
 1. p = slot \<Longrightarrow> mdb_chain_0 m
 2. p = slot \<Longrightarrow> slot \<in> dom m
 3. \<lbrakk>p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 4. \<And>y. \<lbrakk>p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 5. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (4 subgoals):
 1. p = slot \<Longrightarrow> slot \<in> dom m
 2. \<lbrakk>p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 3. \<And>y. \<lbrakk>p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 4. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y. \<lbrakk>p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 3. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y \<and> y \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> slot; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ mdbPrev s_node; mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev s_node \<leadsto>\<^sup>+ mdbNext s_node
 2. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> slot; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto>\<^sup>+ y; y \<noteq> slot; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z \<and> z \<noteq> slot proof (prove)
goal:
No subgoals!