theory Finalise_R

lemma n_trancl_eq:
  "n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot)" using no_0_n apply - apply (rule iffI) apply (frule n_tranclD) apply clarsimp apply (drule tranclD) apply (clarsimp simp: n_next_eq) apply (simp add: rtrancl_eq_or_trancl) apply clarsimp apply (drule m_tranclD) apply (simp split: if_split_asm) apply (rule r_into_trancl) apply (simp add: n_next_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot) proof (prove)
using this:
no_0 n

goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot) proof (prove)
goal (1 subgoal):
 1. no_0 n \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; n \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; n \<turnstile> p \<leadsto>\<^sup>+ p'; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; n \<turnstile> slot \<leadsto>\<^sup>+ p'; m \<turnstile> slot \<leadsto>\<^sup>+ p'; p' \<noteq> slot; p = slot\<rbrakk> \<Longrightarrow> p' = 0
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ p'; p' \<noteq> slot; p = slot; \<exists>z. n \<turnstile> slot \<leadsto> z \<and> n \<turnstile> z \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = 0
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 n; m \<turnstile> slot \<leadsto>\<^sup>+ p'; p' \<noteq> slot; p = slot; n \<turnstile> 0 \<leadsto>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = 0
 2. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 n; m \<turnstile> p \<leadsto>\<^sup>+ p'; p = slot \<longrightarrow> p' = 0; p' \<noteq> slot\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 n; p = slot \<longrightarrow> p' = 0; p' \<noteq> slot; 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'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 n; p' = 0; p = slot; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> n \<turnstile> slot \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 n; p' = 0; p = slot; n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> n \<turnstile> slot \<leadsto> 0 proof (prove)
goal:
No subgoals!