theory CNodeInv_R

lemma mdb_chain_0_trancl:
  assumes chain: "mdb_chain_0 m"
  and   n0: "no_0 m"
  and   ab: "m \<turnstile> a \<leadsto>\<^sup>+ b"
  shows "m \<turnstile> b \<leadsto>\<^sup>* 0" using ab proof induct case (base y) thus ?case using chain by (clarsimp simp: next_unfold') (erule (1) mdb_chain_0_nextD) next case (step y z) thus ?case using n0 apply - apply (erule next_rtrancl_tranclE) apply (simp add: next_unfold') apply (drule tranclD [where x = y]) apply clarsimp apply (drule (1) next_single_value) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> b \<leadsto>\<^sup>* 0 proof (prove)
using this:
m \<turnstile> a \<leadsto>\<^sup>+ b

goal (1 subgoal):
 1. m \<turnstile> b \<leadsto>\<^sup>* 0 proof (state)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> a \<leadsto> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* 0
 2. \<And>y z. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (state)
this:
m \<turnstile> a \<leadsto> y

goal (2 subgoals):
 1. \<And>y. m \<turnstile> a \<leadsto> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* 0
 2. \<And>y z. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
using this:
m \<turnstile> a \<leadsto> y

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* 0 proof (prove)
using this:
m \<turnstile> a \<leadsto> y
mdb_chain_0 m

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* 0 proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* 0

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (state)
this:
m \<turnstile> a \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> y \<leadsto>\<^sup>* 0

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
using this:
m \<turnstile> a \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> y \<leadsto>\<^sup>* 0

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
using this:
m \<turnstile> a \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> y \<leadsto>\<^sup>* 0
no_0 m

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> y \<leadsto>\<^sup>* 0; no_0 m\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; no_0 m; y = 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0
 2. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; no_0 m; y \<noteq> 0; m \<turnstile> y \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; no_0 m; y \<noteq> 0; m \<turnstile> y \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; no_0 m; y \<noteq> 0; \<exists>z. m \<turnstile> y \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<And>za. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; no_0 m; y \<noteq> 0; m \<turnstile> y \<leadsto> za; m \<turnstile> za \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<And>za. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ y; no_0 m; y \<noteq> 0; m \<turnstile> y \<leadsto> za; m \<turnstile> za \<leadsto>\<^sup>* 0; z = za\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>* 0 proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> z \<leadsto>\<^sup>* 0

goal:
No subgoals!